Techniques for malware analysis based on symbolic execution

The landscape of malicious software, more commonly known as malware, grows every year in number, popularity and financial damage. Just like we see happening in the software industry, organizations in the cybercrime world are well coordinated: they hire developers, distributors, maintainers, they advertise their product, offering deployment services to paying customers and channels to signal bugs to fix. Manually examining every potentially malicious executable would be unfeasible to the least, therefore turning towards automated, fast analysis systems is becoming more and more a requirement to be efficient in the industry and offer meaningful results. To interfere with such automated techniques, malware developers will often hide meaningful routines activated only if certain conditions in the execution environment are met. These, in the literature called trigger conditions, become a great obstacle in automated analysis systems: specific dates, directory names or network commands that would expose the malicious nature of a sample will not most likely be triggered in a generic execution context without prior knowledge of their expected values, therefore leading to false negatives and, in general, to a decrease of the analysis coverage. Consequently, designing systems to expose hidden trigger conditions has drawn some interest in the reverse engineering and malware analysis literature. This thesis introduces Symba, a prototype based on symbolic execution that attempts to reveal trigger conditions in executables. Symbolic execution, precisely, is a software analysis technique which has been introduced in the literature a few decades of years ago but only recently -- thanks to an increasing attention from the scientific community -- is being practically adopted. Its rationale is to transform a binary executable into a set of symbols and equations binding them, which can be at any time mathematically solved to query the executable for interesting properties. In this work, we specifically resort to symbolic execution to handle the problem posed by trigger conditions. By extracting these conditions from both proof-of-concept and real world samples, consequently observing new paths of execution revealed in automated systems, we demonstrated how applying new analysis techniques, such as symbolic execution, on malware analysis can push a step forward towards more intelligent systems.