publication . Conference object . Other literature type . 2015

ProvenCore: Towards a Verified Isolation Micro-Kernel

Lescuyer, Stéphane;
Open Access
  • Published: 20 Jan 2015
Abstract
We report on an ongoing project aiming at a fully secure micro-kernel named ProvenCore. This operating system is both developed and specified in a single specification language called Smart. The Smart models are used to generate efficient C code and express low- and high-level properties of the implementation, and first among them guarantees of integrity and confidentiality for the various processes running on the kernel. ProvenCore is designed to be used as a secure world operating system in mobile devices, beneath a professional application platform or a Trusted Execution Environment.
Persistent Identifiers
Subjects
free text keywords: Separation Kernel,, Isolation, Formal Proof, Certification Toolchain, Separation Kernel,, Isolation, Formal Proof, Certification Toolchain
Download fromView all 2 versions
Zenodo
Conference object . 2015
Provider: Datacite
Zenodo
Other literature type . 2015
Provider: Datacite
ZENODO
Conference object . 2015
Provider: ZENODO
Any information missing or wrong?Report an Issue