Software verification techniques for malware detection

Information leakage is the undesired output of information from a program that reveals the value or nature of a piece of private information that should not be shared. Detecting information leakage is a problem that has been approached using methods including taint tracking and analysis which deals with the marking of private data in a program and tracking its flow to detect if that flow is connected to an undesired output. In this thesis, a technique is presented to specify information leaks in programs with regard to assertions (program annotations) and demonstrate that this technique can be used to unveil common information leakage using current software verification tools. This method is then compared with information leakage examples from current publications and current taint analysis benchmarks for detecting information leakage to demonstrate its effectiveness. Motivation for this work is driven by a need for a formal method for defining and encoding leaks through program annotation, that leads to more effective future work into accurately detecting information leakage, both in malicious programs (malware) and unintentional leaking programs.