State Space Reduction for Verifying Noninterference
Existing algorithmic approaches to verifying noninterference suffer from the state explosion problem. In order to make these approaches more practical, we proposed an abstraction technique which attempts to decrease the size of the security systeM by focusing on variables and local transitions of the system related with noninterference. In this way, noninterference is preserved, but the size of the model that needs to be verified becomes smaller. We further showed how the technique can be applied in verifying the programming language IMP. We proposed an over approximation computation of related variables and local transitions such that our technique can be implemented automatically. Our technique also can be extended to verify intransitive noninterference smoothly.
noninterference abstraction intransitive noninterference
Conghua Zhou Li Chen Shiguang Ju Zhifeng Liu
School of Computer Science and Telecommunication Engineering Jiangsu University, Zhenjiang,212013, C School of Computer Science and Telecommunication Engineering Jiangsu University,Zhenjiang,212013,Chi
国际会议
上海
英文
132-138
2009-07-08（万方平台首次上网日期，不代表论文的发表时间）