Compositional Verification and Refinement of Noninterference
The COVERN Project
The COVERN project investigates methods to prove that concurrent programs do not leak sensitive information. It comprises a number of related activities. Each has the following in common:
Value-Dependent Classification: Supporting complex, real-world security policies requires being able to reason about programs in which the sensitivity of data is data-dependent.
Functional Correctness: Reasoning about value-dependent classification necessitates being able to also prove that the program in question is functionally correct.
Shared-Memory Concurrency: Concurrency is ubiquitous in modern programming. We tackle this challenge head on by adapting existing concurrent program verification methods to the task of reasoning about information flow security.
Proof Technique: Rely/Guarantee
- [Paper (EuroS&P 2018)]
First machine-checked proof of information flow security for a non-trivial concurrent program: a design model of the CDDC.
- [Paper (JFP Special Issue on Secure Compilation), DOI]
[Paper (ITP 2019), DOI]
COVERN Compiler: verified preservation of value-dependent, concurrent information flow security.
Proof Technique: Relaxed Separation Logic
- [Paper (OOPSLA 2021)]
[Paper (Extended Version]
Security Relaxed Separation Logic (SecRSL): a separation logic for precise reasoning about information flow security for C11 Release-Acquire weak-memory concurrency.
- First information-flow security definition for axiomatic weak-memory models.