Practical Software Verification - Open Source Tools

Tags: #<Tag:0x00007f5334f3c6c0> #<Tag:0x00007f5334f3c580> #<Tag:0x00007f5334f3c418>


This is a data dump from the PSV wiki from #formal

The links and information are a couple of years old.

Program analysis

Link Description License
The LLVM compiler infrastructure The Low-Level Virtual Machine (LLVM) is a collection of libraries and tools that make it easy to build compilers, optimizers, Just-In-Time code generators, and many other compiler-related programs. LLVM uses a single, language-independent virtual instruction set both as an offline code representation (to communicate code between compiler phases and to run-time systems) and as the compiler internal representation (to analyze and transform programs). This persistent code representation allows a common set of sophisticated compiler techniques to be applied at compile-time, link-time, install-time, run-time, or "idle-time" (between program runs). University of Illinois/NCSA Open Source License
Valgrind Valgrind is an award-winning instrumentation framework for building dynamic analysis tools. There are Valgrind tools that can automatically detect many memory management and threading bugs, and profile your programs in detail. You can also use Valgrind to build new tools.

The Valgrind distribution currently includes six production-quality tools: a memory error detector, two thread error detectors, a cache and branch-prediction profiler, a call-graph generating cache profiler, and a heap profiler. It also includes one experimental tool, which detects out of bounds reads and writes of stack, global and heap arrays. It runs on the following platforms: X86/Linux, AMD64/Linux, PPC32/Linux, PPC64/Linux.

DynamoRio, Dynamic Instrumentation Tool Platform DynamoRIO is a runtime code manipulation system that supports code transformations on any part of a program, while it executes. DynamoRIO exports an interface for building dynamic tools for a wide variety of uses: program analysis and understanding, profiling, instrumentation, optimization, translation, etc. Unlike many dynamic tool systems, DynamoRIO is not limited to insertion of callouts/trampolines and allows arbitrary modifications to application instructions via a powerful IA-32/AMD64 instruction manipulation library. DynamoRIO provides efficient, transparent, and comprehensive manipulation of unmodified applications running on stock operating systems (Windows or Linux) and commodity IA-32 and AMD64 hardware. New BSD
The ERESI Reverse Engineering Software Interface The ERESI Reverse Engineering Software Interface is a multi-architecture binary analysis framework based on a common domain-specific language for reverse engineering. It provides extensive OS-wide support for program analysis, instrumentation, and debugging. ERESI mostly targets operating systems based on the Executable & Linking Format (ELF) such as Linux, *BSD, Solaris, HP-UX, IRIX and BeOS, on INTEL, SPARC, MIPS, ALPHA and ARM architectures. GPLv2
Boomerang The Boomerang reverse engineering framework is the first general native executable decompiler available to the public.The intent is to create a retargetable decompiler (i.e. one that can decompile different types of machine code files with modest effort, e.g. X86-windows, sparc-solaris, etc). It was also intended to be highly modular, so that different parts of the decompiler can be replaced with experimental modules. It was intended to eventually become interactive, a la IDA Pro, because some things (not just variable names and comments, though these are obviously very important) require expert intervention. Whether the interactivity belongs in the decompiler or in a separate tool remains unclear. Mixed? GPL+Others
Splint Splint is a tool for statically checking C programs for security vulnerabilities and coding mistakes. With minimal effort, Splint can be used as a better lint. If additional effort is invested adding annotations to programs, Splint can perform stronger checking than can be done by any standard lint. GPLv2
BOON BOON is a tool for automatically finding buffer overrun vulnerabilities in C source code. Buffer overruns are one of the most common types of security holes, and we hope that BOON will enable software developers and code auditors to improve the quality of security-critical programs. It is written in SML See project
Cqual Cqual is a type-based analysis tool that provides a lightweight, practical mechanism for specifying and checking properties of C programs. Cqual extends the type system of C with extra user-defined type qualifiers. The programmer adds type qualifier annotations to their program in a few key places, and Cqual performs qualifier inference to check whether the annotations are correct. The analysis results are presented with a user interface that lets the programmer browse the inferred qualifiers and their flow paths. GPL
Oink Oink is a collaboration of C++ static analysis tools. The C/C++ front-end for Oink is Elsa by Scott McPeak. Currently the main tool provided by Oink is CQual++, a polymorphic whole-program dataflow analysis for C++. CQual++ was inspired by Jeff Foster's Cqual tool and shares the backend solver with it. Modified MIT
Saturn The goal of the Saturn project is to statically and automatically verify properties of large (meaning multi-million line) software systems. The focus of much of our work is simultaneously achieving scalability, precision, and a straightforward way of expressing analyses that is easy to reason about; see the overview for more details. We plan to use these techniques to verify properties of a full operating system. BSD
CatchConv/SmartFuzz Automatic generation of test inputs to catch conversion errors between signed and unsigned integers. Valgrind plug-in that works with the STP decision procedure (downloaded separately). See for setup instructions. GPLv2
KLEE KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure. See this paper for more information. UIUC Open Source License
BAP BAP (Binary Analysis Platform) is the successor to the binary analysis techniques developed for Vine (the static analysis component of BitBlaze) as part of David Brumley's work on the BitBlaze project, which is headed up by Dawn Song. GPLv2
BitBlaze VINE VINE is BitBlaze's static analysis component that can translate x86 to VINE IL; to allow subsequent analysis and automation functions. While TEMU and Ruddler aren't released jet, the new options VINE allows are to translate the IL, generating control-flow graphs and specific data-flow analysis e. g.. GPLv2
ROSE ROSE is an open source compiler infrastructure to build source-to-source program transformation and analysis tools for large-scale Fortran 77/95/2003, C, C++, OpenMP, and UPC applications. The intended users of ROSE could be either experienced compiler researchers or library and tool developers who may have minimal compiler experience. ROSE is particularly well suited for building custom tools for static analysis, program optimization, arbitrary program transformation, domain-specific optimizations, complex loop optimizations, performance analysis, and cyber-security. BSD
Frama-C Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.

