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.

情报界，军事组织和安全工程师通常会检查二进制文件，以寻求脆弱性。二进制文件通常是巨大的，因此验证和程序分析技术应该是可扩展的。该项目将开创二进制代码的组成分析。这将导致既有模块化又可扩展的分析。组成推理的科学挑战是如何分离复杂的相互作用，诸如量化器消除等诸如量化的avoIdexpitive操作，并得出了紧凑的程序摘要。项目团队将开发基础技术，以对双线性进行组成分析，以综合案例研究来研究案例研究。机密数据在将其记忆归零之前将其归零时被消毒，以防止攻击者检索敏感信息。Datasantisation在科学上令人着迷，因为需要跟踪秘密是如何通过一个程序传递到另一个过程的，而且，此外，以及如何将秘密的秘密嵌入到更高的数据结构中，并逐渐逐渐逐渐形成，并逐渐逐渐逐渐形成，并逐渐逐渐逐渐逐渐构成，并逐渐逐渐逐渐形成逐渐形成，并逐渐逐渐逐渐逐渐形成，并且可以逐渐逐渐形成，并且逐渐逐渐逐渐逐渐逐渐形成，并且逐渐逐渐逐渐逐渐逐渐变化。例如，确保对缓冲区的所有元素进行正确的归零。

项目成果

Concurrent Bounded Model Checking

• DOI: 10.1145/2693208.2693240
• 发表时间: 2015-02
• 期刊: ACM SIGSOFT Softw. Eng. Notes
• 作者: 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)
• 作者: C. Păsăreanu;Quoc-Sang Phan;P. Malacaria

Abstract model counting

抽象模型计数

• DOI: 10.1145/2590296.2590328
• 发表时间: 2014
• 作者: 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
• 作者: Quoc-Sang Phan;P. Malacaria