EPSRC logo

Details of Grant 

EPSRC Reference: EP/R012261/1
Title: Fast Runtime Verification via Machine Learning
Principal Investigator: Grigore, Dr R
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Runtime Verification Inc
Department: Sch of Computing
Organisation: University of Kent
Scheme: First Grant - Revised 2009
Starts: 01 January 2018 Ends: 30 June 2020 Value (£): 100,918
EPSRC Research Topic Classifications:
Artificial Intelligence Software Engineering
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
05 Sep 2017 EPSRC ICT Prioritisation Panel Sept 2017 Announced
Summary on Grant Application Form
When programmers make mistakes, costs can be huge. Programmers make mistakes because they are human. To help them, researchers are developing tools. No tool is a silver bullet; each has advantages and disadvantages. We focus on one kind of tool: the runtime verifiers. Programmers use runtime verifiers more and more, which attests to their utility. Runtime verifiers observe a program while it runs and look for signs that something is amiss. This slows down the program, which is why runtime verifiers are used only by programmers, before releasing the program to users. If runtime verifiers would be more efficient and would not slow down programs so much, then they could remain active in released programs, which would make them more useful. For example, they could be used for detecting security intrusions in deployed systems.

This research project is focused on increasing the efficiency of runtime verifiers.

A Cambridge study from 2013 estimated that the worldwide cost of fixing software defects to be $310 billion per year. A large part of this cost is programmer time. The interval between finding a defect and fixing it is not so small because the task is often not so easy. Some defects are security vulnerabilities, which makes the fixing interval a window of opportunity for criminals. The window of opportunity is bigger than the fixing interval because it also includes the time until users decide to update their software. The size of the window of opportunity is important. For example, updating software regularly is recommended by the UK government, in its Cyber Essentials Scheme. This guidance was issued after a government study showed that, in 2014, nine out of ten large organisations in UK suffered security breaches, and each security breach had an average cost of 1.5 million pounds.

Runtime verifiers could be used to reduce the window of opportunity that criminals have, as follows. Programmers describe scenarios that should not happen. A runtime verifier then observes the program while it runs and, if one of the forbidden scenarios does happen, then the runtime verifier can take an action. For example, the runtime verifier could be instructed to kill the program, because a program crash is preferable to a security breach. Alas, such a use case for runtime verifiers is unrealistic at the moment, because no user would tolerate a program that runs ten times slower than usual just for the benefit of extra protection against security intrusions. In this project we aim at finding a better trade-off. We want the program to run only slightly slower than usual and, in return, we are willing to give up some of the guarantees offered by a runtime verifier, but not much. But, how to find a good trade-off? The key will be using a toolkit developed recently in the machine learning community.

Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.kent.ac.uk