The integration of multi-color taint-analysis with dynamic symbolic execution for Java web application security analysis

Abstract

The view of IT security in today’s software development processes is changing. While IT security used to be seen mainly as a risk that had to be managed during the operation of IT systems, a class of security weaknesses is seen today as measurable quality aspects of IT system implementations, e.g., the number of paths allowing SQL injection attacks. Current trends, such as DevSecOps pipelines, therefore establish security testing in the development process aiming to catch these security weaknesses before they make their way into production systems. At the same time, the analysis works differently than in functional testing, as security requirements are mostly universal and not project specific. Further, they measure the quality of the source code and not the function of the system. As a consequence, established testing strategies such as unit testing or integration testing are not applicable for security testing. Instead, a new category of tools is required in the software development process: IT security weakness analyzers. These tools scan the source code for security weaknesses independent of the functional aspects of the implementation. In general, such analyzers give stronger guarantees for the presence or absence of security weaknesses than functional testing strategies. In this thesis, I present a combination of dynamic symbolic execution and explicit dynamic multi-color taint analysis for the security analysis of Java web applications. Explicit dynamic taint analysis is an established monitoring technique that allows the precise detection of security weaknesses along a single program execution path, if any are present. Multi-color taint analysis implies that different properties defining diverse security weaknesses can be expressed at the same time in different taint colors and are analyzed in parallel during the execution of a program path. Each taint color analyzes its own security weakness and taint propagation can be tailored in specific sanitization points for this color. The downside of dynamic taint analysis is the single exploration of one path. Therefore, this technique requires a path generator component as counterpart that ensures all relevant paths are explored. Dynamic symbolic execution is appropriate here, as enumerating all reachable execution paths in a program is its established strength. The Jaint framework presented here combines these two techniques in a single tool. More specifically, the thesis looks into SMT meta-solving, extending dynamic symbolic execution on Java programs with string operations, and the configuration problem of multi-color taint analysis in greater detail to enable Jaint for the analysis of Java web applications. The evaluation demonstrates that the resulting framework is the best research tool on the OWASP Benchmark. One of the two dynamic symbolic execution engines that I worked on as part of the thesis has won gold in the Java track of SV-COMP 2022. The other demonstrates that it is possible to lift the implementation design from a research specific JVM to an industry grade JVM, paving the way for the future scaling of Jaint.