The Pip Protokernel

About Pip

Pip is a protokernel: it allows for kernels, ranging from hypervisors to monolithic kernels, to be developped as user mode applications. Pip only provides system calls for managing isolated partitions of the memory and basic dealing of control flow, thus reducing the trusted computing base to its bare minimum.

The logic of Pip is implemented in Gallina — the language of the Coq proof assistant — and it is in the process of being equipped with a formal proof that it ensures memory isolation. For efficiency, it is automatically translated into freestanding C code.

The architecture-dependent part of Pip is implemented in C and assembly language. It consists of a thin layer giving access to the hardware.

Get Pip

From a virtual machine image

The latest release of Pip's virtual machine image, which provides a ready-to-use development environment.

Virtual machine image (TAR.GZ) (SHA256SUM)

The login credentials are:

Login....: pip
Password.: pip
or
Login....: root
Password.: pip

From a Docker image

The latest release of Pip's Docker image, which provides a ready-to-use development environment.

Docker image (TAR.GZ) (SHA256SUM)

From sources

Pipcore

The latest release of Pip's source code, which contains the kernel, proof and documentation.

$ git clone https://github.com/2xs/pipcore.git

LibPip

The latest release of LibPip's source code, which provides useful functions for calling the API or managing the data structures of Pip.

$ git clone https://github.com/2xs/libpip.git

Partitions

ARMv7

Launcher

An example partition for Pip (ARMv7) showing how to boot a child partition with the Pip_Yield service:

Launcher partition (TAR.GZ) (SHA256SUM)

x86

Launcher

An example partition for Pip (x86) showing how to boot a child partition with the Pip_Yield service:

Launcher partition (TAR.GZ) (SHA256SUM)

Nanny busy beaver

An x86 partition to loosely test most of Pip's services:

Nanny busy beaver partition (TAR.GZ) (SHA256SUM)

Verified EDF scheduler

A formally verified x86 partition that schedules child partitions by following an EDF policy :

$ git clone https://github.com/2xs/pip-edf-scheduler.git

This partition also comes with a VM image with all the environment already set up. (README)(ZIP) (SHA256SUM)

Documentation

General documentation

Commented source code

Publications

Community

You can interact with Pip's developers and other users through the The Pip-club mailing list.

Events

June 16, 2019
The international workshop ENabling TRust through Os Proofs... and beYond (ENTROPY 2019) was held in Stockholm, Sweden.
December 7, 2018
The first Pip Club Meeting will be held at IRCICA, Villeneuve d'Ascq, France.
January 25-26, 2018
The international workshop ENabling TRust through Os Proofs... and beYond (ENTROPY 2018) was held in Villeneuve d'Ascq, France.

Support

This research project was partially funded by the European project ODSI.