Title :

pipcore-mpu

Author(s) :

Amara, Damien [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Bergougnoux, Quentin [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Cartigny, Julien [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Dejon, Nicolas [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Grimaud, Gilles []
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Hauspie, Michaël [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Lafont, Étienne Helluy [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Hym, Samuel [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Jomaa, Narjes [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Soyez-Martin, Claire [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Torrini, Paolo [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Vanhems, Florian [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Yaker, Mahieddine [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]

English keyword(s) :

Computer Science
Provable Security
Security
Formal Methods
Operating System
Internet of Things
IoT
Embedded system

HAL domain(s) :

Informatique [cs]

English abstract : [en]

Pip-MPU is a project implementing the protokernel Pip on ARM Cortex-M devices having a Memory Protection Unit (MPU).Pip is a protokernel: it allows for kernels, ranging from hypervisors to monolithic kernels, to be developped ...
Show more >Pip-MPU is a project implementing the protokernel Pip on ARM Cortex-M devices having a Memory Protection Unit (MPU).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.Show less >

Language :

Anglais

ANR Project :

Tiny, PrivAte, Proved & isolaTed

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL