强制执行Java中的安全对象初始化
摘要：Sun和CERT建议在安全的Java开发中不允许访问部分初始化的对象。 CERT认为不遵循这一建议所带来的风险严重。当前用于强制执行对象初始化的解决方案是实现Sun提出的编码模式，但未经正式检查。我们提出了一种模块化的类型系统，以形式化地指定库或程序的初始化策略，并提供一个类型检查器，在加载时静态检查所有加载的类是否符合策略。这样可以证明在Java中一些著名的特权升级中不会出现漏洞。我们的实验结果显示，我们的安全默认策略可以证明91％的java.lang，java.security和javax.security类是安全的，无需任何注释，并且通过添加57个简单的注释，我们证明了除了四个类之外的所有类都是安全的。该类型系统及其周全性定理已经被形式化和使用Coq进行了机器检查。
作者：Laurent Hubert (INRIA - IRISA), Thomas Jensen (INRIA - IRISA), Vincent Monfort (INRIA - IRISA), David Pichardie (INRIA - IRISA)
论文ID：1007.3133
分类：Programming Languages
分类简称：cs.PL
提交时间：2010-11-22