ProvenCore: Towards a Verified Isolation Micro-Kernel

Conference object OPEN
Lescuyer, Stéphane (2015)
  • Related identifiers: doi: 10.5281/zenodo.47990
  • Subject: Separation Kernel, | Isolation | Formal Proof | Certification Toolchain

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.
  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    ZENODO 20 9
    Zenodo 20 9
Share - Bookmark

  • Download from
    ZENODO via ZENODO (Conference object, 2015)
  • Cite this publication