BedRock HyperVisor™

Not all hypervisors are created equal, and at BedRock the focus was to build a Formally Secured Computing base for virtualizing mixed criticality workloads in the demanding critical infrastructure, where safety and security are mandatory, and where failure is not an acceptable state.

The BedRock HyperVisor™ (BHV™) blocks lateral movement of threats and eliminates the attack surface with a formally secured computing. The BHV™ is a virtualization TCB. Thanks to BedRock Active Security™, even unmodified operating systems and applications can be protected against attacks.

BHV™ supports workloads being unmodified guests, containers and services. Traditionally applications are vulnerable to attacks. By consolidating these workloads on top of BHV™ not only the benefits of SWaP-C* are a significant benefit, but also the fact that lateral movements are impossible thanks to the formally proven Bare Metal Property™, but also the BedRocked™ applications can be locked down, monitored and made cyber resilient with deep semantic introspection and policy.

BedRocking™ operating systems, services, containers and applications is saving costs, adds agility and creates cyber resilient systems from existing assets in a software defined architecture.

If you are interested in partnering with 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™

Built on a capability-based microkernel, resources are not being created for general consumption, but are locked down by default only for consumption by specific targets that are being assigned dedicated “capabilities” to operate a resource. Think of a resource, a “door”. In common architectures every attacker that would gain access of that resource would be seeing this “door” and be able to open/close/operate it. In a capability-based system the attacker would still only see a “wall”, with no ability to see or operate the resource. This is a fundamental design time decision BHV™ builds on and enables the architecture to build in the Defense In Depth architecture that is unique among commercial offerings.

Defense in Depth

As part of the BedRock Zero Trust Design™, the whole BHV™ architecture is built on the paradigm of defense in depth, assuming that even if one layer of defense would break, the next layer of security would catch the fallout. As an example, even though BHV™ is being formally verified for the Bare Metal Property™, guaranteeing that no lateral movement of threats is possible, every Virtual Machine or Guest (VM) has a dedicated Virtual Machine Monitor (VMM) serving as the hardware abstraction layer to the guest, and provides multiple benefits. From stronger defense against microarchitecture-based side channel attacks to maximum information assurance in a multi-tenant world where essential forensic data and telemetries must not be a source of security concerns.

Standards Based

To enable a smooth transition for brownfield and greenfield approaches to virtualization, adoption of known standards is key. BHV™ supports VirtIO for device drivers in the guest workloads and has a built-in virtual switch making it easy for network administrators to integrate and manage virtual appliances. This enables customer both to transform existing applications, even on the existing supported hardware, into a segregated secure by design system, without forcing the operator and designers to adopt to new interfaces or proprietary protocols.

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.

Greenfield and Software Defined Architectures

The pressure for lower CAPEX, OPEX, the irreversible move to software-based value proposition, and the need to leverage the scalability of modern standards-based commodity hardware did driver many industries to Software Defined Architectures first, and to cloud native where possible, later. With this being the standard now in many industries such as Telecom, and the key driver for change in others such as Industrial Control and Process, the missing link is a virtualization platform that combines the benefits of Software Defined and Consolidation with the guarantees needed for Functional Safety and Security. BedRocks tools based Formal Verification Automation process is the disruptive method to bring the guarantees needed for critical infrastructure to the agile world of Software Defined.

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, eliminating human error. Rather than trusting that code is free of any defects, we prove its correctness based on a formal model of the hardware it runs on. The proof justifies the trust in the code, transferring it into the trust of a much smaller model. Constructing the proof 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 to build and maintain formal proofs. This enables software agility without fear of introducing bugs and human error in the process.

Bare Metal Property™

The Bare Metal Property™ is the formally verified guarantee that every guest running on a Virtual Machine Monitor (VMM) is adhering to the same limits as running bare metal (directly on a physical asset). Meaning, that an action that could not happen on the bare metal device, can also not happen running on BHV™. As a device A connected to a hardware Switch to a device B could never read or write the others device memory, it can also not happen on the virtualized system. This is how our mathematical proof is built to guarantee that lateral movement of threats is blocked, as if the guest VMs would still be running on discrete hardware.

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

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.

BedRock HyperVisor™

Zero Trust Design™

Defense in Depth

Standards Based

Unmodified Guest OS & Applications

Brownfield and Modernization

Greenfield and Software Defined Architectures

Formal Verification

Bare Metal Property™

No Vendor Lock-In

Formal Verification

Minimal Attack Surface

Security

Unmodified Guest OS & Applications

No Vendor Lock-In

KEY BENEFITS & VALUE PROP OF BEDROCK’S SECURE TCB

Connect