Transforming Taint to Typestate Specifications

Bachelor/Master Thesis


Taint analysis is a popular method in data flow analysis that is nowadays extensively used to detect many taint-style vulnerabilities, such as data leaks in Android [2]. This analysis tracks the sensitive information provided by a so called “source”(i.e., a method that returns sensitive data) in the code (Line 1 in Figure 1), and reports an error if it reached a security-critical statement so called “sink”(i.e., usually a method that passes its input to the outside) in the code (Line 3 in Figure 1). A taint analysis will keep information about the facts that are propagated as each line (middle part in Figure 1). 


On the other hand, a typestate analysis [3] can be used for detecting more complex security vulnerabilities where a single object being tracked can have multiple states, e.g. checking a file object being initialized, opened, or closed. This analysis uses a state machine to model the possible state of each object. As shown in Figure 1 on the right, a taint analysis can be expressed as a typestate problem where the state machine has two states: tainted and untainted.


Multiple specification languages have been suggested to declaratively model these different kinds of analyses. Your task is to develop a transformer between two state-of-the-art languages, CrySL, which may express type-state properties, and QWEL, a language for succient taint-analysis specifications.



  • Design and implement a transformation from a taint specifications in the QWEL language[*] to a typestate specifications in the CrySL language [1]
  • [for master] Evaluate the approach



Required skills:

  • Programming experience (preferably Java)
  • Self-organization
  • Design of Domain Specific Languages and Eclipse Modeling Framework



Learning outcomes:

  • Apply knowledge from relevant literature
  • Gain deep understanding of taint analysis and typestate analysis
  • Gain knowledge in model to model transformation
  • Plan, implement, test, and document an independent research project 


Goran Piskachev (

Stefan Krüger (




1 CrySL:

2 Taint analysis:

3 Typestate analysis:

[*] A meta-model for taint specifications will be provided