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

• 作者: 何炎祥 刘瑞 张晓瞳 江南 沈云飞
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: Java访问控制 动态绑定 形式分析 定理证明
• 年，卷（期）: 2016,（11）
• 所属期刊栏目: 学术研究
• 页码范围: 1502-1512
• 页数: 11页
• 分类号: TP312
• 字数: 9393字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1606039

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江南	武汉大学计算机学院	18	70	4.0	8.0
3	何炎祥	武汉大学计算机学院	179	1866	22.0	35.0
9	张晓瞳	武汉大学计算机学院	4	6	2.0	2.0
10	刘瑞	武汉大学计算机学院	5	7	2.0	2.0
11	沈云飞	武汉大学计算机学院	1	2	1.0	1.0