BackFlow: backward context-sensitive flow reconstruction of taint analysis results. (English) Zbl 07228500

Beyer, Dirk (ed.) et al., Verification, model checking, and abstract interpretation. 21st international conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11990, 23-43 (2020).
Summary: Taint analysis detects if data coming from a source, such as user input, flows into a sink, such as an SQL query, unsanitized (not properly escaped). Both static and dynamic taint analyses have been widely applied to detect injection vulnerabilities in real world software. A main drawback of static analysis is that it could produce false alarms. In addition, it is extremely time-consuming to manually explain the flow of tainted data from the results of the analysis, to understand why a specific warning was raised. This paper formalizes BackFlow, a context-sensitive taint flow reconstructor that, starting from the results of a taint-analysis engine, reconstructs how tainted data flows inside the program and builds paths connecting sources to sinks. BackFlow has been implemented on Julia’s static taint analysis. Experimental results on a set of standard benchmarks show that, when BackFlow produces a taint graph for an injection warning, then there is empirical evidence that such warning is a true alarm. Moreover BackFlow scales to real world programs.
For the entire collection see [Zbl 1429.68006].


68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI