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.