Model checking dataflow for malicious input

Ansgar Fehnker, Ralf Huuck, Wolf Rödiger

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

2 Citations (Scopus)


Many embedded systems today are no longer isolated control units, but are fully fledged miniature desktops with their own kernel and sometimes operating system networked with the outside world. This opens up a whole new set of security issues previously not known to embedded systems. One example is potentially malicious input that exploits source code weaknesses leading to critical mission failures. In this paper we propose a new automated malicious input detection approach that works on a staged application of traditional tainted dataflow analysis and syntactic software model checking. The advantages of this approach are that tainted data can be tracked from its source to its application point, a precise path through the source code can be computed, speed and precision can be custom-tuned by automated refinement, and the approach is flexible to deal with real-life security threats. We illustrate our approach with a number of analysis examples taken from existing open source C/C++ projects.
Original languageEnglish
Title of host publicationProceedings of the Workshop on Embedded Systems Security, WESS '11
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery (ACM)
Number of pages10
ISBN (Print)9781450308199
Publication statusPublished - 2011
Externally publishedYes
Event6th Workshop on Embedded Systems Security, WESS 2011 - Taipei, Taiwan
Duration: 9 Oct 201114 Oct 2011


Conference6th Workshop on Embedded Systems Security, WESS 2011


  • Command injection
  • Model checking
  • Security
  • Static analysis


Dive into the research topics of 'Model checking dataflow for malicious input'. Together they form a unique fingerprint.

Cite this