Mues, MalteHerrmann, Andrea2024-07-262024-07-262024https://dl.gi.de/handle/20.500.12116/44197The view on IT security in today’s software develop ment processes is changing. While IT security used to be seen mainly as a risk that had to be man aged during the operation of IT systems, a class of security weaknesses is seen today as measurable qual ity aspects of IT system implementations, e.g., the number of paths allowing SQL injection attacks. In consequence, we need tools that can measure and as sess the quality of an IT system regarding the pres ence of security weaknesses before shipping the final software product. Literature traditionally categorizes such tools into dynamic and static security analyzers with hybrid solutions in between that are static anal yses incorporating dynamic information or vice versa. In my thesis, I present the design of a dynamic se curity analyzer called Jaint that combines dynamic tainting as a pathwise security policy enforcing tech nique with dynamic symbolic execution as a path enu meration technique. 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 anal ysis of Java web applications. The evaluation in Fig ure 1 demonstrates that the resulting framework is the best research tool on the OWASP Java Benchmark. JDart, 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. GDart, the other dynamic symbolic execution engine, demon strates that it is possible to lift the implementation design from the research-specific Java PathFinder VM to the industry grade GraalVM, paving the way for the future scaling of Jaint.enDynamic Symbolic ExecutionAutomated Software TestingSMT SolvingIT SecurityMulti-Color Taint AnalysisSoftware EngineeringSoftware VerificatioText/Journal Article