Compositional Security Analysis for Binaries

二进制文件的组成安全分析

基本信息

批准号：
EP/K032011/1
负责人：
Pasquale Malacaria
金额：
$ 34.53万
依托单位：
Queen Mary University of London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2013
资助国家：
英国
起止时间：
2013 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FK032011%2F1
关键词：
Compositional Security Analysis Binaries

项目摘要

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, avoidexpensive 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 passedfrom 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 sizeof a data object to ensure, for example, that all the elements of a buffer are properly zeroed.

情报界，军事组织和安全工程师通常会检查二进制文件，以寻求脆弱性。二进制文件通常是巨大的，因此验证和程序分析技术应该是可扩展的。该项目将开创二进制代码的组成分析。这将导致分析既是模块化又可扩展的。组成推理的科学挑战是如何分离复杂的相互作用，诸如量化器消除量之类的avoIdexlist强度操作，并得出紧凑的程序摘要。项目团队将开发成分技术的基础技术分析二进制文件，通过运行的案例研究测试其生存能力：数据隐性问题。机密数据在记忆之前将其记忆归零时进行消毒进入复合数据结构。问题通过上调和下调加剧，并且需要跟踪数据对象的尺寸以确保例如，缓冲区的所有元素都会正确归零。

项目成果

期刊论文数量（6）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Concurrent Bounded Model Checking

DOI：
10.1145/2693208.2693240
发表时间：
2015-02
期刊：
ACM SIGSOFT Softw. Eng. Notes
影响因子：
0
作者：
Quoc-Sang Phan;P. Malacaria;C. Păsăreanu
通讯作者：
Quoc-Sang Phan;P. Malacaria;C. Păsăreanu

Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT

DOI：
10.1109/csf.2016.34
发表时间：
2016-08
期刊：
2016 IEEE 29th Computer Security Foundations Symposium (CSF)
影响因子：
0
作者：
C. Păsăreanu;Quoc-Sang Phan;P. Malacaria
通讯作者：
C. Păsăreanu;Quoc-Sang Phan;P. Malacaria

Abstract model counting

抽象模型计数

DOI：
10.1145/2590296.2590328
发表时间：
2014
期刊：
影响因子：
0
作者：
Phan Q
通讯作者：
Phan Q

All-Solution Satisfiability Modulo Theories: Applications, Algorithms and Benchmarks

DOI：
10.1109/ares.2015.14
发表时间：
2015-08
期刊：
2015 10th International Conference on Availability, Reliability and Security
影响因子：
0
作者：
Quoc-Sang Phan;P. Malacaria
通讯作者：
Quoc-Sang Phan;P. Malacaria