The modern world runs on software. From smartphones and automobiles to medical devices and power plants, executable code drives insight and automation. However, there is a catch: computer code often contains programming errors—some small, some large. These glitches can lead to unexpected results—and systematic failures.
“In many cases, software flaws don’t make any difference. In other cases, they can cause massive problems,” says Kathleen Fisher, professor and chair of the computer science department at Tufts University and a former official of the U.S. Defense Advanced Research Projects Agency (DARPA).
For decades, computer scientists have imagined a world where software code is formally verified using mathematical proofs. The result would be applications free from coding errors that introduce bugs, hacks, and attacks. Software verification would ratchet up device performance while improving cybersecurity and public safety. By applying specialized algorithms and toolkits, “It’s possible to show that code completely meets predetermined specifications,” says Bryan Parno, an associate professor in the computer science and electrical and computer engineering departments at Carnegie Mellon University.
At last, the technique is being used to verify the integrity of code in a growing array of real-world applications. The approach could fundamentally change computing. Yet, it is not without formidable obstacles, including formulating algorithms that can validate massive volumes of code at the speed necessary for today’s world. The framework also suffers from the same problem every computing model does: if a verified proof is based on the wrong assumptions, it can validate invalid code and produce useless, and even dangerous, results.
“Formal verification is simply a way to up the ante,” Fisher explains. “It’s a way to modernize and improve the way software is written and ensure that it runs the way it is supposed to operate.”
Looking for Proof
Modern software development revolves around a straightforward concept. Coders define a task, write code, and validate it by testing the code in the real world. How a smartphone app, medical device, or autonomous vehicle acts, reacts, and interacts is probed and studied. As programmers discover flaws or ways to improve the code, they rewrite and update the software to improve the performance of the application. Unfortunately, new code often introduces other errors and new vulnerabilities. This cycle sometimes continues ad infinitum because there is no way to ensure code is error-free, and it is impossible to imagine every possible scenario, or corner case.
That is where formal verification enters the picture.
The idea of writing and executing error-free software isn’t new. In 1973, Edsger W. Dijkstra floated the concept of using mathematical proofs to verify code. Three years later, his seminal book A Discipline of Programming introduced a conceptual framework for putting verified code to work in the real world. It presented the then-revolutionary idea that programming tasks should be treated more like mathematical challenges. Along the way, other computer scientists, including Tony Hoare, formulated key ideas that demonstrated the feasibility of software verification.
Formal verification advanced slowly, however. Breakthroughs proved difficult because the proofs required are incredibly complex and developing user-friendly, off-the-shelf tools for verifying code is extraordinarily difficult. Adding to the challenge: software validation can be a slow process. Over the last couple of decades, scattered examples of formal verification have appeared, including the use of the technique by the National Aeronautics and Space Administration (NASA) for critical flight software. More recently, organizations such as Amazon, Intel, AMD, IBM, Google, Firefox, and Microsoft have begun to use the technique for assorted software components, ranging from microkernels in processors to Web browsers and cloud infrastructure.
“We have witnessed significant advances in how to think about computer programs mathematically and how to formally specify how a programming language is going to behave,” Parno says. Simply put, enormous increases in computing power, significant advances in modeling languages, and the steady evolution of algorithms and off-the-shelf toolkits for verifying code have pushed the field to a tipping point. With a critical mass of knowledge and practical ways to verify code, the method is now moving into the mainstream.
Successfully verifying code hinges on a critical factor: the ability to construct a mathematical model that proves the code is error-free and results in the desired outcome.
Successfully verifying code hinges on a critical factor: the ability to construct a mathematical model that proves the code is error-free and results in the desired outcome. There are essentially three pieces to this puzzle. First, there is the specification—the mathematical description of what someone wants to achieve, along with their assumptions about the environment. Second, there is the program that actually does the work; this program is written in ordinary code that is essentially the same as any other code without verification. Third, there is the proof that demonstrates the code is actually computing what the specification says it should.
Suppose a software developer wants to write a program to sort an array of A of N numbers into a new array of B. She might write a specification that defines the quality of B being sorted as follows:
For all values j and k such that 0 <= j < k < N, it must be the case that B[i] < B[j].
In this case, the developer would write a program with normal code to actually sort the values in the array A. She would then write a proof explaining to the verifier why the program correctly sorted the numbers. She might show each step sorts two numbers into their correct places and preserves the correctness of the numbers already sorted. Although the specification in this example is not entirely complete because it’s focused only on sorting—there would still be a need to ensure B contains the same elements as A—it certifies that this operation meets desired specifications.
In the real world, “All three of these pieces are fed to an automated verifier, which is responsible for checking whether the proof is correct,” Parno says. “Assuming there are no bugs in the verifier and there are no bugs in the specification, then if the verifier signs off, the code is provably/mathematically correct.” However, if the code or the proof is incorrect relative to the specification, then the verifier is guaranteed to reject it. “In that case, as a developer, you can go back and fix your code and/or proof until the verifier accepts it,” Parno adds.
Getting all three components right is the key. “Suppose you want to write software that only opens a door when someone swipes an authorized badge. If you accidentally write your system specification to say that the door should open when a swipe card fails, then your software might provably meet that specification, but you would be unhappy about the result,” Parno explains.
Applying Logic
Temporal logic, which attempts to capture a complete set of actions and behavior over time, is at the heart of formal verification. It is built into the proof used to check the software. Not surprisingly, the complexity and sheer volume of today’s code—along with the enormous number of outcomes and possibilities that can occur with computerized tasks—makes it nearly impossible to verify every code component in every library or device. However, the beauty of verified coding is that it is not necessary to ensure every piece of code is free from errors large and small. “There’s lots of software where it simply doesn’t matter,” Fisher points out. “If a component or system doesn’t work right within the overall framework or environment, nothing serious happens. The overall structure continues to operate without any serious consequences.”
Indeed, the key to effectively using formal verification is to apply it at the right place and in the right way. In some situations, this may mean using the technique for a specific component within a software application. For instance, Google and Firefox have installed code-verified components in their Web browsers. Amazon Web Services (AWS) has turned to this methodology to address design problems in critical cloud systems. This includes using the formal specification language TLA+ (Temporal Logic of Actions) to develop “fault tolerant distributed algorithms for replication, consistency, concurrency control, auto-scaling, load balancing, and other coordination tasks.”
In other scenarios, formal verification may translate into building a verified computing system from the processor up. For instance, DARPA has contributed to the development of a binary verified microkernel for the ARM processor it can place in various systems and devices. The kernel, built on C language, required 26 man-years to build. “We know these chips are faithful to the ARM reference design and we can add software on top with a high degree of confidence,” says Raymond Richards, program manager in the information innovation office at DARPA. “We want to apply this foundation in places where we know the code isn’t going to change quickly and where it’s really important to make sure every bit and byte is correct.”
DARPA has aggressively pursued formal verification as part of its High-Assurance Cyber Military Systems (HACMS) project and a more recent Cyber Assured Systems Engineering (CASE) initiative. In 2015, the agency generated attention when it held an exercise that encouraged a team of experts to try to hack their way into an unmanned military helicopter. Over the span of the six-week event, the hackers failed to gain access to the software residing in the onboard flight control system. “We removed entire classes of vulnerabilities and created a highly resilient system,” Richard says.
Code Compliance
Formal verification continues to advance. A growing array of tools and resources are available to ensure software is mathematically sound. These include Coq Proof Assistant, HOL, Isabelle, Metamath and Z3 Satisfiability Modulo Theories (SMT) solver. The latter, for example, uses several decision procedures to deliver extended static checking, test case generation, and predicate abstraction. The Microsoft-developed tool includes an API library and it works with numerous programming languages, including C, C++, Java, Haskell, OCaml, Python, WebAssembly, and .NET/Mono.
Project Everest, which Parno helped create, aims to build a verified secure implementation of HTTPS. It is supported by Microsoft Research. Yet another high-profile example is seL4, a formally verified operating system microkernel designed to serve as a platform for building safety- and security-critical systems, with no dropoff in performance. Because the kernel controls access to all resources, it dramatically decreases the risk of hacks and attacks. SeL4 has been mathematically proven to be bug-free relative to its specification. Different variations of the kernel are available via a usage model that mimics the Linux Foundation. In fact, SeL4 was used in the DARPA-funded HACMS program to protect the helicopter in its hacking competition.
In the coming years, advances in formal verification likely will lead to far more reliable and secure computers, applications, medical devices, automobiles, robots, IoT systems, and more, Parno explains. The technique will also likely aid in protecting cryptography from far more powerful quantum computers, and it will enable more advanced homomorphic techniques that allow data scientists to analyze and study encrypted data without the ability to view it. While formal verification does not guarantee that a complex software system is completely protected, it greatly improves the odds.
“Formal verification doesn’t result in perfect code; it simply narrows the possibility for errors and vulnerabilities to creep in,” Parno says. “What makes the technique so attractive is that you push the uncertainty or scope of problems down to smaller and smaller windows.”
Further Reading
Barthe, G., Blazy, S, Grégoire, B., Hutin, R., Laporte, V., Pichardie, D., and Trieu, A.
Formal verification of a constant-time preserving C compiler Proceedings of the ACM on Programming Languages, November 2019. https://dl.acm.org/doi/abs/10.1145/3371075
Bhargavan K., et al.
Everest: Towards a Verified, Drop-in Replacement of HTTPS SNAPL 2017, http://www.andrew.cmu.edu/user/bparno/papers/everest-snapl.pdf
Fisher, K., Launchbury, J. and Richards, R.
The HACMS program: using formal methods to eliminate exploitable bugs, 2017, Philosophical Transactions of the Royal Society, 375, 2104. https://royalsocietypublishing.org/doi/full/10.1098/rsta.2015.0401
HOL Interactive Theorem Prover https://hol-theorem-prover.org
Isabelle https://isabelle.in.tum.de/
Metamath Site Selection http://us.metamath.org/mm.html
Miller, S.P., Anderson, E.A., Wagner, L.G., Whalen, M.W., and Heimdahl, M.P.E.
Formal Verification of Flight Critical Software AIAA Guidance, Navigation, and Control Conference and Exhibit, August 2005, https://shemesh.larc.nasa.gov/fm/papers/FormalVerificationFlightCriticalSoftware.pdf
Project Everest—Verified Secure Implementations of the HTTPS Ecosystem https://www.microsoft.com/en-us/research/project/project-everest-verified-secure-implementations-https-ecosystem/#!groups
Protzenko, J., Parno, B., Fromherz, A., Hawblitzel, C., Polubelova, M., Bhargavan, K., Beurdouche, B., Choi, J., Delignat-Lavaud, A., Fournet, C., Kulatova, N., Ramananandro, T., Rastogi, A., Swamy, N., Wintersteiger, C.M., and Zanella-Beguelin, S.
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider http://www.andrew.cmu.edu/user/bparno/papers/evercrypt.pdf
Richards, R.
Cyber Assured Systems Engineering Defense Advanced Research Projects Agency, https://www.darpa.mil/program/cyber-assured-systems-engineering
Richards, R.
High-Assurance Cyber Military Systems Defense Advanced Research Projects Agency, https://www.darpa.mil/program/high-assurance-cyber-military-systems
The Cog Proof Assistant https://coq.inria.fr/
The seL4 Foundation https://sel4.systems/Foundation/About/
Z3 Theorem Prover https://github.com/Z3Prover
Join the Discussion (0)
Become a Member or Sign In to Post a Comment