Implementing 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 should be free from exploitable vulnerabilities.
ProvenRun has developed ProvenCore, a formally proven ultra secure OS/TEE to answer this challenge. 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. ProvenCore uses deductive formal methods to :
- provide superior quality code (as close as possible to zero defects)
- with the right abstraction level in the form of high level APIs
- with security properties that can be formally verified and eventually certified at affordable cost.
ProvenCore has received a Common Criteria EAL7 certification which is the highest level defined by the Common Criteria certification scheme.