Research Institute in Verified Trustworthy Software Systems (VeTSS)

Lead Research Organisation: Imperial College London
Department Name: Computing

Abstract

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

Planned Impact

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.

Publications

10 25 50
publication icon
Gardner P (2017) Verified trustworthy software systems. in Philosophical transactions. Series A, Mathematical, physical, and engineering sciences

 
Description GCHQ provides some funding for research projects, which are awarded by VeTSS. The report that details the key findings for these projects is at https://wp.doc.ic.ac.uk/vetssannualreport/
Exploitation Route See https://wp.doc.ic.ac.uk/vetssannualreport/
Sectors Digital/Communication/Information Technologies (including Software)

URL https://vetss.org.uk
 
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 GCHQ Small Grants scheme
Amount £95,151 (GBP)
Organisation Government Communications Headquarters (GCHQ) 
Sector Public
Country United Kingdom
Start 11/2016 
End 03/2017
 
Description Fifth Workshop on Formal Methods and Tools for Security 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact VeTSS co-organised and co-funded the Fifth Workshop on Formal Methods and Tools for Security, held on 21-22 September at Microsoft Research Cambridge, brought together world-leading UK and international researchers, as well as UK PhD students, industrialists and government employees with a common interest in formal methods and verification. The programme included 19 specialist talks, poster presentations, and a session of short talks for PhD students, RAs, and industrialists to introduce themselves to each other and the audience. Both goal and outcome of the workshop was the establishment of new and the strengthening of existing connections between formal analysis experts in academia, industry, and government.
Year(s) Of Engagement Activity 2017
URL https://vetss.org.uk/fifth-workshop-on-formal-methods-and-tools-for-security-fmats5/
 
Description Sponsorship of 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020) 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact PLDI is one of the main conferences for practical and experimental work in the design and implementation of programming languages. The sponsorship contributed to make registration to the to the conference and co-located events free for participants, widening participation in the event. It also raised awareness of the work the RI and the associated projects to an international audience and resulted in a number of planned collaborations.
Year(s) Of Engagement Activity 2020
URL https://pldi20.sigplan.org/program/program-pldi-2020
 
Description Sponsorship of Federated Logic Conference 2018 Oxford, UK 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact The Federated Logic Conference brings together several international conferences related to mathematical logic and computer science. Our sponsorship contributed to reduced registrations for students to widen participation in the event. We also manned one of the welcome stands, where delegates could find out more about the Research Institute
Year(s) Of Engagement Activity 2018
URL https://www.floc2018.org/sponsors/
 
Description UK Cyber Security Research Conference / 6th Joint Annual Research Institutes Highlights Conference 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Other audiences
Results and Impact 125 people attended the 6th Joint Annual Highlights Conference 2020 at the Royal Society, 6-9 Carlton House Terrace, London. We presented the work of the Research Institute and the funded projects and gave details of activity in industry by VeTSS academics.
Year(s) Of Engagement Activity 2020
 
Description VeTSS PhD School and Sixth Workshop on Formal Methods and Tools for Security 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact VeTSS funded and co-organised the VeTSS PhD School and Sixth Workshop on Formal Methods and Tools for Security, held in Microsoft Research Cambridge on the 24th and 25th of September, 2018. The workshop included around a hundred and twenty delegates and two days of talks by world-leading formal methods experts from academia (Cambridge, Imperial College London, Inria Paris, University College London, Purdue, etc.), industry (Adelard, Galois, Google, Data61, etc.), and funding bodies (NSF). An important goal of this workshop was to bring together verification, systems and security experts interested in formal analysis, industrialists interested in software validation, and government scientists interested in reliable software systems, and to introduce them to the current generation of UK PhD students and postdocs. This was also the opportunity for the researchers leading VeTSS-funded projects to present themselves and their research to a broader audience.
Year(s) Of Engagement Activity 2018
URL https://vetss.org.uk/fmats6/
 
Description Verified Software Workshop 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact The `Verified Software' workshop was held at the Isaac Newton Institute for Mathematical Sciences, Cambridge on 24th-25th September 2019. The workshop was organised by VeTSS working in partnership with the Newton Gateway to Mathematics and the Isaac Newton Institute as a forerunner to the six-week summer programme on `Verified Software', which was meant to be held in the summer of 2020, but was delayed by the Covid-19 pandemic. The workshop was attended by 110 delegates and included talks by world-leading experts from academia, industry and government. The aim is to bring together verification, systems and security experts interested in formal analysis, industrialists interested in software validation, and government scientists interested in reliable software systems, with the main goal of forming a pathway towared addressing the grand challenges in the field of formal analysis. Additionally, another goal was to introduce these experts to the current generation of UK PhD students and postdocs.
Year(s) Of Engagement Activity 2019
URL https://vetss.org.uk/vetss-verified-software-workshop-24th-25th-september-2019/
 
Description Verified Software: From Theory to Practice, Isaac Newton Institute for Mathematical Sciences (INI), Cambridge 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact The workshop was attended by over 30 internationally recognized researchers working on the specification and verification of software-intensive systems. The workshop allowed participants to exchange of ideas between researchers facing the challenges of cutting-edge applications and theoreticians armed with the conceptual tools to potentially address these challenges. The discussions will then inform the INI scientific programme on Verified Software in the summer of 2022.
Year(s) Of Engagement Activity 2021
URL https://www.newton.ac.uk/event/vsow03/
 
Description Verified Software: Tools and Experiments, Isaac Newton Institute for Mathematical Sciences (INI), Cambridge 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Researchers at the workshop discussed integrated tool resources for automated formal methods with standardized interfaces and interchange and data/evidence formats that allow services and arguments to be composed and test cases and counterexamples to be shared across different formal models. The goal workshop was to lay the foundation for powerful automated tools and integrated tool suites that can be deployed in a range of large-scale experiments and case studies.
Year(s) Of Engagement Activity 2021
URL https://www.newton.ac.uk/event/vsow04/