Overview

HTTPS SSH

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

Examples and test scripts

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:

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.