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.
- Hypervisors need to be secured in order to be used as part of any connected device Trusted Computing Base.
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