Reference:

Johannes Kinder. Model checking malicious code. Master's thesis, Technische Universität München, 2005.

Abstract:

Recent years have seen a dramatic increase of security incidents on the Internet related to e-mail worms. These particular pieces of malicious code are often developed by mischievous teenagers and are not very skillfully engineered, but still spread globally in a matter of minutes and cause a large amount of economic damage.

Conventional anti-virus products nowadays still rely on static pattern matching. They do not detect a new worm variant as long as the binary representation is sufficiently different, even if the functionality of the worm has not significantly changed. As a result, e-mail worms remain undetected during the phase of their initial outbreak, successfully reaching hundreds of thousands of mailboxes.

In this thesis, a novel contribution to the field of semantic malware detection is presented. This approach employs model checking, a well proven formal verification method, to find behavioral patterns inside an executable. In particular, the new temporal specification logic CTPL is introduced, which allows a succinct representation of program behavior on assembler level. A specialized model checking algorithm for CTPL allows efficient validation of disassembled executables against malicious code specifications.

In the course of this thesis, the CTPL model checking algorithm has been implemented in the Java programming language. Two exemplary specifications of malicious behavior are created and tested with the prototype on a set of current e-mail worms as well as on benign programs. The positive results prove CTPL model checking to be a very promising approach for the sophisticated detection of viruses and worms.

Suggested BibTeX entry:

@mastersthesis{da-kinder,
    author = {Johannes Kinder},
    school = {Technische Universit\"at M\"unchen},
    title = {Model Checking Malicious Code},
    year = {2005}
}