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 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.
ProvenCore-M is compatible with most NXP products based on ARM Cortex-M microcontrollers, including but not limited to the:
In addition to ready-made security COTS such as ProvenCore 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…