Detecting Malicious Code by Model Checking

The ease of compiling malicious code from source code in higher programming languages has increased the volatility of malicious programs: The first appearance of a new worm in the wild is usually followed by modified versions in quick succession. As demonstrated by Christodorescu and Jha, however, classical detection software relies on static patterns, and is easily outsmarted. In this paper, we present a flexible method to detect malicious code patterns in executables by model checking. While model checking was originally developed to verify the correctness of systems against specifications, we argue that it lends itself equally well to the specification of malicious code patterns. To this end, we introduce the specification language CTPL (Computation Tree Predicate Logic) which extends the well-known logic CTL, and describe an efficient model checking algorithm. Our practical experiments demonstrate that we are able to detect a large number of worm variants with a single specification.

Published in:
Proc. 2nd Int. Conf. Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA 2005), 174-187
Presented at:
Detection of Intrusions and Malware, and Vulnerability Assessment, Vienna, Austria, July 7-8, 2005
Berlin, Heidelberg, Springer

 Record created 2011-07-13, last modified 2018-09-13

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)