Title :

Pip-MPU: Formal verification of an MPU-based separation kernel for constrained devices

Author(s) :

Dejon, Nicolas [Auteur]
Université de Lille
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]
Orange Labs [Caen]
Gaber, Chrystel [Auteur]
Orange Labs [Caen]
Grimaud, Gilles [Auteur]
Université de Lille
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]

Journal title :

International Journal of Embedded Systems and Applications

Pages :

1-21

Publisher :

AIRCC Publishing Corporation

Publication date :

2023

ISSN :

1839-5171

English keyword(s) :

constrained devices
MPU
Pip
secure systems
Separation Kernel
Formal Verification
Isolation Property

HAL domain(s) :

Informatique [cs]/Logique en informatique [cs.LO]
Informatique [cs]/Cryptographie et sécurité [cs.CR]
Informatique [cs]/Systèmes embarqués
Informatique [cs]/Système d'exploitation [cs.OS]

English abstract : [en]

Pip-MPU is a minimalist separation kernel for constrained devices (scarce memory and power resources). In this work, we demonstrate high-assurance of Pip-MPU’s isolation property through formal verification. Pip-MPU offers ...
Show more >Pip-MPU is a minimalist separation kernel for constrained devices (scarce memory and power resources). In this work, we demonstrate high-assurance of Pip-MPU’s isolation property through formal verification. Pip-MPU offers user-defined on-demand multiple isolation levels guarded by the Memory Protection Unit (MPU). Pip-MPU derives from the Pip protokernel, with a full code refactoring to adapt to the constrained environment and targets equivalent security properties. The proofs verify that the memory blocks loaded in the MPU adhere to the global partition tree model. We provide the basis of the MPU formalisation and the demonstration of the formal verification strategy on two representative kernel services. The publicly released proofs have been implemented and checked using the Coq Proof Assistant for three kernel services, representing around 10000 lines of proof. To our knowledge, this is the first formal verification of an MPU based separation kernel. The verification process helped discover a critical isolation-related bug.Show less >

Language :

Anglais

Popular science :

Non

ANR Project :

Tiny, PrivAte, Proved & isolaTed

Collections :

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

Source :

Harvested from HAL