Soundness checking boosts precision of taint flow models from AI
Soundness Checking of Taint Flow Models
Software Engineering
Summary
Finding errors when tracking unsafe data in code is hard, especially when code libraries are involved. The authors used an AI to guess how data flows through library methods, then checked these guesses carefully using special math and simple program checks to make sure they're accurate. This way, they avoid slow checks of the whole program while still catching almost all errors. Their approach works well on many real computer programs and keeps false alarms low.
What this means in practice
- •For software security teams: Automatically generate and verify accurate taint models to improve detection of data leaks and vulnerabilities in enterprise software libraries.
- •For software testing engineers: Reduce false positives in static taint analysis by using AI-crafted models that have been formally checked for soundness.
Authors
Samarth Kishor, Victor Nicolet, Joey Dodds
Abstract
Existing state-of-the-art static taint flow analyses for imperative programming languages can scale to large applications by using precise user-provided taint flow models of library methods. However, manually and precisely modeling a method's taint flows is tedious and potentially unsound. Furthermore, automatically modeling the method via an inter- procedural taint analysis can be inefficient. To solve this problem, we propose a guess-and-check approach: (1) an LLM agent that generates a precise taint flow model of a method and (2) a symbolic algorithm to check the soundness of the model. The algorithm deduces which taint flows must not occur in the method for the LLM's taint flow model to be sound, and uses lightweight static analyses (e.g., type system and pointer analysis) to prove these must-not-flows. When these analyses are insufficient, the algorithm deduces maximally-general callee models and recursively verifies their soundness, avoiding a full inter-procedural taint analysis in most cases. Since a more precise model requires fewer must-not-flows to be verified, the precision of the LLM's model directly determines the efficiency of our approach. We evaluate our approach on 97 LLM-generated taint flow models for methods in 6 large Go codebases and prove the models sound for 93% of the methods they cover. The proven-sound LLM-generated models are also precise, resulting in no new false-positives when proving taint flow properties.