Java安全性机制的形式分析与证明

来源：计算机科学与探索杂志2016年第11期北京时间：

作者：江南，何炎祥，张晓瞳，刘瑞，沈云飞

单位：1. 武汉大学 计算机学院，武汉 4300722. 湖北工业大学 计算机学院，武汉 430068 3. 武汉大学 软件工程国家重点实验室，武汉 430072

摘要：Java访问控制一方面提供了语言级的安全性机制，这种机制针对程序中所声明的实体，通过不同的访问修饰符，向其使用者屏蔽实体的实现细节；另一方面，它也导致了该语言规范的复杂性和实现的不一致性。分析了Java访问控制机制，包括类型、成员变量和成员方法的可访问性，以及可访问性与继承关系、方法覆盖、动态绑定之间的交互；然后使用定理证明助手Isabelle/HOL 2015严格定义了这些语义规范；最后陈述并证明了这些定义所满足的性质定理，从而表明该形式化定义的正确性。

关键词：Java访问控制,动态绑定,形式分析,定理证明