ProvenCore-M is a formally proven secure operating system for embedded devices designed from the ground up, to enforce strong security properties on processes, and to keep full control on all deadlocks and Denial of Services (DoS) situations, that may occur in a complex system. ProvenCore-M uses a microkernel architecture implemented using formally proven code to get as close as possible to zero defects, to guarantee the expected security properties, and to ease the path to any required certifications. This architecture and these formal proofs also improve the sustainability of the maintenance process of the systems based on ProvenCore-M.
ProvenCore-M insures proven isolation between concurrent processes. This is much required for projects where some components of the software stack may not be fully trusted (3rd-party drivers, etc), when the stack is a merge of complex existing software components, when de-facto security properties need to be guaranteed due to the code complexity, or when they required a security assurance level. ProvenCore is usable on its own or as a low-level layer to support existing operating systems or applications.
ProvenCore-M is available for STM32 Arm® Cortex®-M0/M3/M4/M7 microcontrollers.
Key Features:
- Robust high security microkernel architecture, which enforces proven isolation (integrity and confidentiality) between processes, both on code and on data
- Support of optional security services (IP firewall, remote management and updates, etc)
- Time and cost controlled security certification processes even at the highest security levels, with easy maintenance
- Preemptive, deterministic, multitasking scheduler
- Handles interruptions in bounded time
- Supports the CMSIS HAL: most existing drivers can be easily adapted
- Memory requirements: Static microkernel data: 17 Kbytes of Flash memory and 3 Kbytes of RAM
- Per application: 200 Bytes of Flash memory and 350 Bytes of RAM
- Support of STM32 Arm® Cortex® -M0/M3/M4/M7 microcontrollers
