java安全性机制的形式分析与证明 formal analysis and proof of java security mechanisms.pdfVIP

ISSN 1673-9418 CODEN JKYTA8 E-mail: fcst@vip. 163.com Journal of Frontiers of Computer Science and Technology 1673-9418/2016/ 10(11)- 1501-11 Tel: +86-10 doi: 10.3778/j.issn. 1673-9418.1606039 Java 安全性机制的形式分析与证明* 1,2+ 1,3 1 1 1 江 南 ，何炎祥 ，张晓瞳 ，刘 瑞 ，沈云飞 1. 武汉大学 计算机学院，武汉 430072 2. 湖北工业大学 计算机学院，武汉 430068 3. 武汉大学 软件工程国家重点实验室，武汉 430072 Formal Analysis and Proof of Java Security Mechanisms 1,2+ 1,3 1 1 1 JIANG Nan , HE Yanxiang , ZHANG Xiaotong , LIU RUI , SHEN Yunfei 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 + Corresponding author: E-mail: nanjiang@ JIANG Nan, HE Yanxiang, ZHANG Xiaotong, et al. Formal analysis and proof of Java security mechanisms. Journal of Frontiers of Computer Science and Technology, 2016, 10(11): 1501-1511. 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 implemen- tation. After analyzing the Java access control mechanism which includes the accessibilities of class type, member invaria