Symbolic Tainting and Model Inference for Exploit Generation
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