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