Detecting Malicious Code by Model Checking (bibtex)
by Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
Abstract:
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.
Reference:
Detecting Malicious Code by Model CheckingJohannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut VeithGI SIG SIDAR Conference on Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA'05) (Klaus Julisch, Christopher Krügel, eds.), volume 3548 of Lecture Notes in Computer Science, pages 174-187, July 2005, Springer.
Bibtex Entry:
@inproceedings{KinderKatzenbeisserSchallhartVeith-mcodedimva05,
  author = {Johannes Kinder and Stefan Katzenbeisser and Christian Schallhart and   Helmut Veith},
  title = {Detecting Malicious Code by Model Checking},
  month = {July},
  year = {2005},
  address = {Vienna, Austria},
  booktitle = {GI SIG SIDAR Conference on Detection of Intrusions and Malware \&   Vulnerability Assessment (DIMVA'05)},
  editor = {Klaus Julisch and Christopher Kr{\"u}gel},
  pages = {174--187},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3548},
  abstract = {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.},
  isbn = {3-540-26613-5},
  url = {http://dx.doi.org/10.1007/11506881\_11}
}
Powered by bibtexbrowser