Macquarie University
01whole.pdf (361.58 kB)

Software verification techniques for malware detection

Download (361.58 kB)
posted on 2022-03-28, 17:43 authored by Robert Payne
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.


Table of Contents

1. Introduction -- 2. Background -- 3. Formal definitions for information leakage -- 4. Specifying leakages with program annotations -- 5. Software model checking for detecting leaks -- 6. Literature review -- 7. Conclusion -- Bibliography.


Bibliography: pages 51-57 Empirical thesis.

Awarding Institution

Macquarie University

Degree Type

Thesis MRes


MRes, Macquarie University, Faculty of Science and Engineering, Department of Computing

Department, Centre or School

Department of Computing

Year of Award


Principal Supervisor

Franck Cassez


Copyright Robert Payne 2019. Copyright disclaimer:




1 online resource (xvi, 57 pages)

Former Identifiers