Abstract: Java access control is designed to provide security mechanisms on programming language level which prevent the users of an entity declared in a program from depending on unnecessary details of the implementation of this entity with different access modifiers. On the other hand, this design leads to the complexity of the semantics described in the Java language specification, and even the inconsistency between the specification and its implementation. After analyzing the Java access control mechanism which includes the accessibilities of class type, member invariables and member methods and the interactions between accessibility and inheritance, method overriding and dynamic binding, this paper gives strict definitions of these semantics in Isabelle/HOL 2015. Finally, this paper states and proves the properties that these definitions satisfy, which shows that this formalization is correct.

Key words: Java access control, dynamic binding, formal analysis, theorem proving

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

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