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
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
- Florian Vanhems, Vlad Rusu, David Nowak, and Gilles Grimaud. Formal Correctness Proof for an EDF Scheduler Implementation. 28th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2022), Milano, Italy, May 4-6, 2022. DOI: 10.1109/RTAS54340.2022.00030 (Talk)(Slides)
- Florian Vanhems, Narjes Jomaa, Samuel Hym, and David Nowak. On the proof-oriented design of a context-switching service in the Pip protokernel. ENabling TRust through Os Proofs... and beYond - 2nd International Workshop, ENTROPY 2019, Stockholm, Sweden, June 16, 2019. Proceedings, June 2019.
- Quentin Bergougnoux, Gilles Grimaud, and Julien Cartigny. Porting the Pip proto-kernel's model to multi-core environments. The 16th IEEE International Conference on Dependable, Autonomic and Secure Computing (DASC 2018), August 2018, Athens, Greece. DOI: 10.1109/DASC/PiCom/DataCom/CyberSciTec.2018.00108
- Mahieddine Yaker, Gilles Grimaud, Julien Cartigny, Chrystel Gaber, Jean-Philippe Wary, Xiao Han, and Vicente Sanchez-Leighton. Ensuring IoT security with an architecture based on a separation kernel. The IEEE 6th International Conference on Future Internet of Things and Cloud (FiCloud 2018), August 2018, Barcelona, Spain. DOI: 10.1109/FiCloud.2018.00025
- Narjes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud, and Samuel Hym. Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base. 18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018), July 2018, Oxford, United Kingdom. Electronic Communications of the EASST Open Access Journal. Volume 76. DOI: 10.14279/tuj.eceasst.76.1080
- Paolo Torrini, David Nowak, Narjes Jomaa, and Mohamed Sami Cherif. Formalising Executable Specifications of Low-Level Systems. 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018), pp. 155-176, July 2018, Oxford, United Kingdom. DOI: 10.1007/978-3-030-03592-1_9
- Narjes Jomaa, David Nowak, Gilles Grimaud, and Samuel Hym. Formal proof of dynamic memory isolation based on MMU. Science of Computer Programming, Elsevier, pp. 76-92, September 2018, volume 162. DOI: 10.1016/j.scico.2017.06.012
- Narjes Jomaa, David Nowak, Gilles Grimaud, and Samuel Hym. Formal Proof of Dynamic Memory Isolation Based on MMU. 10th International Symposium on Theoretical Aspects of Software Engineering, IEEE Computer Society, pp. 73-80, July 2016, Shanghai, China. 2016. DOI: 10.1109/TASE.2016.28
Community
You can interact with Pip's developers and other users through the The Pip-club mailing list.
Events
- December 13, 2024
- The second Pip Club Meeting will be held at IRCICA, Villeneuve d'Ascq, France.
- 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 was 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.