This repository is home to the COVERN project.
This project currently includes the COVERN logic and the COVERN compiler.
The COVERN logic is a program logic for verifying information flow control (IFC) security of shared-memory concurrent programs.
Specifically, it allows verification of value-dependent noninterference for concurrent programs written in a generic imperative While language with locking primitives.
Furthermore, the verification that the COVERN logic enables is compositional in terms of the proof effort expended for each of the threads of the concurrent program.
This means that if you prove each of the threads of a concurrent program IFC secure using the COVERN logic, then the entire concurrent program is IFC secure.
The COVERN compiler aims to transform IFC secure shared-memory concurrent programs into assembly programs that are also verified to be IFC secure.
Currently, it supports compilation of concurrent programs written in the aforementioned While language, into a generic RISC-style assembly language with locking primitives, while yielding proofs that the output programs retain the compositional value-dependent noninterference property.
It is currently possible to use the COVERN compiler to compile programs verified IFC secure using a type system that was a precursor to the COVERN logic, but that lacked its support for proving shared data invariants.
Work is currently underway on merging the two streams of development to make it possible to compile programs verified IFC secure with the COVERN logic.
The COVERN project is written and verified in the Isabelle proof assistant. It currently runs on Isabelle version Isabelle2017.
COVERN stands for Compositional Verification and Refinement of Noninterference. The word "covern" is German and translates to the English verb "cover", as in "to cover a song".
Source and target languages
while-lang: A generic imperative While language with locking primitives.risc-lang: A generic RISC-style assembly language with locking primitives, inspired by the RISC language from Filippo Del Tedesco, David Sands, and Alejandro Russo. "Fault-Resilient Non-interference." Computer Security Foundations Symposium (CSF), 2016.
The COVERN logic
rg-sec: A generic rely-guarantee-based framework for compositional reasoning about value-dependent noninterference, of which the COVERN logic is an instantiation.logic: The COVERN logic and its soundness proof.
The COVERN compiler
Examples and test scripts
- For the COVERN logic:
examples/Example_CopyInv.thy: A simple example program demonstrating the COVERN logic in action, with a simple data invariant that the classification of the input variable remains equal to the classification of the output variable.examples/cddc/Example_CDDC_LockLanguage_OnePlaceBuf.thy: A three-component while-lang model of the Cross Domain Desktop Compositor (CDDC) demonstrating the COVERN logic in action, establishing and making use of the invariant that the security domain indicated as active by the video compositor hardware remains the same as the domain to which the Switch component delivers keyboard events.
- For the COVERN compiler:
test_examples.sh: Invokes Isabelle session builds for all examples.
Assuming that isabelle is in your path, executing the
following will cause everything to be built.
isabelle build -D . -v -b
You can also build just the
examples using the test_examples.sh script.
The COVERN project builds on prior work, most notably the following
Archive of Formal Proofs (AFP) entries:
The following people, listed in alphabetical order by surname,
have contributed to the COVERN project:
- Kai Engelhardt
- Toby Murray
- Edward Pierzchalski
- Robert Sison
The following research papers describe aspects of the COVERN project.
