Conference Proceedings

COVERN: A Logic for Compositional Verification of Information Flow Control

T Murray, R Sison, K Engelhardt

Proceedings of the 3rd IEEE European Symposium on Security and Privacy | IEEE | Published : 2018


Shared memory concurrency is pervasive in modern programming, including in systems that must protect highly sensitive data. Recently, verification has finally emerged as a practical tool for proving interesting security properties of real programs, particularly information flow control (IFC) security. Yet there remain no general logics for verifying IFC security of shared-memory concurrent programs. In this paper we present the first such logic, COVERN (Compositional Verification of Noninterference) and its proof of soundness via a new generic framework for general rely-guarantee IFC reasoning. We apply COVERN to model and verify the security-critical software functionality of the Cross Doma..

View full abstract


Funding Acknowledgements

We thank the anonymous reviewers for their valuable feedback and for convincing us not to name the logic COV-FEFE. This research was supported by the Commonwealth of Australia Defence Science and Technology Group and the Defence Science Institute, an initiative of the State Government of Victoria.