Compositional Verification and Refinement of Noninterference
The COVERN Project
The COVERN project investigates methods to prove that practical programs are secure, in the sense that they don't leak information that they are not supposed to. It comprises a number of related activities. They each deal with many of the following themes:
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.
Verdeca
Proof Technique: Separation Logic
Property Proved: Secure Declassification
Outcomes:
- [Paper (CCS 2023, Extended Version)]
Verified secure declassification for concurrent C programs. - Auto-active proofs of secure declassification for real-world concurrent programs.
Insecurity Logic
Proof Technique: Separation Logic
Property Proved: Violations of Noninterference
Outcomes:
- [Paper (ICFEM 2023, Extended Version)]
Insecurity Separation Logic: an under-approximate relational separation logic for proving when programs leak information. - Underflow and Pulse-InsecSL: tools for automated detection of information leaks in programs.
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.
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.