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

Formal Analysis and Proof of Java Security Mechanisms

作　　者：江南[1,2] 何炎祥[1,3] 张晓瞳 刘瑞[1] 沈云飞[1] JIANG Nan;HE Yanxiang;ZHANG Xiaotong;LIU RUI;SHEN Yunfei(Computer School,Wuhan University,Wuhan 430072, China;Computer School, Hubei University of Technology,Wuhan 430068, China;State Key Laboratory of Software Engineering,Wuhan University,Wuhan 430072, China)

机构地区：[1]武汉大学计算机学院,武汉430072 [2]湖北工业大学计算机学院,武汉430068 [3]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机科学与探索》2016年第11期1501-1511,共11页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金No.61373039~~

摘　　要：Java访问控制一方面提供了语言级的安全性机制,这种机制针对程序中所声明的实体,通过不同的访问修饰符,向其使用者屏蔽实体的实现细节;另一方面,它也导致了该语言规范的复杂性和实现的不一致性。分析了Java访问控制机制,包括类型、成员变量和成员方法的可访问性,以及可访问性与继承关系、方法覆盖、动态绑定之间的交互;然后使用定理证明助手Isabelle/HOL 2015严格定义了这些语义规范;最后陈述并证明了这些定义所满足的性质定理,从而表明该形式化定义的正确性。Java access control is designed to provide security mechanisms on programming language level whichprevent the users of an entity declared in a program from depending on unnecessary details of the implementation ofthis entity with different access modifiers. On the other hand, this design leads to the complexity of the semanticsdescribed 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, memberinvariables and member methods and the interactions between accessibility and inheritance, method overriding anddynamic binding, this paper gives strict definitions of these semantics in Isabelle/HOL 2015. Finally, this paperstates and proves the properties that these definitions satisfy, which shows that this formalization is correct.

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

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]