Compositional Security Analysis for Binaries
Lead Research Organisation:
Queen Mary University of London
Department Name: Sch of Electronic Eng & Computer Science
Abstract
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.
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.
Planned Impact
The research developed in this proposal will have strong impact on individuals and organizations
in charge of inspect and assess the security of binary code of real-world software such as:
- Security Engineers
- Intelligence/military organizations
The proposal will provide them with automatic tools able to detect or prove the absence of security vulnerability in binary code. These tools will also be useful to software developers as they will be able to check the binary code coming from the compilation of their programs.
In the long term this will impact software users and our society as we would count on more secure software infrastructures and applications. As our modern society and economy is highly dependent from the use of software systems, more secure software will translate in high economic impact as well as better quality of life.
in charge of inspect and assess the security of binary code of real-world software such as:
- Security Engineers
- Intelligence/military organizations
The proposal will provide them with automatic tools able to detect or prove the absence of security vulnerability in binary code. These tools will also be useful to software developers as they will be able to check the binary code coming from the compilation of their programs.
In the long term this will impact software users and our society as we would count on more secure software infrastructures and applications. As our modern society and economy is highly dependent from the use of software systems, more secure software will translate in high economic impact as well as better quality of life.
Publications
Pasareanu C
(2016)
Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT
Phan Q
(2015)
Concurrent Bounded Model Checking
in ACM SIGSOFT Software Engineering Notes
Phan Q
(2014)
Abstract model counting
Description | the use of bounded modelchecker cbmc for detecting leakage in system code and crypto library like OpenSSL |
Exploitation Route | Security analysis working at system code level |
Sectors | Digital/Communication/Information Technologies (including Software) |
Description | the findings from this research have informed work being done at GCHQ on automated code security analysis |
First Year Of Impact | 2015 |
Sector | Digital/Communication/Information Technologies (including Software) |
Impact Types | Policy & public services |