Testing Static Taint Analyzers with Equivalence Modulo Taint

Abstract

Static taint analyzers are widely used to detect security vulnerabilities, yet their complexity makes them prone to soundness and precision issues. Validating these analyzers is challenging because ground-truth taint flows are rarely available and differential testing requires multiple comparable tools. To address this challenge, we introduce Equivalence Modulo Taint (EMT), a testing oracle for static taint analysis that defines program equivalence in terms of preserved source-sink flows rather than program semantics. EMT enables testing a single analyzer without ground-truth labels by checking consistency of reported flows across equivalent-modulo-taint program variants. Based on EMT, we present TaintCC, a framework that generates equivalent-modulo-taint variants through semantically equivalent, taint-oblivious, and taint-aware transformations targeting recurring difficulty dimensions in taint analysis. We evaluate TaintCC on four widely used analyzers---FlowDroid, Mariana Trench, Pysa, and Semgrep---and uncover 16 unique developer-confirmed issues, showing that even mature analyzers, whether academic or industrial, remain susceptible to reliability issues.