SATE V Ockham Sound Analysis Criteria

Published

March 22, 2016

Author(s)

Paul E. Black, Athos Ribeiro

Abstract

Static analyzers examine the source or executable code of programs to find problems. Many static analyzers use some heuristics or approximations to handle programs up to millions of lines of codes. We established the Ockham Sound Analysis Criteria to recognize static analyzers whose findings are always correct. In brief the criteria are (1) the analyzer's findings are claimed to always be correct, (2) it produces findings for most of a program, and (3) even one incorrect finding disqualifies an analyzer. This document begins by explaining the background and requirements of the Ockham Criteria in more detail. In Static Analysis Tool Exposition (SATE) V, one tool, Frama-C, examined pertinent parts of the Juliet 1.2 test suite to participate. We reviewed eight classes of warnings, including improper buffer access, NULL pointer dereference, integer overflow, and others. This document details the many technical and theoretical challenges we addressed to classify and review the warnings against the Criteria. It also reports anomalies, our observations, and interpretations. Frama-C reports led to the discovery of three unintentional, systematic flaws in the Juliet test suite involving 416 test cases. Our conclusion is that Frama-C satisfied the SATE V Ockham Sound Analysis Criteria.

Citation

NIST Interagency/Internal Report (NISTIR) - 8113

Report Number

8113

NIST Pub Series

NIST Interagency/Internal Report (NISTIR)

Pub Type

NIST Pubs

Download Paper

https://doi.org/10.6028/NIST.IR.8113

Keywords

software assurance, sound analysis, static analysis, Ockham Criteria

Citation

Black, P. and Ribeiro, A. (2016), SATE V Ockham Sound Analysis Criteria, NIST Interagency/Internal Report (NISTIR), National Institute of Standards and Technology, Gaithersburg, MD, [online], https://doi.org/10.6028/NIST.IR.8113 (Accessed December 26, 2024)