Searching for tainted vulnerabilities in static analysis tool Svace

The paper is dedicated to search for taint-based errors in the source code of programs, i.e. errors caused by unsafe use of data obtained from external sources, which could potentially be modified by an attacker. The interprocedural static analyzer Svace was used as a basis. The analyzer searches both for defects in the program and searches for suspicious places where the logic of the program may be violated. The goal is to find as many errors as possible at an acceptable speed and a low level of false positives (< 20–35%). To find errors, Svace with help of modified compiler builds a low-level typed intermediate representation, which is used as an input to the main SvEng analyzer. The analyzer builds a call graph and then performs summary-based analysis. In this analysis, the functions are traversed according to the call graph starting from the leaves. After analyzing the function, its summary is created, which will then be used to analyze the call instructions. The analysis has both high speed and good scalability. Intra-procedural analysis is based on symbolic execution with the union of states at merge points of paths. An SMT solver can be used to filter out infeasible paths for some checkers. In this case, the SMT-solver is called only if there is a suspicion of an error. The analyzer has been expanded to find defects of tainted data using. The checkers are implemented as plugins by using the source-sink scheme. The sources are calls of library functions that receive data from outside the program, as well as the arguments of the main function. Sinks are accessing to arrays, using variables as a step or loop boundary, calling functions that require checked arguments. Checkers covering most of the possible types of vulnerabilities for tainted integers and strings have been implemented. The Juliet project was used to assess the coverage. The false negative rate ranged from 46.31% to 81.17% with a small number of false positives.