PI: Andy King, University of Kent
- We have developed new analysis techniques that are able to correctly handle machine arithmetic for integers of various width.
- This is crucial for reasoning about how paths can be taken, and cannot be taken, through binary programs.
- Our approach allows the model checker itself to be verified by using a classic bit-vector solver, which does not need to support interpolation.
The project focuses on the problem of how to automatically compare two AVR binaries. Using one given binary as the reference semantics, the problem is to determine whether the other binary has the same behaviour (even if it syntactically different), or whether it has been tampered with. We use interpolation-based model-checking to search for a path in one binary which does not exist in the other.
We have developed a new interpolation method for bit-vector formulae by leveraging on existing interpolation techniques for linear integer arithmetic, and integrated this method into the Impact interpolation algorithm, demonstrating how it improves on interpolation techniques which do not reason about the wrap-around nature of machine arithmetic. Interpolation is used to relax a sequence of symbolic formulae which represent a path through a program to give a more general sequence that describes, not just one path, but many.
We have also shown how interpolant methods can be extended beyond systems of linear constraints, and also how to take an interpolant which is a system of linear inequalities and always encode it as a compact bit-vector formula. We have improved an existing interpolation algorithm for bit-vectors by adapting computer algebra techniques to work over modulo arithmetic rather than the field of real numbers. Paradoxically, modulo arithmetic makes it easier, not harder, to automatically reason about the behaviour of the program.
Our analysis work is built on atop a tool-chain for decompiling AVR binaries which is, in turn, build on the QEMU toolkit for emulating various architectures. While undertaking our project, we have made contributions to the AVR support for QEMU, both making it both more robust and extending its functionality.
This research is of key importance to AWE’s work on treaty verification in an arms control context. It will provide tools and techniques to verify the authenticity of monitoring equipment that could be deployed for future arms control treaties.
PUBLICATIONS. [1] Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic, T. Okudono and A. King, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’20); (2) Polynomial Analysis of Modulo Arithmetic, T. Seed, C. Coppins, A. King and N. Evans (under review); [3] Improved AVR support for QEMU, S. Harris, E. Robbins (signed off by M. Rolnik), https://lists.sr.ht/~philmd/qemu/, 2019.
RELATED GRANTS. Atomic Weapons Establishment. Follow-on funding, Dec 2019–Apr 2020, £20K.
IMPACT. “As a professional reverse engineer and binary analysis tool developer with 16 years of experience, I believe that the future of binary analysis lies in the further adoption and advancement of techniques in mathematical program analysis. In my estimation, the research group at the University of Kent is one of the only remaining groups – certainly the most prolific one – that is regularly attempting to tackle the theoretical issues plaguing the scalability of binary analysis. Not only are they “attempting” to tackle these issues, they have published a number of deep and fascinating papers, which offered truly novel contributions to binary analysis.” – Rolf Rolles, Möbius Strip Reverse Engineering –
