Research Institute in Verified Trustworthy Software Systems (VeTSS)

Modern software systems comprise components constructed by many parties, ranging from individual open-source developers to companies and government organisations spanning the globe. They are written in multiple, complex languages, depend on the correctness of sophisticated third-party libraries, exploit concurrency and distribution to handle vast data sets, and are developed according to new software design processes that advocate frequent source code updates. Traditional methods for ensuring software reliability are inadequate in this modern context: modern companies move fast, leaving little time for code analysis and testing; traditional testing methods do not work well with concurrent and distributed programs; and the reluctance of users to update mobile apps renders the deployment of software fixes ineffective. Scalable techniques that can provide trust, in the deep technical sense of analysis and verification, are vital not only to support safe software, but also to give stability to this international software infrastructure.

The purpose of this new Research Institute in Verified Trustworthy Software Systems (RIVeTSS) is to bring together and support world-class UK academics and industrialists in systems, security and verification, unified by a common interest in program analysis and verification, at the forefront of research developments in fundamental theories and industrial-strength tools, targeting real-world applications. Such analysis of program behaviour is of critical importance to proper management of the rapid evolution of modern software systems

RIVeTSS will have direct industrial impact. While key ideas behind analysis and verification were introduced more than three decades ago, only recently have these techniques become practical as a result of significant advances in fundamental theory, solver technology, and scalable tool development. The resulting explosion of activity is evidenced by papers appearing in the best theoretical and practical conferences, tools being used in industry, and expert academics transferring to industry. Despite this success, program analysis and verification for modern software systems is in its infancy. In the context of applying program analysis to improve software quality, Facebook has the saying: "this journey is 1% finished'' [Facebook Infer tool, open-source announcement, 2015]. RIVeTSS will catalyse a change in industrial practice by developing industrial-strength tools, influencing industrial standards, and improving core software infrastructure, so that analysis and verification become routinely used in industrial software development, leading to broad, sustainable and long-term industrial impact.

RIVeTSS will have substantial societal impact. We already face critical danger from faults in software, ranging from intellectual and monetary theft, to failures that have led to loss of life. As society becomes even more dependent upon computer and communication systems, and the complexity of these systems grows, we expect to see more failures and greater damage. Therefore, analysis techniques for verifying the correctness, security and privacy of software systems are crucial.

RIVeTSS will also have economic impact. Modern large software systems must be composed of software units constructed by many parties, ranging from individual open source developers, to companies and government organisations that span the globe. Techniques that can provide trust, in the deep technical sense of verification, are absolutely vital to support not only safe software, but also to give stability to this international software infrastructure. More directly, economic impact will arise from the reduction in effort required for software maintenance due to the high degree of reliability that analysis and verification can offer.

An essential issue is to understand how to make program analysis and verification trustworthy. In security and aircraft industries, certification is based on out-dated ideas of trusting that a developer is a good person and tracking the provenance of software. Instead, software should be judged on fundamental scientific principles, such as "Are the behaviours exhibited by the software the ones we want?" In the high-assurance software group at GCHQ, the process of software certification is done by GCHQ employees reading the code. Instead, software should be, at least in part, assessed by industry using trusted analysis and verification tools. A key role of RIVeTSS is to develop a culture of best practice amongst academics and industry, leading discussion about how to move industry standards and processes in the right direction. Analysis and verification should be embedded right at the heart of the software design process, even to the extent that lawyers can actually guarantee software behaviour.