计算机科学与探索 ›› 2016, Vol. 10 ›› Issue (11): 1501-1511.DOI: 10.3778/j.issn.1673-9418.1606039

• 学术研究 • 上一篇    下一篇

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

江  南1,2+,何炎祥1,3,张晓瞳1,刘  瑞1,沈云飞1   

  1. 1. 武汉大学 计算机学院,武汉 430072
    2. 湖北工业大学 计算机学院,武汉 430068
    3. 武汉大学 软件工程国家重点实验室,武汉 430072
  • 出版日期:2016-11-01 发布日期:2016-11-04

Formal Analysis and Proof of Java Security Mechanisms

JIANG Nan1,2+, HE Yanxiang1,3, ZHANG Xiaotong1, LIU RUI1, SHEN Yunfei1   

  1. 1. Computer School, Wuhan University, Wuhan 430072, China
    2. Computer School, Hubei University of Technology, Wuhan 430068, China
    3. State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072, China
  • Online:2016-11-01 Published:2016-11-04

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

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

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