| 基于无干扰理论的并发程序隐私性分析模型研究 |
| |
| 引用本文： | 曹珲,张焕国,严飞. 基于无干扰理论的并发程序隐私性分析模型研究[J]. 武汉大学学报(理学版), 2012, 58(6) |
| |
| 作者姓名： | 曹珲 张焕国 严飞 |
| |
| 作者单位： | 武汉大学计算机学院／空天信息安全与可信计算教育部重点实验室,湖北武汉,430072 |
| |
| 基金项目： | 国家自然科学基金，湖北省自然基金，中央高校基本科研业务费专项资金 |
| |
| 摘 要： | 基于无干扰理论和Hoare公理方法,针对并发进程中不可信代码带来的信息泄露问题,提出一种隐私性分析模型CPNIAM,一方面把并发程序功能正确性证明分化为对程序中所有并发进程的形式化验证,以达到复杂程序简单化证明的目的;另一方面,可以在进程的功能正确性验证的基础上进行并发进程间的无干扰性分析.实例分析表明,相对于传统的无干扰模型,本文提出的模型可以在程序设计及实现阶段的形式化验证过程中,对由不可信代码导致的进程间隐私泄露问题进行分析,分析结果可指导程序设计者用于不可信代码定位和修改.
|
| 关 键 词： | 隐私保护 无干扰理论 Hoare公理方法 并发程序 形式化验证 |
The Research of Privacy Analysis Model for Concurrent Program Based on Noninterference Theory |
| |
| Abstract: | |
| |
| Keywords: | privacy preservingl noninterference theory Hoare axiom concurrent program formal verification |
| 本文献已被 万方数据 等数据库收录！ |
|
