ProvenRun, a leader in embedded security, announces that its flagship product, ProvenCore for ARM™ Cortex-A, has recently obtained a Common Criteria (CC) EAL7 certification. This is a world premiere as there is no other OS or Trusted Execution Environment (TEE) at that level of security. As a comparison, the next most secure TEE on the mobile security market – for the very few that have been certified – only reached the EAL2+ level. 

ProvenCore is a formally proven secure OS for ARM Cortex-A, ARM Cortex-M and RISC-V processors. It is also a next-generation ultra-secure TEE. Receiving a CC EAL7 certification for ProvenCore showcases the unique security expertise of ProvenRun’s team for delivering highly secure software components such as OSs and hypervisors. EAL7 is the highest level defined by the Common Criteria certification scheme and offers an extremely important increase in security assurance compared to EAL2+. Providing such a high level is a must when willing to withstand remote cyberattacks for devices whose massive compromise would lead to high losses.

It is also a key milestone for being able to develop secure-by-design connected devices in many IoT sectors (automotive, railways, aeronautics, energy, industrial, medical, etc.) in a cost-effective way:

• 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 Trusted Computing Base. 
• ProvenCore is the very first OS or kernel to be formally proven for its complete Trusted Computing Base. Formally proving the complete Trusted Computing Base is essential to avoiding situations in which hackers will exploit weaknesses in the part of the Trusted Computing Base that has not been formally proven, and that can still be complex and error prone such as the Process Management for example. 
• 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.
• 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 (TCO).  
• 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.

A copy of the certificate is available.

Dominique Bolignano, President and Founder of ProvenRun: “ProvenCore is the first OS/TEE to be formally proven down to the generated code. The proof also covers all of the essential parts of the OS/TEE as ProvenCore’s Trusted Computing Base is also proven. Those are two world premieres and we are extremely proud to have achieved this outstanding milestone. With ProvenCore, ProvenRun brings to the market a solution that provides a distinctively higher security level and a lower cost of security than any existing solutions for connected and mobile devices.”