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.