ProvenCore-M is a highly secure RTOS for ARM® Cortex®-M microcontrollers that enables the creation of secure IoT devices. Its architecture allows customers to target everything from small up to large-scale deployments, while staying focused on developing the functional part of their applications, and with no need for a deep expertise in security.
ProvenCore-M is available for most ARM Cortex-M microcontrollers. For ARM Cortex-A microprocessors, please inquire about our ProvenCore product.
Why Use ProvenCore-M
Embedded devices are increasingly facing cybersecurity issues originating from the lack of robustness of their software stacks, with hackers exploiting bugs and weaknesses, in particular of Operating Systems. On one hand, devices are more connected than ever, through a variety of communication links: deeply embedded devices are now just one hack away from the Internet. On the other hand, they are required to carry increasingly sensitive industrial operations, involving cyber-physical systems or dealing with confidential and/or personal data, performing payment transactions, creating or forwarding valuable data while safekeeping their authenticity, etc.
Prove & Run addresses these challenges with ProvenCore-M. ProvenCore-M has been designed from the ground up to securely isolate applications from each other, and to protect the stability of an IoT device at all times, with minimal impact on existing code. This RTOS uses a microkernel architecture implemented using formally proven code to get as close as possible to zero defects and to guarantee the expected security properties. Together, these attributes also ease the path toward any required certifications. In the end, ProvenCore-M removes the complexity of implementing reliable and secure embedded systems, even under constraints (complex code stack or architecture, high certification requirements, etc).
ProvenCore-M can be used as the main OS of a device based on an ARM Cortex-M chip, providing a strong foundation to the software architecture of the device. For example, third-party drivers that cannot be fully trusted can be isolated from more trustworthy components.
In a device that includes several processors, a single ARM Cortex-M core running ProvenCore-M can be dedicated to security and offer secure services to the other components of the device, in effect turning the ARM Cortex-M core into a security coprocessor. Potential use include:
- Secure Storage: Protecting sensitive data,
- Cryptographic processor: Storing keys and performing cryptographic operations,
- VPN Client: Forcing applications running on other processors to communicate with remote servers only through a secure VPN using specific certificates and options,
- Application Firewall: Filtering high-level commands and responses between two applications or between an application and a remote server.
ProvenCore-M can be configured with built-in security services, allowing customers to rely on Prove & Run’s strong security expertise:
- The Secure Boot service provides a strong root of trust to the device by guaranteeing the authenticity of ProvenCore-M and of all its applications upon each reset. The authenticity check uses embedded public key signature verification, and relies on hardware-specific mechanisms to protect associated root of trust elements.
- The Firmware Update service allows updating IoT device when they are in the field. The ProvenCore-M architecture guarantees that full control is kept under any circumstances on any update of applicative executable code, including buggy code or viruses in applications or drivers. The Firmware Update service also checks the authenticity of the updated code using a PKI, and guarantees an atomic update of the application.
Using ProvenCore-M with a Secure Element
For an even higher level of security and insurance, ProvenCore-M can be augmented with a Secure Element, a tamper-proof chip offering secure storage and a cryptographic coprocessor. A Secure Element is highly resistant to attacks (including high-potential physical ones) and is usually certified Common Criteria EAL5+, which guarantees that stored sensitive secrets are protected. Thanks to its unique architecture, ProvenCore-M retains exclusive control of the Secure Element, and is able to enforce strict rules on the applications that make use of the secrets stored inside the Secure Element.
ProvenCore-M At a Glance
- Robust high-security microkernel architecture, which enforces proven isolation (integrity and confidentiality) between applications, both on code and on data.
- Allows to strongly increase security and robustness of services on IoT devices (key management, remote update, TLS, etc).
- Preemptive, deterministic, multitasking scheduler, which handles interruptions in bounded time, and guarantees the stability of the system in any situation.
- Minimal constraints for supporting existing code: easy integration with CMSIS HAL (minor modifications for existing drivers).
- High confidence on developed product with time- and cost-controlled security certification processes, even at the highest security levels, with easy maintenance.
- Support for Secure Elements.
- Memory requirements:
- Static microkernel data: ~20KB of Flash and 3KB of RAM
- Per application: 256 bytes of Flash and 384 bytes of RAM
- Available under flexible licensing terms.
Formally Proven Security
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 insure the sustainability of the maintenance process of systems based on ProvenCore-M.
Most existing OS kernels for microcontrollers (uCLinux, FreeRTOS, etc) rely on a monolithic architecture where every component of the kernel executes in “privileged mode”: the scheduler, the memory manager but also all the drivers for the peripherals. Such kernels are therefore quite large, up to hundred of thousand lines of code. Any security bug in one of these components completely compromises the kernel. ProvenCore-M uses a microkernel architecture, where the software components executing in privileged mode are as small as possible (usually less than ten thousand lines), and additional components such as device drivers execute as conventional processes. A security issue in one of these components cannot propagate itself to the other components.
ProvenCore-M has been completely modeled in Smart and proven using ProvenTools, Prove & Run’s formal software development toolchain. This means that it is mathematically proven that processes running on ProvenCore-M will always retain their integrity (no other process can tamper with their internal data) and confidentiality (no other process can read their internal data). A misbehaving or malicious process has no practical way to modify a running process or to practically spy on another process.
In addition to ready-made security COTS such as ProvenCore, ProvenCore-M and ProvenVisor, Prove & Run offers a range of professional services to:
- Help our customers design/build/develop secure software and/or integrate our COTS,
- Help our customers secure their existing architectures:
- Performing security analyses
- Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…