Frama-C gathers several static analysis techniques in a single collaborative framework. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer and dependency analysis.


Decision Procedures

Link Description License
STP: A Decision Procedure for Bitvectors and Arrays STP is a constraint solver (also referred to as a decision procedure or automated prover) aimed at solving constraints generated by program analysis tools, theorem provers, automated bug finders, intelligent fuzzers and model checkers. STP has been used in many research projects at Stanford, Berkeley, MIT, CMU and other universities. It is also being used at many companies such as NVIDIA, some startup companies, and by certain government agencies.

The input to STP are formulas over the theory of bit-vectors and arrays (This theory captures most expressions from languages like C/C++/Java and Verilog), and the output of STP is a single bit of information that indicates whether the formula is satisfiable or not. If the input is satisfiable, then it also generates a variable assignment to satisfy the input formula.

UCLID: A Verification Tool for Infinite-State Systems UCLID (pronounced "Euclid") is a tool for analyzing the correctness of models of hardware and software systems. UCLID can be used to model and verify infinite-state systems with variables of integer, Boolean, function, and array types. It can be used in to ways. 1) As a verifier, for term-level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based verification. 2) As a stand-alone decision procedure for the theories of uninterpreted functions and equality, integer linear arithmetic, and arrays. UCLID can also handle limited forms of quantification.

The applications of UCLID explored to-date include microprocessor design verification, analyzing software for security exploits, and verifying distributed algorithms.

Z3: SMT solver Z3 is a new high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. (This isn't open source but it's freely available and pretty useful) Microsoft Research License Agreement - Non-Commercial Use Only
MiniSat MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT MIT
Why Why is a software verification platform.

This platform contains several tools:

  • a general-purpose verification condition generator (VCG), Why, which is used as a back-end by other verification tools (see below) but which can also be used directly to verify programs (see for instance these examples) ;
  • a tool Krakatoa for the verification of Java programs;
  • a tool Caduceus for the verification of C programs; note that Caduceus is somewhat obsolete now and users should turn to Frama-C instead.
Hampi: A Solver For String Constraints Hampi is a solver for string constraints. Hampi is designed for constraints generated by program analysis tools, automated bug finders, intelligent fuzzers.

Hampi constraints express membership in regular languages and bounded context-free languages. Hampi constraints may contain context-free-language definitions, regular-language definitions and operations, and the membership predicate. Given a set of constraints, Hampi outputs a string that satisfies all the constraints, or reports that the constraints are unsatisfiable.


Model Checking

Link Description License
SPIN On the Fly, LTL Model Checking SPIN commerical license

Support tools

Link Description License
!exploitable Crash Analyzer !exploitable is a Windows debugging extension (Windbg) that provides automated crash analysis and security risk assessment. The tool first creates hashes to determine the uniqueness of a crash and then assigns an exploitability rating to the crash Microsoft Public License (MS-PL)
CrashWrangler Crash Analyzer CrashWrangler is an extension based on CrashReporter, that inspects application's state at the time of the crash and uses basic heuristics to try to determine exploitability. Apple Open Source License


Link Description License
The Bukowski Offensive Code Framework This project is intended to demonstrate that current popular approaches to software security (e.g. DAC, VMA randomization, anti-virus, NIDS, etc.) are not sufficient and that other approaches should be considered more seriously (e.g. MAC, design by contract, mutual authentication/authorization, etc.). The project applies formal methods to improving the quality of common offensive code techniques. Bukowski includes such technologies as metamorphism, polymorphism, proofs for lack of trusted path, etc. GPLv2