The integration of multi-color taint-analysis with dynamic symbolic execution for Java web application security analysis
Loading...
Date
2023
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
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.
Description
Table of contents
Keywords
Dynamic symbolic execution, Formal verification of Java, Taint analysis