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

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 (draft, ITP 2019)]
    COVERN Compiler: verified preservation of value-dependent, concurrent information flow security.

VERONICA

Proof Technique: Owicki-Gries

Outcomes:

  • [Paper (draft)]
    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

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.

Contact

Toby Murray