Our STARLITE (Static Analysis Architecture and Lifecycle Implementation, Test and Evaluation) project is a DHS-sponsored R&D activity under its Static Tool Analysis Modernization Project (STAMP), aimed at modernizing some of the open source tools already available to support the verification side of the software development lifecycle. The project started in September 2016.
The two main threads of activity for the first year include the development of new static analysis tool test suites and the characterization and selection of static analysis tool improvement candidates. Included in our test suite development, the goal of which is to enhance test case realism, will be the build-out of framework-related tests for Java applications, and the development of an innovative vulnerability injector for embedded system code. Included in our improvement candidate universe are some new and old open source static analysis tools, and the consideration of feature set enhancements for proprietary analysis tools.
Our Gold Standard project, formally A Gold Standard Method for Benchmarking C Source Code Static Analysis Tools, led to a concise formal definition of memory safety properties for C programs. We implemented an analyzer for these memory safety properties, which became our KT Advance product.
The project sponsor sought an innovative solution to the problem of evaluating static analysis tools. We focused on language-level vulnerabilities in the C programming language that allow a precise mathematical definition based on the standard C semantics We provided the mathematical foundation for identifying and localizing these types of weaknesses, relating these foundations to descriptions and formal definitions of 27 (of 32) CWEs covered, and describing our method for finding all code locations in a C program where they may occur, along with the formal proof obligations that we discharged at each such location to prove the definitive presence or absence of each weakness class. We chose to make this set of CWEs more precise by relating it to a single (abstract) instance of the violation of C language semantics concerning the storage integrity of variables. Our approach was to formally define this single notion of reference outside the storage type of a variable, characterize the locations in a C program where it can possibly occur (locations where the compiler cannot enforce its absence), and define the formal assertions of its absence that became proof obligations for analysis by abstract interpretation.
The procedure of identifying and locating memory-related vulnerabilities was the basis for evaluating the effectiveness of unsound static analysis tools, also known as bug finders, in terms of both false negatives and false positives. A scoring approach was based on six real-world programs for which analysis results were publicly available from several major tool vendors because these programs were part of the Static Analysis Tool Exhibition (SATE) program organized by the National Institute of Standards and Technology (NIST).