Security engineers define the Trusted Computing Base (TCB) as the set of hardware, firmware and software components that are critical to the security of a system.
With the advent of the Internet of Things (IoT) and deployment of Cyber Physical Systems (CPS) in the automotive, railway, aeronautic, energy, industrial, medical and defense sectors (among others), the Trusted Computing Base (TCB) of connected devices involved in connected architectures and their surface of attack become much wider than for mobile telephony. Devices to secure are indeed more diverse than “just” mobile phones: instead they handle a larger number of various peripherals to be secured. They also include large and complex software stacks, with rich Operating Systems (OSs) and kernels, some of which are essential to security.
In addition, connected devices create new situations where assets that need to be protected are not just virtual, but also physical: goods, infrastructures, lives, etc. The effects of large-scale attacks are no longer limited to tampering with crucial data or creating improper transactions (issues which can usually be avoided or traced back with proper risk management processes), but could also potentially include irremediable physical destruction. The prospects and business model for attackers become much more attractive. In many cases the risk for services and industries may become incommensurate.
Keep it small and simple principle
It is therefore quite essential to design architectures that rely on TCBs that are as small and simple as possible.
The TCB always includes critical security functions 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.
Secure OS must be as close as possible to zero defects
As 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.
This is why we have developed at ProvenRun products such as a secure OS called ProvenCore as well as a secure hypervisor called ProvenVisor. In both cases, the objective is to use deductive formal methods to provide:
Superior quality software
As close as possible to zero-defect
High level API
The right abstraction level for writing simple security functions
Key security properties
That can be formally verified and eventually certified at affordable costs
Up to the highest security level at industrial cost
In effect, traditional Secure OS and hypervisors solutions available on the industrial market or for mobile telephony fall short on meeting the requirements for building TCB that is fitted to the industrial requirements of IoT or CPS settings. With ProvenCore and ProvenVisor, we are filling that technology gap by providing off-the-shelf TCB components (COTS) that can be used by security engineers and security architects to reach a higher level of security while reducing the total costs of security when securing-by-design their products.
With ProvenCore in particular, that has received a Common Criteria EAL7 certification which is the highest level defined by the Common Criteria certification scheme, we answer to the main and most critical problem for building TCBs that can be really trusted in a cost-effective way.
