Overview
Atlassian Sourcetree is a free Git and Mercurial client for Windows.
Atlassian Sourcetree is a free Git and Mercurial client for Mac.
COVERN
This repository is home to the COVERN project.
This project currently includes the COVERN logic and the COVERN compiler.
The COVERN Logic
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
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.
About COVERN
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".
Repository contents
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
old-rg-sec: An earlier rely-guarantee-based framework for compositional reasoning about value-dependent noninterference (based on that of Dependent_SIFUM_Type_Systems).old-type-system: A type system for compositional verification of value-dependent noninterference for programs written inwhile-lang(based on that of Dependent_SIFUM_Type_Systems, with support for locking primitives added), and its soundness proof.refinement: A framework for compositional proofs of refinement of value-dependent noninterference (based on that of Dependent_SIFUM_Refinement).wr-compiler: The COVERN compiler fromwhile-langtorisc-lang, and a proof that it produces programs that retain value-dependent noninterference.
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-componentwhile-langmodel 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:
examples/cddc/Example_CDDC_WhileLockLanguage.thy: A two-componentwhile-langmodel of the CDDC demonstrating a type system (found inold-type-system) that was a precursor to the COVERN logic.examples/cddc/Example_CDDC_RISCLanguage.thy: An invocation of the COVERN compiler on the two-componentwhile-langCDDC model yieldingrisc-langassembly artifacts of the same model, and proofs that they constitute an IFC secure concurrent program.
test_examples.sh: Invokes Isabelle session builds for all examples.
Building
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.
Contributors
The COVERN project builds on prior work, most notably the following Archive of Formal Proofs (AFP) entries:
- Dependent_SIFUM_Type_Systems by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
- Dependent_SIFUM_Refinement by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
The following people, listed in alphabetical order by surname, have contributed to the COVERN project:
- Kai Engelhardt
- Toby Murray
- Edward Pierzchalski
- Robert Sison
Research Papers
The following research papers describe aspects of the COVERN project.
- Toby Murray, Robert Sison and Kai Engelhardt. "COVERN: A Logic for Compositional Verification of Information Flow Control". In IEEE European Symposium on Security and Privacy (EuroS&P), 2018. To appear.