| Projects and Workshops | |
| SAMATE | NIST Software Assurance Metrics and Tool Evaluation Project |
|---|---|
| BugWorkshop05 | Workshop on the Evaluation of Software Defect Detection Tools |
| C Tools List | Static Analysis Tools for C Code list, with links to other lists. |
| Academic/Open Source Tools | |
| BLAST | BLAST is a software model checker for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses. Berkeley. |
| Buffer Overrun detectiON | Buffer overflow detection tool written as part of David Wagner's PhD dissertation, released in 2000 and no longer supported. |
| BOOP Toolkit | The BOOP Toolkit was implemented within the scope of the master's thesis of Georg Weißenbacher at the Institute for Software Technology at Graz University of Technology. It is based on the SLAM project of Microsoft Research. The BOOP Toolkit uses abstraction and refinement to determine the reachability of program points in a C program. |
| ComFoRT | The Component Formal Reasoning Technology (ComFoRT) is a reasoning framework for predicting whether a system will satisfy its safety, reliability, and security requirements. In ComFoRT, these requirements are encoded as behavioral assertions that are verified automatically. CMU/SEI. See also MAGIC. |
| CQual | Cqual is a type-based analysis tool that provides a lightweight, practical mechanism for specifying and checking properties of C programs. UMD. |
| Eau Claire | Security analysis tool by Brian Chess built on the Simplify theorem prover. |
| MAGIC | Modular Analysis of proGrams In C. CMU. See also COMFORT. |
| PMD | PMD Java source code checker with IDE plugins. |
| MOPS | MOdelchecking Programs for Security properties. Berkeley. |
| SPLINT | Secure Programming Lint from UVa. Extensive annotation capability. |
| Orion | An in-progress extension of Uno to C++ code. Not yet available. |
| UNO | Static global analysis tool from AT&T. Named for the three common vulnerabilities it searches for: unitialized variables, nil-pointer references, and out-of-bounds array accesses, but it can be extended to look for other vulnerabilities. See also Orion. |
| Commercial Tools | |
| Coverity Prevent | Commercial source code analysis tool. |
| ESC/Java | Extended Static Checker for Java (ESC/Java), developed at the Compaq Systems Research Center |
| Fortify | Commercial source code analysis tool with Eclipse IDE plugin. |
| MS PREfast/PREfix | Microsoft's proprietary static analysis tools with a focus on device drivers. They run lighter PREfast regularly; run slower interprocedural PREfix on full builds. |
| SLAM | Source code analysis project from Microsoft Research. No downloadable tools at current time. |
| Lexing Tools | |
| Flawfinder | Multi-language source analysis tool. |
| ITS4 | Free command-line static source code analysis tool from Cigital. |
| PScan | GPLed tool that scans code for format string vulnerabilities. |
| RATS | Rough Auditing Tool for Security, available freely from Secure Software. |