基于语言理论和实现技术的移动代码安全

利用在编译时产生的额外信息对不被信任的移动代码进行检查，以保证移动代码在本地主机上的执行是安全的和有效的。该研究以类型论作为主要理论基础，用形式化方法作为主要手段，用类型注释作为证书中的主要信息，并结合其它方法，解决高层的安全策略要求。研究成果可用来开认证编译器，对建设我们国家各种安全的信息系统有着重要的作用。