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 the hardware.
You can download the latest alpha release of Pip from its Git repository:
git clone https://github.com/2xs/pipcore.git
You can interact with Pip's developers and other users through the The Pip-club mailing list.
This research project is partially funded by the European project ODSI.
|September 29, 2017||0.2|
|October 3, 2016||0.1|