What Is Sound Static Analysis?

Sound static analysis is a beneficial practice when developing software that needs to be safe, secure, and compliant. Here we discuss what makes sound analysis different, in terms of static analysis, why it is important, and how sound static code analysis works.

Read along or jump ahead to the section that interests you the most:

➡️ Sound static analysis Free Trial

What Is Sound Static Analysis?

Sound static analysis, or just sound analysis, refers to the true statement about the findings or “soundness” of the analysis results. For a static analysis tool to claim to provide sound analysis results, it means that if a specified bug, defect, or vulnerability is existing within a piece of software, then it will be reported by the tool.

In the case that the existence or non-existence is disputable then some form of warning will be provided*so that nothing can ‘slip through'.
(*Note: These are classed as Possible issues in Helix QAC and can be disabled if sound analysis is not required.)

Sound static analysis differs from other forms of static analysis where results are perhaps based on what is possible within a certain amount of time or resources.

Given that modeling the runtime behavior of a program requires certain approximations (e.g. lack of knowledge of program inputs, or OS state), sound analysis is required to be an over-approximation.

Over-approximations guarantee no false negatives (for a given kind of vulnerability), while under-approximations typically prioritize the absence of false positives.

Other forms of static analysis do not exhibit such strictness and may contain a mix of under- and over-approximations.

It is possible that the results from sound and unsound analysis tools will offer a clean bill of health for a particular part of a program, but a sound analysis engine is providing the additional assurance that all possibilities and all paths have been verified in reaching this conclusion.

How Sound Static Analysis Works

When referring to sound analysis, we are generally considering the more complex forms of inter- and intra-procedural control- and data-flow analysis, as found in most advanced static analysis tools today.

Rather than the more simplistic code syntax and semantic analysis, control- and data-flow static analysis is usually associated with the detection of more complex issues such as:

• Null Pointer De-Reference
• Array or Buffer Underflow and Overflow
• Use of an Uninitialized Object
• Memory Allocation and De-Allocation Anomaly
• Numeric Overflow, Underflow, and Wraparound
• Divide by Zero
• Dead Code
• Data Race, Deadlock, and Other Concurrency Violations

Control- and data-flow analysis is a computationally heavy task since all possible inputs to the system and all possible control-flow paths through the system must be considered. Indeed, brute-force exhaustive algorithms for control- and data-flow analysis lead to exponential analysis time and so are rarely ever suitable. However, more elegant options exist in the form of Symbolic Execution and Abstract Interpretation algorithms.

According to Abstract Interpretation, Symbolic Execution and Constraints  by Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey, “abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program.”

Whereas “symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program.” Both abstract interpretation and symbolic execution maintain constraints during execution, in the form of invariants or path conditions, which determine what possible paths can be executed and what values can be held within the various data sources.

Crucially, though, while abstract interpretation is sound, symbolic execution is not.

Why Is Sound Static Analysis Important?

Soundness is an important factor within safety-critical software systems, in particular, because it guarantees that the software does not contain any of the coding defects being checked for. That is, sound analysis can be used to show the absence of errors within a piece of software.

For this reason, abstract interpretation analysis is explicitly referenced as a method for software unit verification (Table 7, Method 1i) within the ISO 26262 functional safety (FuSa) standard for automotive systems.

How to Perform Sound Static Analysis with Helix QAC

For its ability to deliver in-depth and highly accurate analysis results, Helix QAC has been a trusted static code analysis tool for over 30 years. Able to perform sound static analysis, Helix QAC has been the preferred tool for tightly regulated and safety-critical industries that need to meet rigorous compliance requirements.

However, there are certain steps necessary in order to enable sound analysis within your Helix QAC projects:

Dataflow Depth needs to be set to the highest value (5), which will add several -prodoptions as seen in the above screenshot. (Please refer to Section “Analysis Timeout” in the QAC or QAC++ component manual for a discussion of why these “timeout” settings are mandatory for sound analysis.)

Additionally, ‘df::inter=5’ and ‘Inter TU Analysis’, while not required for sound analysis, can be enabled — at an additional computational cost — to reduce the amount of Possible issues that need to be reported. The effect of these settings is to enable inter- and intra-procedural analysis.

Why Choose Helix QAC for Sound Static Analysis

Experience firsthand the difference that Helix QAC sound static analysis can have on the quality and soundness of your code. Sign up for a free trial today.

➡️ Start Your Free Helix qac Trial