论文部分内容阅读
为完善Seal演算的自身性质及形式化证明移动代码的安全性，提出了一个信息流分析系统，该系统经过seal进程的静态分析，检查出一些比较重要的语义错误，通过发送和接收的同步来实现通信和代码移动，具体分为同层、父到子、子到父3种模式。重点分析了父子之间的代码移动及类型相容。该系统为Seal演算的自身性质的完善及移动代码的安全性判断提供了理论依据。