| EPSRC Reference: |
EP/N020243/1 |
| Title: |
Vulnerability Discovery using Abduction and Interpolation |
| Principal Investigator: |
King, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Computing |
| Organisation: |
University of Kent |
| Scheme: |
Standard Research |
| Starts: |
01 August 2016 |
Ends: |
30 September 2019 |
Value (£): |
199,130
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
14 Oct 2015
|
Singapore-UK Cyber Security
|
Announced
|
|
|
Summary on Grant Application Form |
The Automated Exploitation Grand Challenge lists a series of problems in vulnerability discovery.
One is finding whether it is possible to reach a required program (malicious)
state from a given state at an entry point. Another is how to infer states for the entry point which lead to the required state. An algorithmic answer to either would enable a security engineer to easily answer the question, ``is there a vulnerability at this point in the program?'' and if so, ``how can it be leveraged into an exploit?''
Since source is often unavailable to a security engineer, it is necessary to answer these questions by examining the binary executable alone. We will thus develop binary analyses
to address these two challenges, deploying interpolation-based reasoning on the first and abductive reasoning on the second.
The project will make both foundational and practical advances. We will develop new algorithms for bit-vector abduction and interpolation, that will have wide applicability. The algorithms will share common infra-structure and ideas, but offer a two-pronged approach to reachability.
We will deploy these algorithms in a vulnerability researchers' toolkit so as to enable a security engineer to compute a path to a (malicious) target state. We will then evaluate the tools on different classes of vulnerability using the Juliet Test Suite.
The project will employ one researcher at Kent and another at NUS for 32 months, building on the track records of Jaffar on interpolation, King on binary program analysis, and Chawdhary on engineering static analyses for commerce and industry.
|
|
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
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| 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 |