Copyright 2004,2005 Johannes Kinder [email protected]
Mocca (Model Checker for CTPL on Assembly code) is a prototype implementation of a CTPL model checker for verifying CTPL specifications on assembly files as produced by IDA Pro.
Mocca is intended for detecting malicious behavior in executables.
The example input files consist of several disassembled e-mail
worms, and the example specifications describe using Windows API
calls to copy the image of the running process to another
directory (usually windows/system32).
Use ./compile.sh to compile.
Run ./mocca.sh for a simple GUI, or ./moccac.sh for a command
line interface.
This is really old code I wrote for my Master's thesis in 2005, and I haven't looked at it for years. It is probably full of bugs, but I'm no longer maintaining it nor do I provide any support. I make it available purely for documenting the algorithm and experimental setup used in our DIMVA 2005 and TDSC 2010 papers.
If you use this code or parts of it in your own papers, please cite either:
- Kinder, J., S. Katzenbeisser, C. Schallhart, and H. Veith (Oct. 2010). Proactive Detection of Computer Worms Using Model Checking. In: IEEE Trans. Dependable Sec. Comput. 7(4), 424–438. DOI
and/or
- J. Kinder, S. Katzenbeisser, C. Schallhart, and H. Veith (2005). Detecting Malicious Code by Model Checking. In: Second Int. Conf. on Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA 2005). Vol. 3548. LNCS. Springer, pp.174–187. DOI