Trusted products and services for embedded security. Join-us on Linkedin

ProvenVisor

A secure hypervisor for virtualization solutions

What is an hypervisor

A hypervisor is a software that emulates hardware systems and makes them available as “virtual machines” (VMs). As hypervisors can usually execute several VMs in parallel, they allocate CPU time and memory to the VMs. Hypervisors sometimes provide for inter-VM communication, either by emulating traditional communication peripherals or by implementing their own interface. 

Hypervisors are often used by embedded system’s architects and designers as they make it possible to consolidate widely different guest OSs (running on the different VMs) on a single chip, saving development time and reducing costs.  

Hypervisor’s security is critical

However, using a hypervisor introduces security risks since a hypervisor has full control over all the resources of an embedded device (CPU, memory, peripherals, etc.): a security issue inside the hypervisor would affect every OS it hosts. Therefore, the security and reliability of the hypervisor is paramount to the overall security of the whole device. 

Why ProvenVisor

ProvenRun addresses this challenge with ProvenVisor, a secure and certifiable hypervisor that security architects can use as an off-the-shelf certifiable component for their connected device’s TCB:

  • ProvenVisor executes directly on the bare metal (i.e. a type-1 hypervisor), making it possible to run multiple, unmodified OSs on a single hardware platform. 
  • ProvenVisor has been designed from the ground up to enforce strong security properties on its guest OSs, keeping full control over all situations that may occur in a complex embedded system. 
  • Leveraging on deductive formal methods, ProvenVisor insures that the guest OSs will retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.
  • In addition, thanks to ProvenCore, ProvenRun’s ultra-secure OS, ProvenVisor can enforce sophisticated security policies on its guest OSs, such as filtering all incoming and outgoing communications, and create an-in depth defense system around the guest OSs. 

Hypervisors and security

While ProvenVisor provides maximum guarantees on the enforcement of security policies of its guest OSs, there subsists a misconception among security professionals that hypervisors, even as secure as ProvenVisor, allow to do without secure OSs. 

Hypervisors do not provide the high-level abstractions that secure OSs do but only expose interfaces that are as complex as the hardware they are emulating. Security functions still need secure OSs to run on, even when hypervisors are used. Indeed the best a secure hypervisor can do is to isolate VMs as if they were running on physically distinct processors, but this doesn’t solve the main security problem that comes from the need of VMs or processors to communicate. 

This is why we recommend using ProvenCore, our secure OS in combination of ProvenVisor in order to provide maximum security guarantees for connected devices TCBs.

Supported hardware

ProvenVisor is available for ARM Cortex-A microprocessors compatible with the ARMv8-A architecture.

Please Contact us for more details

Challenge coverage

Security-by-design

Security-by-design

Security needs to be integrated at the design stage (security-by-design) and embedded in the most effective way wherever it is required in the technical infrastructure. There are many ways to embed security in systems and devices and the selected solution will be the result of a trade-off between cost, security level and performance.

More info
Trusted Computing Base

Trusted Computing Base

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. In order to limit the risk of vulnerabilities, the TCB need to be well identified, as small as possible and made-up of components that can be really trusted.

More info

Other Secure Components