Logical Relations for Termination-Insensitive Noninterference

A mechanized logical relations model for an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. The semantic model of the type system can be used to show that well-typed programs satisfy termination-insensitive noninterference but also to show that composing syntactically well-typed and syntactically ill-typed---but semantically sound---components is secure.

The model is defined using the Iris program logic framework. To capture termination-insensitivity, we make us of our theory of Modal Weakest Precondition. We formalize all of our theory and examples on top of the Iris program logic framework in the Coq proof assistant.

This development accompanies the paper Mechanized Logical Relations for Termination-Insensitive Noninterference published at POPL 2021.

Building the theory

The project can be built locally or by using the provided Dockerfile, see the Using Docker section for details on the latter. The development uses modal-weakestpre as a git submodule; remember to run

git submodule update --init --recursive

after cloning the repository to initialize it. Alternatively, you can clone the repository using the --recurse-submodules flag.

Prerequisites

The project is known to compile with:

• Coq 8.13.0
• Iris 3.4.0
• std++ 1.5.0
• Autosubst 1

The dependencies can be obtained using opam

1. Install opam

2. To obtain the dependencies, you have to add the following repositories to the registry by invoking

    opam repo add coq-released https://coq.inria.fr/opam/released
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
    opam update
   

3. Run make build-dep to install the right versions of the dependencies.

Building

Run make -jN to build the full development, where N is the number of CPU cores on your machine.

Using Docker

The development can be built using Docker.

1. Install Docker
2. Run make docker-build to build the Docker image Dockerfile that compiles the development.
3. Optionally, you can execute docker run -i -t iris-tini to get an interactive shell.

Documentation

Documentation can be generated using coqdoc by running make html. doc.html provides an entry and overview of the generated documentation.

Source organization

Language and semantic model

• theories/lambda_sec/lattice.v: theory of join semilattices, including the induced lattice ordering
• theories/lambda_sec/lang.v: the language and operational semantics
• theories/lambda_sec/types.v: syntactic types, substitution principles, and syntactic flows-to relation
• theories/lambda_sec/notation.v: notation for writing programs and types
• theories/lambda_sec/typing.v: subtyping and typing relation
• theories/lambda_sec/rules_unary.v: unary language lemmas
• theories/lambda_sec/logrel_unary.v: unary logical relation
• theories/lambda_sec/fundamental_unary.v: unary fundamental theorem of logical relations
• theories/lambda_sec/rules_binary.v: binary language lemmas
• theories/lambda_sec/logrel_binary.v: binary logical relation
• theories/lambda_sec/fundamental_binary.v: binary fundamental theorem of logical relations
• theories/lambda_sec/noninterference.v: noninterference statement and proof, both for a generic lattice and a two-point lattice

Modal Weakest Precondition Theory

Below we highlight the parts of the modal weakest precondition theory that is relevant for this development.

• modal-weakestpre/theories/mwp.v: definition of the generic modal weakest precondition
• modal-weakestpre/theories/mwp_adequacy.v: adequacy theorem of the generic modal weakest precondition
• modal-weakestpre/theories/mwp_triple.v: a Hoare-triple definition for modal weakest precondition
• modal-weakestpre/theories/mwp_modalities/mwp_step_fupd.v: step-taking update modality MWP instance used for the unary relation
• modal-weakestpre/theories/mwp_modalities/mwp_fupd.v: update modality MWP instance
• modal-weakestpre/theories/mwp_modalities/ni_logrel/mwp_right.v: inner MWP instance for the binary relation
• modal-weakestpre/theories/mwp_modalities/ni_logrel/mwp_left.v: binary MWP instance for the binary relation
• modal-weakestpre/theories/mwp_modalities/ni_logrel/ni_logrel_lemmas.v: lemmas for the interaction between the step-taking update modality instance (unary) and the binary MWP instance
• modal-weakestpre/theories/mwp_modalities/ni_logrel/mwp_logrel_fupd.v: binary MWP instance used for the theories/examples/refs.v and theories/examples/refs_implicit.v example that allows invariants to be kept open for the full execution

Examples

The theories/examples folder includes multiple case studies, among others, about value dependency, the awkward example, and parametricity.