Sansa

The Sansa project (Static Analysis for Security Audits) developed static analysis technologies for security audits of Java programs. The system includes two coveted static analysis systems for Java programs: 1) string subcomponent taint and value analysis, and 2) high-level functionality queries. The combined system provides novel capabilities that substantially increase the precision, accuracy, and throughput of pre-install security auditing of Java-based programs (including Android applications).

String Subcomponent Taint and Value Analysis

We developed an automated static analysis for Java programs that precisely determines possible run-time values and untrusted components of strings. The analysis tracks the source taint (trusted or untrusted) of each subcomponent used to create a string. Untrusted strings are those that are derived from untrusted inputs (such as a network connection)

Furthermore, the analysis reasons about how a string’s untrusted components are sanitized or escaped with respect to a given command language (such as Structured Query Language (SQL)).  To achieve additional precision, the analysis accounts for how checks of a string along execution paths constrain the possible values of the string. The analysis is flow and context-sensitive, which is required to analyze common string sanitization and checking code.  We have successfully evaluated the system on a variety of SQL programs, and it was able to find almost all vulnerabilities with limited false positives. Furthermore, it was able to provide detailed information provenance for each string subcomponent, allowing a user to easily verify and repair vulnerabilities.

High-Level Functionality Queries:

We also built a toolkit to help an analyst understand the functional behavior of code segments of interest, by answering questions and extracting facts about the code, including specifications of code behavior. The tool helps analyze tricky segments of code, including those suspected of being incorrect or malicious. It supports reasoning about application-specific behaviors, such as “Can adding a waypoint to a route decrease the total computed time for the route?”. (A malicious route-finding application can add waypoints that take “negative” time, causing the user to take bad routes.) If the answer to such a yes/no question is yes, the tool can often produce a concrete input (using the SMT solver) that drives the program to the behavior of interest. The tool also supports scenario-based questions such as “What happens when X is negative?”. In this case, the tool extracts a specialized behavior specification for the given situation. This makes the extracted specification more straightforward and more understandable.