ProvenCore stands at the core of ProvenRun’s offering of Trusted Computing Base (TCB) secure components.
Hosting the security critical services
The TCB always includes critical security services that need to remain small and simple to remain verifiable, especially on complex hardware such as modern microprocessors or microcontrollers. Implementing these security functions require high-level abstractions of the hardware, typically provided by an Operating System (OS). Because the correctness of the security functions depends on the correctness of these high-level abstractions, the OS that implements them is also part of the TCB and should be free from exploitable vulnerabilities.
The implementation of a secure OS is inevitably complex, traditional software development methods systematically fall short of eliminating vulnerabilities that are exploitable by attackers ready to invest a few million dollars. Such investments may seem high, but they are in fact extremely attractive in IoT or CPS settings when put in perspective with the number of devices that can be attacked at the same time, and the damage that can be done by devices that control physical systems. The secure OS needs to be of the highest software quality as possible and be as close as possible to zero defect. To meet that goal, the only available strategy to date is to develop the OS using deductive formal methods.
Why ProvenCore
ProvenCore is an ultra secure OS developed using deductive formal methods. It is a key milestone for being able to develop secure-by-design connected devices in many sectors (automotive, railways, aeronautics, energy, industrial, medical, etc.) in a cost-effective way:
A Secure OS is always required
Even when using other security technologies such as Secure Elements or hypervisors, an OS is still required to execute the sensitive security services on complex hardware such as microcontrollers or microprocessors, and this OS has to be secure because it is part of a device’s TCB.
Formally proven
ProvenCore is the very first OS to be formally proven for its complete TCB. This is essential to avoid situations in which hackers will exploit weaknesses in the part of the OS’s TCB that has not been formally proven.
High level API
ProvenCore offers a high abstraction level (POSIX-like) to developers of security services. With ProvenCore, the development of security services becomes simpler and cheaper, leading to more security at a lower cost.
More security, lower cost
ProvenCore is formally proven and can therefore claim superior code quality (as close as possible to zero-defects) leaving almost no attack surface to hackers. Use of formal proofs also promotes a much easier maintainability of the ProvenCore code base, a critical factor for a software component as complex as an OS, and consequently a much-reduced Total Cost of Ownership.
Certification
For industries that are subject to certification – or that may be subject to certification in the coming years – ProvenCore brings certainty that certification will be achieved painlessly, whatever the requirement level, for the lowest possible cost.
Certification
ProvenCore has received a Common Criteria EAL7 certification which is the highest level defined by the Common Criteria certification scheme.
Certification kits are available with ProvenCore.
Supported hardware
ProvenCore is available for ARM Cortex-A and RISC-V microprocessors.
Please contact us for more details.
