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.