Searching for Taint Vulnerabilities with Svace Static Analysis Tool

This paper is dedicated to finding taint-based errors in the source code of programs, i.e., errors caused by unsafe use of data from external sources, which could potentially be modified by a malefactor. The interprocedural static analyzer Svace is used as a basis. The analyzer searches for both program defects and suspicious points where the logic of the program may be corrupted. The goal is to find as many errors as possible at an acceptable speed and low false positive rate (<20-35%). For this purpose, Svace builds, with the help of a modified compiler, a low-level typed intermediate representation, which is input to the main SvEng analyzer. The analyzer constructs a call graph and then carries out summary-based analysis. In this analysis, functions are traversed according to the call graph, starting from the leaves. Once a function is analyzed, its summary is created, which is then used to analyze call instructions. The analysis has both high speed and good scalability. Intraprocedural analysis is based on symbolic execution with state merging at join points. An SMT solver can be used to filter out infeasible paths for some checkers. In this case, the SMT solver is called only if an error is suspected. The analyzer has been extended to find defects of tainted data use. The checkers are implemented as plugins based on the source-sink scheme. The sources are calls of library functions that receive data from the outside of the program, as well as arguments of the main function. The sinks are accesses to arrays, uses of variables as steps or loop boundaries, and calls of functions that require checked arguments. Checkers that cover most of possible vulnerabilities for tainted integers and strings are implemented. To assess the coverage, the Juliet project is used. The false negative rate ranges from 46.31% to 81.17% with a small number of false positives.