Logo des Repositoriums

Auflistung nach Schlagwort "SMT Solving"

1 - 2 von 2
  • Konferenzbeitrag
    Data-Driven Design and Evaluation of SMT Meta-Solving Strategies
    (Software Engineering 2022, 2022) Mues, Malte; Howar, Falk
    The 36th IEEE/ACM International Conference on Automated Software Engineering (2021) accepted the paper ‘Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and Cost’ [MH21a] and selected it for an ACM SIGSOFT Distinguished Paper Award. The paper presents four generally applicable patterns for the combination of multiple SMT decision procedures in a meta-solving strategy and demonstrates how a meta-solving strategy for string constraints can be developed in a data-driven approach based on these patterns: The paper cleans up and merges existing collections of SMT benchmarks in string theory solving to evaluate and compare derived meta-solving strategies. Notably, we can demonstrate on the available data that commonly used strategies as earliest returning SMT solver do not always return the most reliable result if all available SMT solvers are combined. Instead, cross-checking strategies work slightly better at moderate overhead.
  • Zeitschriftenartikel
    The Integration of Multi-Color Taint-Analysis with Dynamic Symbolic Execution for Java Web Application Security Analysis
    (Softwaretechnik-Trends Band 44, Heft 2, 2024) Mues, Malte
    The 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.