Why Formal Methods?

Why Formal Methods?

 By BedRock Systems Team

The Promise of Traditional Virtualization → 

Flexible Consolidation and Management

BedRock Systems is building a modern, microkernel-based hypervisor to serve as a foundation for trustworthy computing. The BedRock Hypervisor™ (BHV) enables extension by adding new applications without risking the integrity of the system as a whole. 

Virtualization is a crucial technology for the evolution of software systems. It enables running legacy software on modern hardware and facilitates the consolidation of fundamentally different components (e.g. those that rely on different operating systems) to build more integrated systems reducing size, weight, power, and cost (SWaP-C). Consolidation also provides additional flexibility by enabling dynamic reconfiguration of a system – something that, without virtualization, would require new hardware to be connected and configured.

Unfortunate Costs of Traditional Virtualization → Compromised Security & Resiliency

With standard virtualization there is an unfortunate cost to this capability. In physically separate systems, we can leverage physical laws to establish isolation, but when systems are consolidated we lose this reasoning principle. Without the isolation, it becomes easier for a failure in one component to compromise other components. This potential for “lateral movements” makes it possible for add-on features to compromise the integrity of the crucial components in the system. While faulty components can exist in any system, they are generally not malicious. However, as we have seen over the years, faulty components can be compromised when they become connected and compromised systems are (generally) malicious. With the higher bandwidth and larger attack surfaces provided and exposed by virtualization platforms, malicious components have a greater reach than they do in an environment based on physical isolation.

Breaking through this trade-off is possible.

To re-establish the security and isolation principles provided by physics without sacrificing the benefits of virtualization, we need a more flexible reasoning principle: one that allows controlled and configurable connectivity. At BedRock Systems, we are building the BedRock Hypervisor™ (BHV™), a virtual machine monitor that leverages mathematics to fill this gap. Formal methods (FM) enables us to give a more nuanced characterization of connectedness, describing not only that two components are connected, but also what communication is permitted. In the context of virtualization, independent virtual machines are both “connected” to the underlying hardware that they are running on and the virtualization layer establishes a logical isolation. For example, while two VMs both talk to the same RAM chip, they are each logically connected to a disjoint region of the memory. In essence, we are able to logically partition a single physical resource. 

At BedRock, our goal is to establish the bare-metal property™ of the BedRock Hypervisor™ (BHV™). We architect BHV as a highly modular, microkernel-based platform that enables extension by adding new applications – verified or unverified – to the system without needing to worry about the integrity of the system as a whole. At the level of a single computer, the bare-metal property guarantees that the behavior of a guest running on the BHV stack is a subset of the possible behaviors that could be seen if that guest ran directly on a conformant bare-metal system. Said another way, the BHV’s virtual machine monitor conforms to the architecture specification. Due to BHV’s use of hardware virtualization, which is necessary for performance, our guarantee assumes that the underlying hardware virtualization mechanisms are correct. BHV’s capabilities extend this bare metal guarantee to the network through the virtual switch to provide a strong guarantee about connected guests running on BHV. 

To prove these properties at the scale of BHV, we need to mechanize and operationalize the mathematics of software so that computers can assist us with the proofs, which requires us to draw on software engineering principles and methodologies. Our verification infrastructure targets C++, providing our engineers with a mainstream programming language that has all the associated abstraction mechanisms and tooling to quickly develop robust code. The mathematics that we use to formalize BHV is concurrent separation logic, which embraces and formalizes the modularity and reasoning principles that software engineers use every day. Our use of separation logic enables us to integrate formal methods early into the development process and to carry formal methods (FM) through the full development cycle. Every day, we are using these techniques to verify interesting concurrent libraries and to compose these libraries to build verified, concurrent applications.

In this post, we gave a high-level overview of why and how we use formal methods at BedRock. In future posts, we’ll dive deeper into these topics. Stay tuned! 

Interested in how we use FM at BedRock? Check out our whitepaper.

Share This Post

Share on linkedin
Share on facebook
Share on twitter
Share on email