To content
Fakultät für Informatik
STING

Symbolic Tainting and Model Inference for Exploit Generation

© Falk Howar​/​TU Dortmund

The goal of the STING project is to develop a precise, scalable, compositional, and automated formal analysis for checking the security of multi-tier web-based applications.

The envisioned analysis decomposes the analysis task into first generating models of the individual layers and parts of frameworks in the stack and then, in a second step, using these models to check for security vulnerabilities and to synthesize witnesses for identified vulnerabilities:

  • The persistence layer, e.g., involves external resources and will be analyzed using black-box learning techniques that produce models (e.g., register automata) of stateful behavior.
  • The business layer consists of containerized Java components  that will be analyzed through a combined concolic execution and taint analysis, allowing for exhaustive exploration of behavior and analysis of data-flow through the layer.

Finally, for checking the behavior of the application across layers, white-box model learning techniques will be used to compute behavior for sequences of requests, integrating generated models across the whole stack, analyzing the data-flow across multiple requests and through all layers. 

Funding

  • DFG