New project to research Safe and Secure Software Systems

Dr Budi Arief, Senior Lecturer at the School of Computing and member of the Kent Interdisciplinary Research Centre in Cyber Security (KirCSC), is collaborating with PhD student Tom Seed and Emeritus Professor Andy King, on a new project titled "Symbolic Computation for Mainstream Verification".

The project is funded by the National Cyber Security Centre (NCSC), via the Research Institute in Verified Trustworthy Software Systems (VeTSS) –  a UK Academic Research Institute in Cyber Security at Imperial College London, funded by the Engineering and Physical Sciences Research Council (EPSRC). VeTSS supports world-class academics and industrialists to develop novel techniques for keeping software systems safe and stable.

The project will run for one year from April 2021 to March 2022 and aims to develop advanced SMT (Satisfiability Modulo Theory) solvers, which are used to verify and test the vulnerability of software.

Andy said: "This research is particularly timely since we are now seeing a new class of SMT solvers emerge, that apply powerful algebraic reasoning in the theory component of SMT solvers. The focus of this work has been to adapt classical algebraic algorithms to the new setting of SMT, typically by adding incrementality or learning. This will ensure software correctness, which in turn will improve security.”

Budi said: "As software continues to play a bigger role in our society, it is imperative to ensure its security and trustworthiness, hence the interest in verification. We are really pleased we have been given funding for this project. It is a particularly significant achievement since the acceptance rate for VeTSS has been around 25% in the previous 4 years of calls. Furthermore, this project demonstrates the continued collaboration between the Cyber Security and the Programming Languages and Systems research groups at Kent."

For further information on the project or for updates, please contact Dr Budi Arief.