ProvenVisor for NXP Products

ProvenVisor is a formally proven hypervisor designed to help secure embedded devices based on application processors such as gateways, infotainement units, communication and mobile devices, etc. ProvenVisor provides security architects with an off-the-shelf certifiable foundation to build or reinforce the security of their solution, whether for new or existing devices. ProvenVisor is available for ARM Cortex-A microprocessors.

Why Use ProvenVisor

Hypervisors are useful solutions to a range of issues faced by embedded systems’ architects and designers: they make it possible to consolidate widely different OSs on a single chip, saving development time and reducing costs. However, using a hypervisor introduces additional security risks. 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. Prove & Run addresses this challenge with ProvenVisor, a proven, secure and certifiable hypervisor. ProvenVisor has been designed from the ground up to enforce strong security properties on its guest OSs and to keep full control over all situations that may occur in a complex embedded system. In addition, thanks to ProvenCore, Prove & Run’s secure OS kernel, 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.

Use Cases

ProvenVisor - UC1 ProvenVisor can execute multiple OSs on a single microprocessor, including an instance of ProvenCore, Prove & Run’s secure OS kernel
ProvenVisor can also leverage the TrustZone™ hardware security feature provided by ARM microprocessors

ProvenVisor At a Glance

  • Robust high security hypervisor using a microkernel architecture which enforces proven isolation (integrity and confidentiality) between OSs
  • Compatible with ARM applications processors such as the Cortex-A family
  • Optional ProvenCore support to create a security perimeter around the device and to enforce sophisticated security policies
  • Allows for time and cost controlled security certification processes even at the highest security levels, with easy maintenance
  • Support for multicore architectures, TrustZone™, and hardware virtualization extensions
  • Available under flexible licensing terms

Formally Proven Security

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. Modern embedded hypervisors (such as Xen) rely on a simple architecture where the kernel of the hypervisor handles basic tasks while more complex tasks are delegated to a “special” guest OS such as Linux. All of these components execute in “privileged mode” and have full control over the guest OSs. In that situation, a single security bug in the millions of lines of code that make up these components is enough to compromise the hypervisor. Instead, ProvenVisor uses a microkernel architecture, where the software components executing in “privileged mode” are as small as possible (usually less than ten thousand lines) while additional tasks execute in “non-privileged mode”. A security issue in one of these components cannot propagate itself to the other components. Furthermore, security-critical tasks are delegated to ProvenCore, which security has been verified. ProvenVisor has been completely modeled in Smart and proven using ProvenTools, Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always 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.


ProvenVisor is compatible with most NXP products based on ARM Cortex-A processors, including but not limited to the:

Professional Services

In addition to ready-made security COTS such as ProvenCore, ProvenCore-M and ProvenVisor, Prove & Run offers a range of professional services to:
  • Help our customers design/build/develop secure software and/or integrate our COTS,
  • Help our customers secure their existing architectures:
    • Performing security analyses
    • Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…
Print Print