Fifth Annual VeTSS Call for Proposals: Safe and Secure Software Systems

This call is now closed. For details of the funded projects please see our funded projects page.

The Research Institute in Verified Trustworthy Software Systems (VeTSS), hosted at Imperial College London, is a UK Academic Research Institute in Cyber Security, funded by the Engineering and Physical Sciences Research Council (EPSRC), 2017-2022.

This VeTSS call, funded by the National Cyber Security Centre (NCSC), is for funding to be spent between 1/4/2021 and 31/3/2022.

THE CALL

Modern computer systems provide unprecedented benefits to society, science, technology and health, making their reliability, safety and security of crucial importance. However, current methods for establishing such trust in our software are insufficient; system faults are pervasive, resulting in privacy violations, intellectual and monetary theft, and even loss of life. Rigorous analysis, testing and verification techniques are essential for validating the reliability, safety and security of our international software infrastructure.

This VeTSS call on ‘Safe and Secure Software Systems’ is a broad call, grouped loosely under the headings Safe AI, Trustworthy Software, Verified Software Infrastructure and Reliable Continuous Software Behaviour. This is the last VeTSS call associated with the current funding from EPSRC and GCHQ.

• Safe AI

Intelligent AI systems, such as autonomous vehicles and robots, are crucial for the development of our modern society. This call welcomes proposals that explore the integration of techniques from AI with those from software analysis, such as the use of symbolic execution to establish trust in systems based on machine learning.

• Trustworthy Software

Mainstream developers are benefiting from scalable analysis tools used inside the large, open systems of technological giants, such as Amazon, Facebook and Google. Such tools are currently limited to lightweight bug-finding, but many of their underlying mathematical techniques can also be used for verification. This call welcomes proposals on the development of testing and verification tools for the specialist, and eventually the mainstream, developer to verify programs written in traditional languages, such as C, C++, Java and JavaScript, and also more modern languages, such as Rust, Verona, and WebAssembly.

Verified Software Infrastructure

A key challenge is to verify important parts of our software infrastructure, and understand how these verified parts interact with the rest of the infrastructure. Success stories include: the verified microkernel seL4; the verified C compiler CompCert; the verified autonomous helicopter software for the DARPA HACMS project; and the verification work at Cambridge associated with the ARM/CHERI project.  This call welcomes proposals that explore the verification of such specialist software, paying particular attention to understanding how such verification can be simplified, extended, maintained and integrated within our software infrastructure.

• Verified Continuous Software Behaviour

Many modern applications use software that combines continuous and discrete behaviour: for example, the software associated with cyber-physical and hybrid systems, data systems and reactive systems. The combination of continuous and discrete behaviour is a challenge for verification: for example, developers have a poor intuitive understanding of how their machine-learning algorithms behave, let alone of how to verify them. This call welcomes proposals to identify and solve significant verification challenges of software which combines continuous and discrete behaviour.

These highlighted problems are by no means comprehensive. The expectation is that proposals will address numerous challenges with the goal of placing verified software at the heart of the overall software infrastructure.

This is the fifth VeTSS call. The previous calls were highly competitive. Proposals should provide evidence of engagement with the international academic or industrial verification community, or the UK industrial community interested in applying such techniques to industrial practice

KEY DATES:

CALL PUBLISHED: 16th December 2020

PROPOSALS SUBMITTED: 21st January 2021 by 16:00 hrs

RESULT ANNOUNCEMENT: By 8th February 2021

RESEARCH PERIOD: 1st April 2021 – 31st March 2022