We entrust large parts of our daily lives to computer systems, and these systems require thorough verification to ensure their correctness. System vulnerabilities can lead to leakage of confidential information, loss of money, and (in the case of cyber-physical systems) may even threaten one's physical safety and security. Many such bugs have in fact been found in computing systems in recent years, ranging from security vulnerabilities (like Meltdown and Spectre) to network errors to concurrency bugs.
Some important bugs are due to flaws in system design/specification, while others are due to implementations violating the design specification. Since verification is generally focused late in development, bugs tend to get caught late in development as well. Design bugs may necessitate a redesign, wasting the development time spent creating incorrect implementations. Furthermore, many bugs only occur in very specific scenarios, making them hard to find. Current verification processes have proven inadequate for catching these bugs, resulting in the release of flawed hardware and software.
Verification using formal methods provides strong correctness guarantees based on mathematical proofs, and is adept at catching hard-to-find bugs. My work aims to improve the verification of hardware and software using formal methods, without requiring engineers to have formal methods expertise. I propose a philosophy of Progressive Automated Formal Verification, i.e. verification throughout the system development process, from early-stage design through to final implementation. Progressive verification has multiple benefits, including reductions in verification overhead and in overall development time. Automating formal verification also enables engineering teams to prove strong correctness properties about their designs and implementations by themselves, shifting the verification burden away from the relatively small number of formal methods experts.
In progressive verification, formal models of systems are first created and verified during early-stage design, thus catching design bugs before implementation commences. These models can then evolve to become more detailed as system design progresses. Once the system is implemented, the implementation is formally verified against a proven-correct design model to help ensure implementation correctness. The number of steps in a progressive verification flow may vary depending on the type of system being built, but the key idea is to conduct verification throughout the design timeline and link the verification methods at each stage together.
The work in my dissertation constitutes a concrete instance of a progressive verification flow for MCM properties in parallel processors. However, progressive verification is a generic flow, and is applicable to other types of properties like hardware security properties. It is also applicable to other types of systems like cyber-physical systems.