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:


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:

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.



Contact

Toby Murray