Svace Static Analyzer. Finding critical program errors in production within secure development lifecycles

Svace Static Analyzer. Finding critical program errors in production within secure development lifecycles

Problem Statement

Software quality is significantly affected by source code defects that result in malfunctions and sometimes in malicious code execution. Finding defects became much more complex during the last 20 years due to extremely large program sizes reaching 10s-100s MLOCs. Many defect detection approaches have been introduced, and their application is regulated within established secure development lifecycles, such as Microsoft Security Development Lifecycle or Russian state standard GOST R 56939-2016.

One of the widely acknowledged detection methods is static source code analysis. Its advantages are as follows:

• Analysis of multiple execution paths simultaneously (i.e. scalability),
• Defect detection for rarely executed paths (that are hard to cover via testing or dynamic analysis).

The disadvantages are potentially false warnings about defects (false positives), which cannot be fully eliminated due to limitations of static analysis.

Svace Static Analysis Tool Collection

ISP RAS has developed Svace static analysis tool that satisfies all requirements for a production quality analyzer, namely:

1. Automatic analysis: fully automatic analysis workflow that requires minimal setup by the end user;
2. Scalability: programs of several MLOCs can be analyzed within a few hours (e.g. analysis of the complete Android 6 OS takes 5-6 hours);
3. Quality: high true positive rate (60-90% depending on the defect type);
4. Easy to understand: detailed explanation of each potential defect (textual description, defect location, events causing the defect along with their locations);
5. Results tracking: storing consecutive program analysis results in a database, GUI support for warnings review (true/false markup made by the user), comparing analysis runs, transferring existing warnings review to the new analysis results etc.

Svace supports C/C++, Java, and C# programming languages (C# can be also shipped separately as it is implemented as a standalone tool), and it runs on Linux and Windows. Svace analyzes programs that can be built on Intel x86/x86-64 Linux/Windows, ARM/ARM64 architectures. Popular C/C++ compilers for Linux and Windows are supported as well as a range of compilers for embedded systems.

Svace can find defects from a number of different defect classes (more than 50 in total), such as null pointer dereferences, memory management errors for dynamically allocated memory, buffer overflows, division by zero, resource and memory leaks, accessing uninitialized variables, locking errors. Furthermore Svace provides more than a hundred of lightweight checkers for various coding defects, API misuse and coding style violations.

Svace Applications

ISP RAS has been working on the basic research for static analysis technologies that have formed the Svace tool collection since 2002. In 2009 ISP RAS started a series of joint projects with Samsung Electronics to deploy Svace in Samsung's software development lifecycle. As a result, in 2015 Svace has been deployed in Samsung as the main static analysis tool, including its application for checking Samsung's own code based on Android and Tizen operating systems source code.

The latter is used in mobile phones, TVs, cameras and other products of the company. Also Svace is being extensively used in the internal projects of ISP RAS for code analysis.

All intellectual property rights for Svace tools belong to ISP RAS.

Svace Architecture and Workflow

Svace pipeline includes three major stages (similarly to other production static analyzers):

1. Building a program to be analyzed under tool monitoring

   Svace monitors regular program building process. When the monitoring subsystem detects compiler launches (for supported languages), it also runs own Svace compilers to generate internal intermediate representation for further analysis.

   

2. Analyzing the program

   The intermediate representation constructed on the previous stage is first processed by the lightweight language-specific analyzers that look for simple coding errors. After that, the main analysis engine starts. The engine constructs a program call graph and performs interprocedural context-sensitive (and for some checkers path-sensitive) analysis. This analysis is organized as a single call graph traversal such that callers are analyzed after callees. During intraprocedural analysis the engine creates a memory model and performs alias analysis, value analysis, etc. Function analysis results in creating its summary, a special data structure that contains all interesting “facts” about the analyzed function. The engine utilizes the summary when it processes calls to the function without revisiting its body.

   

   The main analysis engine consists of a core part and checkers for specific defect types. The core performs the most part of the analysis providing the checkers with various data such as the program memory model, its control and data flows, etc. Checkers may calculate additional attributes (program facts) using the APIs of the core. This allows achieving extensibility and scalability of the tool.

   To perform path-sensitive analysis the core calculates predicates for all considered paths. Path-sensitive checkers store conditions of "interesting" events specific to each checker. Using them along with a path predicate the checkers formulate the sufficient condition for defects on the considered path. Svace uses production level solver Z3 from Microsoft Research to check the satisfiability of the formulated defect conditions.

3. Viewing results

   Svace stores results of analysis in a database. We provide a graphical web-based interface to view them (see the picture). The interface allows marking the warnings as true or false positives and storing the review data, so that it is transferred to the following analysis runs of the same code automatically (see the picture).

Additional Svace features

Svace implements some usability features to smooth its integration within the development lifecycle. They include but not limited to:

• Support for running build and analysis stages on separate machines.
• Fast analysis support: when Svace reruns analysis of a small modified part of the program it takes into account earlier gathered analysis data for the big unchanged part. For instance, subsequent analysis of an Android application reuses the data from previous full analysis of the complete Android OS.
• Support for writing user lightweight checkers for C/C++ and Java.

Quality data

The table presents an example of Svace analysis results (true positives ratios) for the Android 5.0.2 source code.

Implementer

Compiler Technology