| EPSRC Reference: |
EP/K032011/1 |
| Title: |
Compositional Security Analysis for Binaries |
| Principal Investigator: |
Malacaria, Professor P |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Electronic Eng & Computer Science |
| Organisation: |
Queen Mary University of London |
| Scheme: |
Standard Research |
| Starts: |
30 August 2013 |
Ends: |
29 August 2016 |
Value (£): |
270,982
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
23 Jan 2013
|
EPSRC Research Institute APA & V
|
Announced
|
|
|
Summary on Grant Application Form |
Binaries are routinely inspected by the intelligence community, military organisations and security
engineers in their search for vulnerabilities. Binaries are often huge and therefore verification and
program analysis techniques should be scalable.
This project will pioneer compositional analyses for binary code. This will result in analyses
that are both modular and scalable.
The scientific challenge in compositional reasoning is how to separate intricate interactions, avoid
expensive operations such as quantifier elimination, and derive procedure summaries that are compact.
The project team will develop foundational techniques for the compositional analysis of binaries, testing
their viability with a running case study: the data santisation problem. Confidential data is sanitised when
its memory is zeroed before it is deallocated, preventing an attacker retrieving the sensitive information.
Data santisation is scientifically fascinating because of the need to track how secrets are passed
from one procedure to another and, in addition, how secrets are embedded into compound data-structures.
The problem is exacerbated by up-casting and down-casting, and the need to track the size
of a data object to ensure, for example, that all the elements of a buffer are properly zeroed.
|
|
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: |
|