STING: Symbolic Tainting and Model Inference for Exploit Generation

• Applicant: Professor Dr. Falk Howar
• Subject Area: Software Engineering and Programming Languages ; Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: since 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 495857894

Software defines the infrastructure of the twenty-first century. Web applications in particular power a major part of this digital infrastructure, making their security paramount. Formal analysis of web application security, however, is difficult. Many ofthe known vulnerabilities tracked in the list of common vulnerability and exposures (CVEs) pertain to the flow of information throughweb applications from a potentially malicious source to a protected sink. Attacks typically exploit these data flows to distributemalicious code to sites it should not reach and execute it there.A mix of stateful and stateless programming paradigms, text-based protocols between layers, and multiple different programminglanguages in the layers make it hard to analyze the complete stack at once. Control flow and data flow cannot be computed on a single program graph but emerge from making sequences of requests against application endpoints with string-encoded data that may be stored in a persistence layer between requests.Existing analysis techniques for discovering vulnerabilities mostly fall into one of two classes: dynamic analyses execute web applications, providing inputs and requests and observing outputs. Dynamic analysis can provide witnesses but usually under-approximates the behavior of a system dramatically. Over-approximating static analysis techniques, on the other hand, compute information about program behavior and data flow on the source code of applications, mostly for individual requestmethods inside the business layer of an enterprise application. These analyses cannot provide witnesses for actual vulnerabilities and suffer from false positive alarms. Techniques from these groups target only a horizontal or only a vertical slice of applications.The goal of the STING project is to develop a precise, scalable, compositional, and automated formal analysis for checking thesecurity of multi-tier web-based applications. The envisioned analysis decomposes the analysis challenge into first generatingmodels of the individual layers and relevant 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 techniqueswill be used to compute behavior for sequences of requests, integrating generated models across the whole stack, analyzing thedata flow across multiple requests and through all layers.

• DFG Programme: Research Grants