Overview

This repository contains the proof-of-concept developed for Milestone 1.2 of the IPCEI-CIS project, corresponding to WP2.1: horizontal abstraction of isolation services. Its purpose is to explore how isolation mechanisms can be exposed through an abstract interface, allowing software components or applications to rely on formally specified isolation guarantees without depending directly on a single concrete implementation.

The code and specifications provided here are expected to define the core concepts of this horizontal abstraction, identify the minimal isolation services exposed by the interface, and prepare the connection with the Pip protokernel and its formally proven isolation properties. This milestone acts as an intermediate step between the state-of-the-art study of isolation services and the later extended proof-of-concept in which the abstraction will be attached more explicitly to Pip.

Project Status

Version: 1.0beta.

Code Structure

• README.md: project overview and usage notes.
• _CoqProject: Coq project configuration, exposing ./theories as PipAPI and expecting ../FreerDPS/theories as FreerDPS.
• theories/PipApi.v: abstract Pip-MPU API and FreerDPS contract.
• theories/IsolationProofs.v: isolation properties and preservation proofs.
• AUTHORS: author list.
• LICENSE: CeCILL-C license text.

Prerequisites

The prerequisite setup is still to be rationalized. Expected dependencies include:

• Coq 9.0.
• FreerDPS.
• Monae.
• Infotheo.
• MathComp.
• Hierarchy Builder.

Build / Check Instructions

The current expectation for this project to build is that FreerDPS is installed manually in a folder adjacent to this repository. Most of the libraries needed by FreerDPS can be installed via opam:

opam switch create . ocaml-base-compiler.4.14.2
eval $(opam env)
opam pin add coq 9.0.0
eval $(opam env)

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-hierarchy-builder coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable coq-mathcomp-classical coq-infotheo

However, FreerDPS requires a specific version of monae. The version currently known to work is this monae, which has to be manually installed and compiled. To do so, clone the repositories and run the following inside them:

eval $(opam env)
opam pin add .

Once these dependencies are installed, go inside the directory created by cloning FreerDPS and run the following:

coq_makefile -f _CoqProject -o Makefile 
make

The compilation process is then the same for this project:

coq_makefile -f _CoqProject -o Makefile

creates a makefile. When this is done, run make to compile the files. If compilation succeeds, all lemmas are proved !

The current _CoqProject file includes the theories directory, which contains both PipApi.v and IsolationProofs.v.

Reading the Specification

Start from theories/PipApi.v, then continue with theories/IsolationProofs.v. The recommended reading order is:

1. The PIP interface, which lists the abstract isolation services.
2. The witness state model, which describes partitions, memory blocks, rights, MPU mappings, sharing, kernels, and child partitions.
3. The pip_contract, which combines caller obligations, callee guarantees, and abstract state updates.
4. The isolation properties and preservation lemmas in theories/IsolationProofs.v.

Formalized and Proved Elements

The proof-of-concept formalizes:

• The abstract PIP interface for isolation services such as partition creation, memory-block splitting and merging, sharing, MPU mapping, and partition deletion.
• A witness state model for partitions, memory blocks, access rights, address ranges, MPU mappings, child sharing, kernels, and partition descriptors.
• A Hoare-style contract, pip_contract, describing caller obligations, callee guarantees, and abstract state updates for each service.
• Predicates and helper functions for accessible addresses, configuration addresses, used addresses, mapped addresses, partition isolation, and vertical sharing.

The current Coq development proves, under the assumptions stated in the source files:

• Kernel/data isolation from the absence of duplicate addresses.
• Partition isolation from the absence of duplicate addresses.
• Preservation of the set of used addresses across programs using the abstract PIP interface.
• Preservation of address and block-identifier uniqueness across such programs.
• Preservation of disjointness between kernel blocks and partition-descriptor blocks.
• Preservation of the vertical sharing property.

Project Context / Citation

This repository is part of the IPCEI-CIS work. It corresponds to Milestone 1.2 of WP2.1, focused on the horizontal abstraction of isolation services.

Authors

See AUTHORS.

Contributing

Please contact the authors before contributing to this proof-of-concept.

Known Issues / Limitations

• External dependencies are still managed manually.
• FreerDPS setup instructions are still TBD.
• Build and installation instructions need to be rationalized with the current Coq project layout.
• The dependency on an adjacent ../FreerDPS/theories checkout should be made more robust or documented with exact setup commands.

License

This project is distributed under the CeCILL-C Free Software License Agreement version 1.0 (SPDX-License-Identifier: CECILL-C), a French free software license for components comparable in intent to the GNU LGPL.

See LICENSE for the full license text.