DTacs - Program Verifier Tactics : Reducing the Development Time for Program Verifiers with re-usable Verification Strategies

Software is woven into just about everything digital that we touch or depend upon: from communications, entertainment and consumer electronics - to railway, air-control, automotive, finance, defence, national infrastructure and health-care systems. The dependability of such software remains a major challenge. In 2002 it was estimated that software mistakes cost the US economy $59 Billion; more recent estimates have suggested an annual cost of more than $300 Billion worldwide. Dependability is therefore a key differentiator in commercial products. Whoever can cost-effectively crack the dependability challenge will have a major advantage.

Conventional techniques used to ensure dependability are based around testing; and this can amount to half of the development time. Still, a fundamental problem of testing is that all combinations of inputs and conditions are not feasible. Formal approaches to software engineering use mathematics to ensure dependability. These have the advantage over conventional testing techniques that the software can be proven correct for all combinations of inputs and conditions. This is a result of using mathematics, and increases both the dependability and product quality. However, common bottlenecks of these approaches are limited availability of theorem proving skills and lack of automation provided by tools. Therefore they have often suffered from increased development time and costs when applied beyond niche markets such as safety and mission critical systems.

Program verification is a formal software engineering technique where the source code is combined with a formal specification of desired behaviour. Mathematics is used to prove that the program satisfies its specification. Recently, there has been a wave of new program verifiers, where the underlying mathematics is hidden. Skills familiar to programmers are used to guide the proof in the program text rather than theorem proving skills; removing the "skill-barrier" associated with theorem provers and creating a more accessible discipline for a software engineer. Still, an open challenge is to reduce the amount of guidance that is required to complete the verification of a program - a challenge that has to be solved before program verification becomes a viable cost-effective mainstream software engineering discipline.

This proposal addresses the automation challenge by enabling software engineers to encode patterns used to guide proofs directly in the program text as special programs. As a result, low-level and repetitive details, often resulting from a trial-and-error process, can be replaced by a higher-level underlying pattern. These can be re-used for similar tasks, liberating users from low-level and repetitive search tasks. As a pattern only needs to be developed once, less guidance will be needed - increasing automation and reducing development time and cost.

The language used to write programs and guide proofs within a program verifier will be extended to enable software engineers to also encode their verification patterns. The extension should be as minimal as possible, to avoid reducing accessibility with new skill-barriers that have to be overcome. The development of such language requires a new understanding of how users guide program verifiers. We will focus on the Dafny program verifier; re-engineering the development process used in a selection of the available Dafny case studies; and developing and verifying new programs from scratch. In both cases, each step of the verification process will be captured, creating a catalogue of verification patterns.

Based on this catalogue the language used within Dafny will be extended with a new special method called a `DTac' (Dafny Tactic). A verification pattern will be encoded as a DTac. Automation will be achieved by developing a new tool called Tacny that can read DTacs and apply them to other Dafny programs to automate the verification.

There are a large number of examples illustrating the cost of software failures - human, financial and reputational. Recent examples include Toyota, which had to recall 3.8 Million cars due to a defect in the electronic throttle-control system in 2009/10; and a bug in the software of the Moody credit rating agency, incorrectly awarding top ratings worth $4 Billion at the beginning of the recent recession. The crash of Air France flight 447 in the Atlantic Ocean in 2009, killing 228 people, can also be attributed to software, or at least a misunderstanding of software behaviour. These examples clearly illustrate the need for dependable software.

Formal approaches to software engineering improve dependability by using mathematics to prove correctness for all combinations of inputs and conditions. This is unfeasible for traditional test-based techniques. Formal approaches have been shown to improve the product quality; it has also been shown to be more cost-effective than methods based upon testing for safety/mission critical systems; and to combat Cyber Security threats to the UK - considered as `Tier 1' by the UK National Security Strategy. However, a significant amount of user guidance is often required for the verification, and such skills are at a premium. Whoever can reduce the amount of guidance, and cost-effectively crack the dependability challenge, will therefore have a major advantage.

The type of program verifiers addressed in this proposal has reduced the skills required by hiding much of the underlying mathematics. The proofs are instead guided in the program text, using techniques more familiar to a software engineer. Toyota is now considering using such techniques following the bug in their electronic throttle system.

While automation has improved in such techniques, further reduction will be required to have real impact as a cost-effective mainstream software engineering discipline.

This proposal addresses the automation challenge by enabling users of the Dafny program verifiers to encode verification patterns that can be re-used for similar verification tasks. A prototype tool called Tacny will be developed for Dafny. Tacny will be able to apply user-provided verification patterns to unverified programs in order to automate the verification. Dafny users will therefore directly benefit from this work by using this tool to reduce the required user-interaction. Tacny will be freely available for anyone to try out.

The main scientific impact of this proposal will be improved automation by reducing this interaction. A language where a user can capture the underlying patterns of a proof will be developed. A novelty of this language is that constructs familiar to software engineers should be used to write the patterns. This will have a profound effect on the potential update of this technology, as the additional knowledge required is incremental, and the language used will be known.

By re-applying a pattern to a verification task, more automation can be achieved without requiring interaction and exposition of underlying proof details. This could take program verification techniques one step closer as a solution to the dependability challenge. Companies already using program verification technology may have a direct advantage by embedding the techniques we develop to reduce their development time.
Safer, more dependable and more secure software can then also be developed faster, which may help in attracting new companies to adopt program verification technology, and further combating the Cyber Security threats.