BedRock Systems’ approach keeps software safe from intrusion and running as designed.
Traditionally, software design relies on inefficient, ineffective, informal techniques to ensure that the software operates as intended. Consequently, bugs slip through the quality assurance process and companies spend a great deal of time and money trying to fix them. Formal methods techniques provide an alternative (but complementary) means to ensure quality. Using formal methods Address, developers build mathematical models of the systems and use logic to reason precisely about them. Verified code is proved to adhere to its specification, resulting in software systems that are higher quality and more secure.
Limitations of Traditional Testing
In the past, evaluating the quality of systems has been more an art than a science. Testing examines a small subset of a large number of possible interactions and relies on extrapolation to infer “correctness” of the system. However, as we all know, extrapolation is not a sound reasoning principle. The black swan proves the fallacy but bug reports in “tested” code are a much more telling story underscoring what is at stake.
The growing complexity of modern systems has pushed the testing-based model to the breaking point. Larger software applications mean more inputs, more states, more variables, and more opportunities for designs to go wrong. The vast possibilities have become too great for developers to comprehend, account for, and protect. Security is one of the biggest challenges for software in critical infrastructure. It is imperative that we rebuild the development process on a rock-solid foundation in order to deliver the quality required by users.
Formal Methods Provide a Rigorous Foundation for Systems Development
To build provably correct software at scale, we need a toolbox that can scale to the infinite. While our systems themselves may not be truly infinite, the world beyond them is practically so, and attempting to leverage the finiteness of modern systems is, often, a fool’s errand. Mathematics provides a foundation for building iron-clad proofs about systems even in the presence of never-before-seen behaviors. This open-world mentality makes it possible to protect against attackers ranging from script kiddies to entities with nation-state scale resources.
To enable developers to leverage formal methods techniques, we use the BedRock Formal Methods process to connect our code to mathematics. Building on this connection, we can leverage a myriad of techniques to analyze and verify properties of our code.
Recent innovations developed in academia and built upon by BedRock Systems have enabled BedRock to compositionally express, and begin to verify, the correctness of the BedRock HyperVisor™ as a refinement of bare-metal hardware. This Bare-Metal Property™ ensures that BHV™ will not (by default) inhibit the behavior or the software you care about[1]. In addition, running on BHV™ you can leverage BedRock’s suite of Active Security™ tools to safely introspect and protect your application stack without increasing its attack surface.
Formal Methods Deliver a Rock-Solid Foundation for Secure Computing
Formal methods makes it possible to construct systems with mathematically rigorous correctness guarantees. The BedRock Formal Methods process produces proofs that are independently machine checkable, providing a concrete, trustworthy foundation for the next generation of life-, safety-, and government-critical systems. Taking the human out of the loop as much as possible on the verification process helps to scale the verification effort to more software modules, and enables a more agile process for critical systems. Building on a solid foundation enables corporations to focus on their core businesses, rather than increasing attack surfaces by plugging infrastructure holes with even more layers of technology. All together, the BedRock Systems approach enables innovation while under attack, even in a contested environment, and unlocks the business potential of the Internet of Things.
By Gregory Malecha
[1] Up to timing-insensitive safety properties.
