BedRock HyperVisor™

Not all hypervisors are created equal, and at BedRock the focus is to build a Formally Secured Computing base for virtualizing mixed-criticality workloads in the demanding domain of critical infrastructure, where safety and security are mandatory and failure is unacceptable.

The BedRock Hypervisor™ (BHV™) is the future Trustworthy Compute Base (TCB) for virtualization. Using a Formally Secured Computing base, the BHV™ blocks the lateral movement of threats via VM escapes and eliminates attack surfaces. Thanks to BedRock Active Security™, the BHV™ can protect a variety of workloads – including unmodified guests, containers and services – against attacks.

BedRocking™ your workloads yields numerous benefits including: novel SWaPC optimizations; the elimination of lateral movements of threats via VM escapes (thanks to the (in-progress) proof that the BHV™ respects the Bare Metal Property™); and access to deep semantic introspection and policy, which ensures that applications can be locked down, monitored and made cyber resilient.

If you are interested in partnering with BedRock Systems and utilizing the BHV™ and Active Security™ for Orchestration, Device Management and Policy Management, please contact us to discuss how to enable and expand your customer base on BedRocked™ infrastructure.


Zero Trust Design™

Zero Trust builds on the paradigm of deny by default, allow by exception. This minimizes the attack surface to needed functionality, limiting the exposure.

BedRock is designed from ground up enforcing least privilege and least functionality.

In common architectures, giving a process access to a resource involves exposing the “door” which it is behind; a motivated attacker will find a way to get through that “door” and take control of the resource. In contrast, the BedRock Hypervisor™ (BHV™) utilizes a capability-based microkernel in order to mediate access to the underlying resources; even if a malicious process gains access, it will be left staring at a wall instead of a “door”. This is a fundamental design-time decision of the BHV™ which enables a Defense In Depth architecture that is unique among commercial offerings.

BedRock is also extending the least privilege and least functionality paradigm into the guest, container and application. Leveraging Active Security™, BedRock can use allow/deny policy on code, API calls, resources, processes, memory, and prevent access execution. By limiting the existing unmodified stack to specific functionality and behavior, the vulnerable workload is being limited to least functionality, without expensive redesign and complex rework.

Formal Verification

Building a foundation based on formal verification enables us to precisely define with a formal model what a system can do. This is then matched, through proofs, to the actual code implementing the model. If the proof can satisfy the model, the code is formally verified. Formal verification allows us to establish the correctness of a system to the same degree of confidence that you know that 1 + 1 = 2, eliminating human error. In other words, we have mathematical proof of the BedRock Hypervisor’s effectiveness. At BedRock we are building formal verification at scale by investing in automation.

Minimal Attack Surface

The BedRock Hypervisor combines the best concepts from microkernels, capability-based systems, and modular design for superior performance, security, and isolation. Because it enforces the principle of least authority, BedRock is able to guarantee that most attacks are not possible to begin with. Our secure architecture keeps all critical functions, including Active Security and Policy Enforcement, below the OS-reachable attack surface, thereby fully protecting the OS and its applications.


BedRock Security is enabled without a cooperating operating system or application, eliminating the attack surface of the components. Based on formal verification, the capability-based system ensures resources can only be accessed when explicitly enabled. With this level of security embedded into the BedRock Hypervisor, users can run the software stack from the OS and up without modification beyond their life cycle, while still preventing attacks.

Unmodified Guest OS & Applications

The BedRock Hypervisor is designed to run unmodified guest operating systems without the need to recompile the kernel or any application. Powered by formal methods, the Hypervisor cannot be breached, and, therefore, is not part of the attack vector. The fundamental hardware abstraction layer can leverage hardware features while concealing them from the OS, increasing system security.


No Vendor Lock-In

The BedRock Hypervisor includes a business-friendly open source license. This prevents vendor lock-in, provides freedom of choice, and prohibits intellectual property contamination. Rather than create a dependency, BedRock Systems is committed to community-driven projects and collaboration.


Interact With Us

Contact Us ›

Give us a call or fill out our contact form.

Partners ›

Apply to become a partner with BedRock.

Resources ›

Learn how BedRock's technology can benefit your business.