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.