Program Verification Techniques for Understanding Security Properties of Software

This proposal aims to develop automatic program verification methods that help security engineers to understand software that they have not written themselves. The engineer will be able to make sophisticated queries about resource requirements and temporal behaviour of code, such as about memory safety, privileges, or information flow. Our methods will even support synthesis of behavioural properties for the engineer: rather than make a closed-world assumption, where the complete program and physical computing device are known, our tools will discover logical descriptions of execution environments (preconditons, protocols, invariants, etc.) that pinpoint the assumptions necessary for code safety or those that trigger violations. Such tools would aid engineers by, for example, advising where to concentrate effort when looking for critical security breaches. They would also suggest where to place effort in hardening an application. Finally, by using strong analysis techniques based on verification, guarantees of security properties could be obtained, as well as flaws discovered.

Towards realising this vision we have assembled a team whoseexperience ranges from program verification research on logics and algorithms to systems security research involving new operating system primitives and software structuring principles that achieve robust security goals.

The work on this proposal will have potential for impact into the industry and the public sector.

We have links into Microsoft, both into static analysis research and into the security division on the product side. The London-based SME Monoidics ltd markets a static analysis tool which would be well placed to be influenced by the theoretical work and analysis prototypes done in this project. We also have a longstanding collaboration with Google on Native Client (NaCl), which securely runs untrusted native code downloaded from the Internet within the Chrome web browser.

These specific connections provide viable avenues for industrial impact of the results of this project. More generally,
static analysis is gaining more attention in industry as time goes on. Major players in avionics, consumer electronics, and the automotive and defence industries use static analysis for bug-catching in-house. Thus, if this project were to achieve its aims there would appear to be opportunity for further industrial impact in the mid- to long-term (.e., 5-10 years and out).

In the public sector, the mere fact of GCHQ's support for the Research Institute in Automatic Program Analysis and Verification indicates interest, and potential for impact. The UK Government has made clear that they view cybersecurity as important, from the Cabinet Office Cybersecurity Strategy document in 2009, through to a parliamentary briefing note "Cybersecurity in the UK" in 2011, to the Cybersecurity Challenge launched in 2012. Generally speaking, as far as the public sector goes, work under this RI call will likely have more avenues for impact into the public sector than static analysis work has had before.