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 SWaP–C 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.







Defined Architectures



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.
Active Defense in Depth
As part of the BedRock Zero Trust Design™, the whole BHV™ architecture is built on the paradigm of Active Defense in Depth, assuming that even if one layer of defense is penetrated the next layer would catch the fallout. As an example, even though the BHV™ is being formally verified to establish the Bare Metal Property™ – guaranteeing that no lateral movement of threats via VM escapes is possible – every Virtual Machine or Guest has a dedicated Virtual Machine Monitor (VMM) serving as the hardware abstraction layer. Per-guest VMMs enable stronger defense against microarchitecture-based side channel attacks and provide higher information assurance in a multi-tenant world where essential forensic data and telemetries must not be a source of security concerns.
Guest VMs that communicate with each other, can do so through the BedRock Virtual Switch that is part of the formally secure virtualization stack. Active Defense in Depth means that Active Security™ policy will actively constrain the communication to its designed and enforced pattern, actively preventing misbehavior and risky communication.
Standards Based
To enable a smooth transition for brownfield and greenfield approaches to virtualization, adoption of known standards is key. The BedRock Hypervisor™ (BHV™) supports VirtIO for device drivers in guest workloads and has a built-in virtual switch making it easy for network administrators to integrate and manage virtual appliances. This enables customers to transform existing applications – even on existing supported hardware – into a segregated secure by design system, without forcing the operator and designers to adopt to new interfaces or proprietary protocols.
Novel SWaP-C Optimizations
When optimizing Size, Weight, Power and Cost, physical separation is replaced with virtualization. With traditional hypervisor offerings, security is naturally being sacrificed. However, for certain sectors within Government, Enterprise and Defense, security, and sometimes safety, are of paramount concern which means that standard SWaP–C optimizations cannot be utilized. BedRock is becoming a key player in driving down SWaP–C for its customers and partners by enabling them to securely and transparently consolidate their physical assets.
The BedRock HyperVisor™ (BHV™) provides secure virtualization based on the Bare Metal Property™ and even increases the level of possible security by leveraging BedRock Active Security™– which not only eliminates the lateral movement of threats via VM escapes, but also allows to enforce least privilege and least functionality inside the guest, from within the HyperVisor. For example, a user which currently utilizes 3 desktops/workstations in order to segregate a variety of privileged and unprivileged information can transition to a single BedRocked™ workstation, providing clear benefits in terms of Size, Weight, Power and Cost, while also increasing the level of isolation – and thus the security – of the overall system.
Unmodified Guest OS & Applications
The BedRock Hypervisor™ (BHV™) is designed to run unmodified guest operating systems, applications and containers, without the need to recompile the kernel or any application. Powered by formal methods, a fully verified BHV™ cannot be breached, and, therefore, is not part of the attack vector. Furthermore, the fundamental hardware abstraction layer leverages hardware (security) features, enabling them for the upstream OS and application, while concealing them from the OS, increasing system security.
Brownfield and Modernization
Existing legacy applications and appliances have seen huge investment and adoption. With modernization and security driving change, the Bedrocking™ approach allows you to migrate to a new Zero Trust Design™ with minimum effort and risk. The ability to virtualize unmodified workloads enables state of the art security for existing assets. This is key to retaining existing investments and BedRocking™ them without costly – and sometimes impossible – redesign and redevelopment.
Greenfield and Software Defined Architectures
The pressure for lower CAPEX and OPEX, the irreversible move to software-based value propositions, and the need to leverage the scalability of modern standards-based commodity hardware drove many industries to Software Defined Architectures first, and then – if possible – to Cloud Native Architectures. Currently these are the standard in many industries such as Telecom, and they are key drivers for change in others such as Industrial Control and Process. However, these approaches struggle to provide the necessary Functional Safety and Security guarantees. BedRock’s tools-based Formal Verification process is crucial to bringing the foundational guarantees needed for critical infrastructure to the agile world of Software Defined Architecture.
Formal Verification
Formal verification allows us to establish the correctness of a system to the same degree of confidence that you know that 1 + 1 = 2. Rather than trusting that code is correct, we prove it correct; the proof justifies the trust in the code, transferring it into the trust of a much smaller model.
Constructing these proofs at the scale of modern software is a monumental task. To make this tractable, BedRock Systems is investing in automation to reduce the manual effort required to build and maintain formal proofs. This approach enables software agility without fear of introducing bugs and human error in the process.
Bare Metal Property™
Virtualization stacks which exhibit the Bare Metal Property™ guarantee that every running guest behaves as if it were running directly on a physical asset. This means that an action that could not happen on the device could also not happen running in the virtualized environment. At BedRock, we are developing mathematical proofs which show that the BedRock Hypervisor™ (BHV™) adheres to the Bare Metal Property™ and thus that lateral movement of threats through VM escapes are blocked.
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.
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.
Security
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.
KEY BENEFITS OF BEDROCK’S SECURE TCB
