VeTSpec: Verified Trustworthy Software Specification

Lead Research Organisation: Imperial College London
Department Name: Dept of Computing


Modern society faces a fundamental problem: the reliability of complex, evolving software systems on which it critically depends cannot be guaranteed by the established, non-mathematical techniques, such as informal prose specification and ad-hoc testing. Modern companies are moving fast, leaving little time for code analysis and testing; concurrent and distributed programs cannot be adequately assessed via traditional testing methods; users of mobile applications neglect to apply software fixes; and malicious users increasingly exploit programming errors, causing major security disruptions. Trustworthy, reliable software is becoming harder to achieve, whilst new business and cyber-security challenges make it of escalating importance.

Developers cope with complexity using abstraction: the breaking up of systems into components and layers connected via software interfaces. These interfaces are described using specifications: for example, documentation in English; test suites with varying degrees of rigour; static typing embedded in programming languages; and formal specifications written in various logics. In computer science, despite widespread agreement on the importance of abstraction, specifications are often seen as an afterthought and a hindrance to software development, and are rarely justified.

Formal specification as part of the industrial software design process is in its infancy. My over-arching research vision is to bring scientific, mathematical method to the specification and verification of modern software systems. A fundamental unifying theme of my current work is my unique emphasis on what it means for a formal specification to be appropriate for the task in hand, properly evaluated and useful for real-world applications. Specifications should be validated, with proper evidence that they describe what they should. This validation can come in many forms, from formal verification through systematic testing to precise argumentation that a formal specification accurately captures an English standard. Specifications should be useful, identifying compositional building blocks that are intuitive and helpful to clients both now and in future. Specifications should be just right, providing a clear logical boundary between implementations and client programs.

VeTSpec has four related objectives, exploring different strengths of program specification, real-world program library specification and mechanised language specification, in each case determining what it means for the specification to be appropriate, properly evaluated and useful for real-world applications.

Objective A: Tractable reasoning about concurrency and distribution is a long-standing, difficult problem. I will develop the fundamental theory for the verified specification of concurrent programs and distributed systems, focussing on safety properties for programs based on primitive atomic commands, safety properties for programs based on more complex atomic transactions used in software transactional memory and distributed databases, and progress properties.

Objective B: JavaScript is the most widespread dynamic language, used by 94.8% of websites. Its dynamic nature and complex semantics make it a difficult target for verified specification. I will develop logic-based analysis tools for the specification, verification and testing of JavaScript programs, intertwining theoretical results with properly engineered tool development.

Objective C: The mechanised specification of real-world programming languages is well-established. Such specifications are difficult to maintain and their use is not fully explored. I will provide a maintainable mechanised specification of Javascript, together with systematic test generation from this specification.

Objective D: I will explore fundamental, conceptual questions associated with the ambitious VeTSpec goal to bring scientific, mathematical method to the specification of modern software systems.

Planned Impact

I summarise the significant long-term academic, industrial, economic, governmental and societal impact that VeTSpec offers. I emphasise my strong focus on delivering widespread impact beyond academia: on industry, via technology transfer and targeted dissemination; and on society in general via interaction with GCHQ, government and outreach.

Academic Impact

As outlined in 'Academic Beneficiaries', VeTSpec will have substantial academic impact, influencing both theoretical and practical research in program analysis and verification, and contributing to the next generation of research leaders in academia.

Impact on Industry

