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 in while-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 from while-lang to risc-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-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:
  • examples/cddc/Example_CDDC_WhileLockLanguage.thy: A two-component while-lang model of the CDDC demonstrating a type system (found in old-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-component while-lang CDDC model yielding risc-lang assembly 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.