Compositional Security Analysis for 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.