VeTSpec research will help bring formal specification and verification into the industrial software design process, resulting in broad, sustainable, long-term industrial impact. Engagement with my industrial partners at ARM (Chong, Reid), Amazon (Cook), Facebook (O'Hearn), Google (Miller, also on the ECMAScript Committee), and IBM (Dolby), is vital to achieving this. These partners will provide challenging examples to drive the VeTSpec foundational research, and will contribute by evaluating prototypes of the tools arising from the project, and helping me identify and capitalise on industrial impact opportunities. Economic impact will arise from the reduction in effort required for software maintenance due to the high degree of reliability that program specification and verification offer.

VeTSpec research will have impact on programming language and library standards. VeTSpec will provide a maintainable formal specification of JavaScript (C1), a concurrent specification of POSIX (A1), and several formal specifications of libraries and benchmarks. By engaging with the organisations that manage these languages, libraries and benchmarks, such as ECMAScript for JavaScript, the Austin Group for POSIX, and Erlang Solutions for the Erlang language, I will achieve valuable technology transfer to industry.

VeTSpec research will have impact on the industrial program developer. My partners are at the cutting edge of industrial specification and tool building, and, in turn, have huge impact on expert and non-expert developers in their respective industries, analysing millions of lines of code, deployed in products used regularly by billions of people. In particular, my work on fundamental theory and prototype tools is of direct interest to O'Hearn in Facebook, and my work on logic-based analysis tools for analysing JavaScript programs is of direct interest to Amazon, Facebook and IBM.

Governmental and Societal Impact

VeTSpec will influence the wider community interested in analysis and verification: those responsible for high-grade industry software certification at GCHQ and NCSC (partner Burns); those developing high-grade industrial software; and those representing cybersecurity inside government. For example, I have recently been invited to the NCSC Research Advisory Group, with the remit to be a 'critical friend'. I have also been asked to write a short position paper on 'Verified Trustworthy Software Systems' for civil servants representing the 'Secure by Default' programme and the 'CyberInvest' programme, so that they can better represent analysis and verification in strategy meetings. My industrial and academic impact plans will, in turn, generate wider societal impact, by leading to higher-quality software for end-users that is hardened against malicious attackers. To maximise societal impact, I will do outreach and advocacy activities to make the government and the general public aware of our research.


10 25 50
Description JaVerT 2.0 (POPL'19) Amazon Web Services (AWS). Using JaVerT 2.0 and later Gillian, Gardner's team has verified the deserialisation procedure of the AWS Message Header, part of the AWS Encryption SDK Message Format, formally verifying properties that were previously written by an Amazon code developer as English comments. This is the first time that industrial-grade JavaScript code has been verified. Facebook. Facebook have established the viability of using continuously-integrated compositional analysis techniques inside the industrial design process, both at Facebook and in many other companies. The modular design of JaVerT 2.0 provides a fundamental understanding of bi-abduction, the pioneering compositional analysis technique used by the Facebook static analysis tool Infer, in terms of fixes arising from resource errors. Gillian (PLDI'20) Amazon Web Services (AWS). Gillian was used to verify both the JavaScript and C implementations of the deserialisation procedure of the AWS Message Header, demonstrating how data-structure specification can be used across substantially different programming languages.
First Year Of Impact 2019
Sector Digital/Communication/Information Technologies (including Software)
Description Amazon Web Services, Research Gift: A Formally Verified Serialisation Module for the AWS Encryption SDK Message Format
Amount £100,000 (GBP)
Department Amazon Web Services
Sector Private
Country United States
Start 08/2019 
Description Funding for VeTSS projects
Amount £2,500,000 (GBP)
Organisation National Cyber Security Centre 
Sector Public
Country United Kingdom
Start 04/2017 
End 04/2022
Description Genifer: A General Verification and Testing Framework
Amount £74,526 (GBP)
Funding ID RFA20789/4214910 
Organisation Government Communications Headquarters (GCHQ) 
Sector Public
Country United Kingdom
Start 10/2019 
End 03/2020
Description Research Gift: Gillian
Amount $400,000 (USD)
Organisation Facebook 
Sector Private
Country United States
Start 09/2020 
Title Gillian 
Description Gillian is a language-independent platform for the development of compositional symbolic analysis tools. It supports three flavours of analysis: whole-program symbolic testing, full verification, and bi-abduction. It comes with fully parametric meta-theoretical results and a modular implementation, designed to minimise the instantiation effort required of the user. Gillian has been instantiated to JavaScript and C and evaluated on both real-world code and custom-made data-structure libraries, obtaining results that indicate that Gillian is robust enough to reason about real-world programming languages and programs. 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
Impact Gillian has garnered interest from both academia (e.g., Cambridge), industry (e.g., Facebook, Amazon, Arm), and government (National Cyber Security Centre). It was used to verify JavaScript and C implementations of the AWS Message Header deserialisation procedure; this is the first full verification of industry-grade JavaScript code. The initial success of Gillian led to a Facebook gift to Prof. Gardner's group in the amount of £500K, with the purpose of further development. 
Title JaVerT 2.0: Compositional Symbolic Execution for JavaScript 
Description JaVerT 2.0 introduces a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. It supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. JaVerT 2.0 has been evaluated on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
Impact JaVerT 2.0 has won a Facebook Research award ($50K) and was part of a project to verify parts of the Amazon AWS Message Format management system, which then migrated to Gillian. JaVerT 2.0 was the starting point for, an extension which has the ability to reason about event-driven programs that use the DOM and JavaScript constructs for asynchronous programming. 
Description We introduce a trusted infrastructure for symbolic analysis of modern event-driven Web applications. This infrastructure consists of reference implementations of the DOM Core Level 1 and UI Events, JavaScript Promises, and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics that is sufficiently expressive to describe the event models underlying all these APIs. Our reference implementations are trustworthy in that they follow the API respective standards line-by-line and they are thoroughly tested against the appropriate official test-suites, passing all the applicable tests. Using the Core Events Semantics and the reference implementations, we develop JaVerT.Click, a symbolic execution tool for JavaScript that, for the first time, supports reasoning about JavaScript programs that use some (possibly all) these APIs. 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
Impact JaVerT.Click was used to perform comprehensive symbolic testing of the events module of Cash, a widely-used jQuery alternative, creating a symbolic test suite with 100% line coverage, establishing bounded correctness of several essential properties of the module, and discovering two subtle, previously unknown bugs. As part of a project protected under an NDA, it was also used to analyse parts of the Amazon Prime Video codebase.