Vulnerability Discovery using Abduction and Interpolation
Lead Research Organisation:
University of Kent
Department Name: Sch of Computing
Abstract
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.
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.
Planned Impact
For maximal academic impact, we will publish our
outputs in leading international
conferences, whilst augmenting these results with
archival journal publications. We will also distribute our
research prototypes with an open source license, partly to encourage
take up of the ideas, and partly to make IPR transparent
if a third-party wishes to spin-out the ideas
into a commercial product.
outputs in leading international
conferences, whilst augmenting these results with
archival journal publications. We will also distribute our
research prototypes with an open source license, partly to encourage
take up of the ideas, and partly to make IPR transparent
if a third-party wishes to spin-out the ideas
into a commercial product.
Publications
Chawdhary A
(2016)
Incrementally Closing Octagons
Chawdhary A
(2017)
Compact Difference Bound Matrices
Howe J
(2019)
Incremental Closure for Systems of Two Variables Per Inequality
in Theoretical Computer Science
Howe J, King A And Simon A
(2018)
Incremental Closure for Systems of Two Variables Per Inequality
in Theoretical Computer Science
Liñares M.C.
(2016)
OpenAccess Series in Informatics: Preface
in OpenAccess Series in Informatics
ROBBINS E
(2020)
Backjumping is Exception Handling
in Theory and Practice of Logic Programming
Takamasa Okudono
(2020)
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
| Description | We developed techniques to scale the application of abstract interpretation to large programs. In particular, we developed memory-efficient representation of a widely-used abstract domain and demonstrated how they made analysis tractable. |
| Exploitation Route | Memory-efficient representations of abstract domains which can be used in either forwards *or* backwards analysis. |
| Sectors | Aerospace Defence and Marine |
| Description | The methodology that we applied in our work, that is, abstract a program as a finite graph, using data-abstractions to induce finiteness, has also been mapped over a different setting of deciding subtyping by abstracting a bi-simulation of a candidate subtype against a proposed supertype, again with a finite graph. This has been applied to solve subtyping problems that were previously out of reach. Deciding subtyping in a fundamental problem in concurrency, compiling and verification. |
| First Year Of Impact | 2023 |
| Sector | Other |
| Impact Types | Economic |