Description
Integer overflows are common software errors, which can lead to severe security- and safety-critical consequences.
Especially when buying commercial-of-the-shelf software, one cannot rely on the program binary to be free of these
vulnerabilities. Static binary analysis methods in the field of formal verification aim to avoid vulnerabilities
such as those introduced by integer overflows and offer the possibility for independent software verification.
To our knowledge, there exists no single study applying formal verification methods directly to ARM binaries to
specifically address integer overflows. The ARM architecture is highly relevant with its large market share in key
technology sectors. In this thesis, we believe we make an impactful contribution towards providing formal verification
tools with our proof-of-concept implementation called AbsInt. It implements intra-procedural abstract interpretation to
show the absence of integer overflows in ARM binaries. Our approach includes a direct mapping of assembly to the abstract
representation in form of a control flow graph (CFG) without an intermediate step such as a translation to an intermediate
representation (IR). To have a greater coverage of processor instructions for this mapping, we extend the well-known theory
of abstract operators. We add definitions of the bit-wise logical instructions AND, OR, and XOR for interval arithmetic and
prove their applicability. On the CFG, we perform range analysis for the intervals of program variables to detect potential
integer overflows. As a formal method, our approach can prove that a program is free of integer overflows or provides a
warning if the over-approximation detects a potential overflow.
Using AbsInt, we analyzed a subset of the NIST Juliet Test Suite C/C++ including integer overflow-oriented, intra-procedural
test cases. Our test results support the theoretical discussion with a false-negative rate of 0. Depending on the techniques
used in the test set, we can achieve a recall of up to 0.98 for proving that no integer overflows exist, and a precision of up
to 0.94 for detecting integer overflows. These results encourage the usage of a direct mapping to the CFG without an IR to perform
abstract interpretation on ARM binaries.
|
Thesis topic in co-operation with the Fraunhofer Institute for Applied and Integrated Security AISEC, Garching