Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs

Abstract

We summarize the paper "Jaint: A Framework for User-Defined Dynamic Taint-Analyses Based on Dynamic Symbolic Execution of Java Programs", published at the sixteenth international conference on integrated formal methods in November 2020. Reliable and scalable methods for security analyses of Java applications are an important enabler for a secure digital infrastructure. In this paper, we present a security analysis that integrates dynamic symbolic execution and dynamic multi-colored taint analysis of Java programs, combining the precision of dynamic analysis with the exhaustive exploration of symbolic execution. We implement the approach in the Jaint tool, based on Jdart, a dynamic symbolic execution engine for Java PathFinder, and evaluate its performance by comparing precision and runtimes to other research tools on the OWASP benchmark set. The paper also presents a domain-specific language for taint analyses that is more expressive than the source and sink specifications found in publicly available tools and enables precise, CWE-specific specification of undesired data flows. This summary presents Jaint’s language and the evaluation.