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:


COVERN-RG

Proof Technique: Rely/Guarantee

Property Proved: Noninterference

Outcomes:

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.

Contact

Toby Murray