About me

I am a research assistant and PhD student in the Formal Methods in Systems Engineering group of Prof. Veith at the Department of Informatics of the Technische Universität Darmstadt. My research interests include software model checking and Abstract Interpretation on low level code, disassembly, code obfuscation, and malicious code detection.

Teaching

Together with Visar Januzaj, I am coordinating the exercises for GdI 2 and ICS 2 in summer term 2010. All material will be distributed via the course platform. Registration is mandatory and will start after the first lecture, in which you will also get the enrollment key.

Please ask all questions regarding GdI 2 and ICS 2 in the forums of the course platform, the tutors and teachers will be happy to assist you there.

Contact

Dipl.-Inf. Johannes Kinder
Formal Methods in Systems Engineering
Technische Universität Darmstadt
Hochschulstr. 10
D-64289 Darmstadt
Germany

Room: E327
Building: S2|02
Phone: +49 6151 16-6167
Fax: +49 6151 16-7374
Email: kinder@cs.tu-darmstadt.de

Conference Papers

•  Johannes Kinder, Helmut Veith. Precise Static Analysis of Untrusted Driver Binaries. In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010), to appear.
  [ BibTeX ] 
   
•  Patrice Godefroid, Johannes Kinder. Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis. In Proceedings of the 19th International Symposium on Software Testing and Analysis (ISSTA 2010), pp. 1–11, July 2010.
  [ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 
   
• Johannes Kinder, Helmut Veith, Florian Zuleger. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009), Lecture Notes in Computer Science, vol. 5403, pp. 214–228, January 2009.
  [ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 
   
• Johannes Kinder, Helmut Veith. Jakstab: A Static Analysis Platform for Binaries. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), Lecture Notes in Computer Science, vol. 5123, pp. 423–427, July 2008.
  [ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 
   
• Andreas Holzer, Johannes Kinder, Helmut Veith. Using Verification Technology to Specify and Detect Malware. In Proceedings of the 11th International Conference on Computer Aided Systems Theory (EUROCAST 2007), Lecture Notes in Computer Science, vol. 4739, pp. 497–504, November 2007.
  [ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 
   
• Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith. Detecting Malicious Code by Model Checking. In Proceedings of the GI SIG SIDAR Conference on Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA 2005), Lecture Notes in Computer Science, vol. 3548, pp. 174–187, July 2005.
  [ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 
   

Journal Papers

• Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith. Proactive Detection of Computer Worms Using Model Checking. In IEEE Transactions on Dependable and Secure Computing, November 2008. Preprint.
  [ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 
   
• Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, Helmut Veith. Software Transformations to Improve Malware Detection. In Journal in Computer Virology, vol. 3, (4): pp. 253–265, November 2007.
  [ BibTeX ]  [ DOI ]  [ PDF ] 
   

Published Patent Applications

• WO/2009/014779: Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, Helmut Veith. System for Malware Normalization and Detection. January 2009.
  [ Link ] 
   

Technical Reports

• Patrice Godefroid, Johannes Kinder. Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis. Technical report, Microsoft Research, Redmond, WA, USA, November 2009.
  [ BibTeX ]  [ Link ] 
   
• Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, Helmut Veith. Malware Normalization. Technical report, University of Wisconsin, Madison, WI, USA, November 2005.
  [ BibTeX ]  [ PDF ] 
   

Theses

• Johannes Kinder. Model Checking Malicious Code. Diplomarbeit, Technische Universität München, 2005.
  [ BibTeX ]  [ PDF ]  [ PS ] 
   

Jakstab

Overview

Jakstab is an Abstract Interpretation-based, integrated disassembly and static analysis framework for designing analyses on executables and recovering reliable control flow graphs. It is designed to be adaptable to multiple hardware platforms using customized instruction decoding and processor specifications similar to the boomerang decompiler. It is written in Java, and in its current state supports x86 processors and 32-bit Windows PE or Linux ELF executables.

Jakstab translates machine code to a low level intermediate representation on the fly as it performs data flow analysis on the partial control flow graph. Data flow information is used to resolve branch targets and discover new code locations. Other analyses can either be implemented in Jakstab to run together with the main control flow reconstruction to improve precision of the disassembly, or they can work on the resulting preprocessed control flow graph.

Publications

We have a tool paper at CAV 2008 describing an early implementation of Jakstab:

Johannes Kinder, Helmut Veith. Jakstab: A Static Analysis Platform for Binaries. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), Lecture Notes in Computer Science, vol. 5123, pp. 423–427, July 2008.
[ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 

Our VMCAI 2009 paper gives a more detailed view of the theoretical background for optimal disassembly guided by data flow analysis:

Johannes Kinder, Helmut Veith, Florian Zuleger. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009), Lecture Notes in Computer Science, vol. 5403, pp. 214–228, January 2009.
[ BibTeX ]  [ DOI ]  [ PDF ]  [ PS ] 

Download

Since publication of the VMCAI paper, Jakstab has been completely rewritten towards a rigorous disassembly and analysis framework, where assumptions and heuristics can be controlled according to the application domain. I plan to make it publicly available on this website soon. Until then, if you would like further information, you can always write me an e-mail.