Analysing compiled binaries using logic

Wednesday 3 October 12:00 - 12:30, Red room

Thais Moreira Hamasaki (F-Secure)

Computer security is a serious issue which attracts the interest of all nations. Malicious codes are implemented in such a way that they remain hidden during infection and operation, preventing their removal and the analysis of the code. The software used today to detect malicious code, such as anti-virus programs and firewalls, are problematic as there is a need for a version of the malicious program to be analysed prior to the detection itself.

The analysis process is necessary for these pieces of software to work with patterns extracted from the malware, called signatures. Furthermore, at least one computer system needs to get infected so that the code can be analysed. These kinds of software defences behave well when detecting known malware, but they provide no defence against new threat variants. The industry's approach still mostly relies on the well-known technique of signature matching.

Software analysis is a critical point in dealing with malware, since most samples employ some sort of packing or obfuscation techniques in order to thwart analysis. It is also an area of economic concern in protecting digital assets from intellectual property theft.

Analysis tools help analysts to identify vulnerabilities and issues before they cause harm downstream. Understanding how software and hardware can be secured using tools and techniques beyond standard debuggers and unit tests ensures higher security and integrity.

This presentation will provide an introduction to some practical applications of SMT solvers in IT security, investigating the theoretical limitations and practical solutions, focusing on their use as a tool for binary static analysis.

SMT-based implementations I have worked on before include: a binary garbage-code eliminator for malware analysis, a XOR search and some cryptographic algorithm breakers. SMT-based implementations on which I am currently working include: a generic unpacker, a binary structure recognizer and a C++ class hierarchy re-constructor.

Thaís Moreira Hamasaki

Thaís is a malware researcher who focuses on static analysis, reverse engineering and logical programming. She started her career within the anti-virus industry working on data and malware analysis, where she developed her knowledge on threat protection systems. She won the "best rookie speaker" award from BSides London for her first talk about "Using SMT solvers to deobfuscate malware binaries". Recent research topics include binary code deobfuscation, generic unpacking and static analysis automation, and tool development. She is a proud member of the Düsseldorf Hackerspace, where she also leads the groups for reverse engineering and x86 Assembly. In her free time, you can find Thaís building static analysis tools, cooking or climbing somewhere offline.

@barbieauglend