Formal verification is the process of using automatic proof procedures to establish that a computer program will do what it’s supposed to. Given a mathematical specification of how a function is supposed to behave, and some assumptions about the environment where the code executes (e.g., how the operating system behaves and which inputs are reasonable), formal verification determines whether the code as written will ever, with any input that meets the assumptions, violate the specification.
Formal verification is known to produce more secure and less buggy code, but it’s rarely used on large commercial software projects. Developers working on deadline lack time to write careful function specifications — if they’re even familiar with the formal languages typically used for them. Verification teams, conversely, lack familiarity with the software under development; learning how every function in a commercial-scale program is supposed to behave can be prohibitively time consuming.
On the Amazon Web Services’ Automated Reasoning team, we’ve piloted several projects on integrating formal verification into the software development process. Some involve verification at the protocol level; some involve generating code directly from a verified specification; and some involve verification at the code level itself.
In a paper we’ll present at the International Conference on Software Engineering — which was to be held this week but has been postponed until July — we describe lessons learned from one of the code-level verification projects, which involved a large development initiative in 2019.
In the paper, we report that, thanks to our methodology, the number of verified lines of code, bugs found and fixed, verification “contracts” introduced by developers, and working code (i.e., non-proof code) contributed by the verification team all increased precipitously in the first eight months of the project.
Our method has six key components:
1. Function specification in a familiar programming language.
Writing function specifications typically requires a special-purpose formal language that can capture all of the logical relationships that might govern a function’s execution. With our method, both the verification team and the developer team instead specify functions in the language in which the code is being written — in this case, C. This approach sacrifices some expressive power: there are some logical relationships that C cannot capture. But we have found that ease of adoption more than makes up for the loss of expressivity.2. Declarative function specification.
Most familiar programming languages — such as C — are imperative, meaning they describe functions as sequences of operations. For function specification, however, declarative syntax is more intuitive. For instance, the developer should be able to say (in slightly more formal terms), “This function doubles each value in an array”, rather than having to write out the procedure for stepping through the array and doubling values individually. With our method, the verification team provides a library of functions that enables developers to write such declarative specifications in a familiar imperative language.3. Code-embedded specifications.
Most program functions are written as self-contained blocks of code. With our method, we allow the developer to write a function specification as a set of preconditions that precede each such block — which function inputs are invalid, for instance — and a set of postconditions after each such block — that an array has adequate memory allocated to it, for instance (see sample code, above). Usually, a developer writing a function is thinking through such operational parameters, anyway, so adding the specification is not a huge burden.4. A proof model that uses a familiar “unit test” syntax.
Many developers are already familiar with writing “unit tests” for their code. Inserted into the code for a specific program function, the unit test cycles through a sequence of inputs to determine whether any cause errors. Our proof method uses a very similar syntax, except that, rather than a sequence of concrete inputs, it specifies a range of possible inputs. Such test code can automatically be converted into the type of mathematical expression that automated provers are designed to evaluate.
5. Bug repair.
The great advantage of formal verification is that it not only identifies bugs but indicates how to fix them, by pinpointing exactly which lines of code lead to violation of the function specification. We have found that one of the most effective means of selling developers on the utility of formal verification is for the verification team to not only identify bugs but provide code patches for them.6. Continuous integration.
On large software projects, code is constantly being revised. As part of our method, we provide a back-end system that automatically re-runs the prover on new code as soon as it’s checked in to a repository, providing immediate feedback on whether the revision does or does not violate function specifications.
In the paper, we report the application of our methodology during development work on the AWS C Common Library, an open-source repository of functions used by several other AWS libraries, including widely used AWS software development kits.
Using our methodology, one full-time verification engineer and two interns, working together with the development team, were able to specify and verify (with some assumptions) 171 entry points (points in the program where the user can input data) over nine key modules of the library.
In ongoing work, we are expanding not only the code base to which we apply our methodology but also the range of functionality that our method can verify automatically. We are also evaluating best practices for long-term maintenance of provable code and for bringing new developers up to speed on existing provable code bases.
