Transforming Taint to Typestate Specifications

Bachelor/Master Thesis

Description:

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.

Goal

 

  • 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 

Contact:

Goran Piskachev (goran.piskachev@iem.fraunhofer.de)

Stefan Krüger (stefan.krueger@upb.de)

 

References

 

1 CrySL: https://bodden.de/pubs/ksa+18crysl.pdf

2 Taint analysis: https://www.bodden.de/pubs/far+14flowdroid.pdf

3 Typestate analysis: https://bodden.de/pubs/sab17ideal.pdf

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