Titre :

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

Auteur(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]

Titre de la revue :

International Journal of Embedded Systems and Applications

Pagination :

1-21

Éditeur :

AIRCC Publishing Corporation

Date de publication :

2023

ISSN :

1839-5171

Mot(s)-clé(s) en anglais :

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

Discipline(s) HAL :

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]

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Vulgarisation :

Non

Projet ANR :

Tiny, PrivAte, Proved & isolaTed

Collections :

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

Source :

Harvested from HAL