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
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.