Static analysis is increasingly used to look for hidden defects in industrial software. The commercialization of tools like Coverity Prevent or CodeSonar, which have been shown to scale to large code bases and find real bugs, helped popularize static analysis technology among software developers.
However, in terms of software assurance this technology does not provide ground truth: all defect reports are mere warnings, which may turn out to be spurious (false positives), whereas real defects may go undetected (false negatives).
This class of static analyzers do not produce any strong evidence in support of the defects reported nor do they provide any metrics for calibrating false negatives.
But a theory devised more than 30 years ago and named Abstract Interpretation enables the construction of static analyzers that do not yield any false negatives.
Long considered to be impractical for analyzing real-life code, in recent years it has been successfully applied to the verification of large aerospace applications .
Customization is the key for achieving both scalability and low false positive rate: the abstraction interpretation algorithms are tailored for a special code or family of codes using knowledge of the application domain (software architecture, use of certain numerical algorithms, types of data structures manipulated, etc.).
We consider this evolution as a major step toward the use of static analysis as a process that can automatically assert ground truth on some important classes of software properties.
In this position paper, we advocate for the use of static analysis by abstract interpretation as a fully automated certification process for modern software assurance.
Abstract interpretation bridges a gap that standard software assurance techniques cannot address: certification standards like DO-178B are solely concerned with the development process, testing can only cover so many of all possible behaviors of the application in the field, and common static analysis tools do not provide evidence of the absence of defects.
To read this external content in full, download the paper from the archives at the U.S. Networking and Information Technology Research and Development (NITRD) agency..