BASIL: Binary Analysis of Secure Information-Flow Logics

This project is extending the state-of-the-art machine automation techniques to address challenges associated with software vulnerability analysis for uncontrolled supply chain targets.  We are building a demonstration tool called BASIL that can analyse Aarch64 binaries to ensure that there are no security vulnerabilities in the code.  The tool reads the binary, lifts it to a higher level and analyses it, then uses an automated SMT solver to verify security properties using an information-flow logic.  This project is pushing the boundaries of automation required to make such tools usable in practice and therefore scope for broad adoption. Automated vulnerability discovery of this nature can lead to the discovery of new classes of cyber vulnerabilities and zero-day exploits. Identification and protection against these vulnerabilities can keep Australia ahead in the cyber ‘arms-race’.