Formal Analysis and Proof of Java Security Mechanisms

作者：JIANG Nan; HE Yanxiang; ZHANG Xiaotong; LIU RUI; SHEN Yunfei

来源：计算机科学与探索, 2016, 10(11).

DOI：10.3778/j.issn.1673-9418.1606039

• Java access control
• dynamic binding
• formal analysis
• theorem proving

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 implemen-tation. 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.

• 单位
  湖北工业大学; 武汉大学