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.
COVERN-RG
Proof Technique: Rely/Guarantee
Property Proved: Noninterference
Outcomes:
- [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.
VERONICA
Proof Technique: Owicki-Gries
Property Proved: Secure Declassification
Outcomes:
- [Paper (CSF 2020)]
Precise reasoning about expressive declassification policies in concurrent programs for the first time. - Ability to reason about various styles of declassification: e.g. delimited release, interactive, stateful.
SecC
Proof Technique: Separation Logic
Property Proved: Noninterference
Outcomes:
- [Paper (CAV 2019)]
Security Concurrent Separation Logic (SecCSL): a separation logic for precise reasoning about expressive security policies. - SecC: automatic verification of information flow security for C programs.
SecRSL
Proof Technique: Relaxed Separation Logic
Property Proved: Noninterference
Outcomes:
- [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.