CSE599L: On the Design and Implementation of Static Analysis Tools

Introduction, intro.ppt, intro.2.ppt
• http://en.wikipedia.org/wiki/Worse_is_Better
http://en.wikipedia.org/wiki/Robert_Tappan_Morris
Assignments
• read ASTREE and FindBugs papers for March 29;
• run FindBugs on a Java program of your choosing by April 5 and come ready to discuss your experience.

• lecture2.ppt
• ASTREE: A static analyzer for large safety-critical software
• FindBugs
  1. Evaluating and tuning a static analysis to find null pointer bugs
  2. Finding more null pointer bugs, but not too many
• ESPx/SAL: Modular checking for buffer overflows in the large
• Saturn: Scalable error detection using boolean satisfiability
• SLAM: Thorough static analysis of device drivers,
• Spec#: The Spec# programming system: an overview

• lecture3.ppt
• On characterization of safety and liveness properties in temporal logic
• Efficient monitoring of safety properties (skip section 4)

• lecture4.ppt
• We'll devote the first 15 minutes of class to discussing experience with FindBugs.
• Just read introduction of following paper A BDD-based model checker for recursive programs

• We'll go over the PDS reachability algorithm in lecture4.ppt again. Then we'll extend pLTL to talk about nested calls and returns.
• Encoding of flip and lock/unlock examples from lecture4.ppt  in bddbddb: lecture4_examples.zip
• Read the introduction of: A temporal logic of nested calls and returns

• lecture5.ppt
• Discuss how we want to go about evaluating software tools (list of questions): tool evaluation.ppt
• Read the paper: Effective typestate verification in the presence of aliasing

• lecture6.ppt
• A unified approach to global program optimization

• lecture7.ppt
• Precise interprocedural dataflow analysis via graph reachability

• lecture8.ppt
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

• lecture9.ppt
• Widening and narrowing (see above paper).
• Boolean and Cartesian abstraction for model checking C programs

• lecture10.ppt
• A new numerical abstract domain based on difference-bound matrices

• lecture11.ppt
• A framework for numeric analysis of array operations
• Combining abstract interpreters
• Counterexample driven refinement for abstract interpretation

• lecture12.ppt
• Undecidability of static analysis [ed. note: of may/must aliasing in particular]
• Pointer-induced aliasing: a problem taxonomy
• Interprocedural may-alias analysis for pointers: beyond k-limiting
• Deciding assertions in programs with references

Eight papers, summarized in one lecture (you don't need to read them all!):

• lecture13.ppt
• 2000: Unification-based pointer analysis with directional assignments
• 2001: Ultra-fast aliasing analysis using CLA: a million lines of C code in a second
• 2002: Parameterized object sensitivity for points-to and side-effect analyses for Java
• 2003: Points-to analysis using BDDs
• 2004: Efficient field-sensitive pointer analysis for C
• 2005: Improving software security with a C pointer analysis
• 2005: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams
• 2006: Refinement-based context-sensitive points-to analysis for Java

• lecture14.ppt
• An interpretation oriented theorem prover over integers
• An axiomatic basis for computer programming
• Symbolic execution and program testing

• lecture15.ppt
• Proof-carrying code
• Weakest-precondition of unstructured programs

• lecture16.ppt
• SAT solving: a mini course
• Chaff: engineering an efficient SAT solver

• lecture17.ppt
• Slides for FMCAD 2006 tutorial on SMT solver

• Static Driver Verifier (SDV)
• Saturn

• Cqual
• Spec#

• Combining under- and over-approximation
• Automated abstraction refinement
• Shape analysis
• Specification inference
• Combining abstract interpretation and theorem proving

Tools/Infrastructure We Will be Evaluating (not necessarily in order)

• Tools:
  • FindBugs: defect detection for Java
  • Windows Vista SDK: PREfast/SAL buffer overflow detection for C/C++
  • FxCop: defect detection for .NET assemblies
  • Spec#: verification for C# using specifications, verification conditions and automated theorem proving
  • CBMC, Saturn: using SAT solvers for defection detection for C
  • BLAST: automated abstraction refinement for C
  • CQual/Oink: type qualifiers for C/C++ polymorphic qualifier dataflow analysis
• Infrastructure:
  • Apron: numerical abstract domain library
  • bddbddb: BDD-based implementation of Datalog
  • BANSHEE: constraint-based analysis engine
  • CIL: infrastructure for C program analysis and transformation
  • Phoenix: Microsoft software optimization and analysis framework

Possible Project Ideas:

Create a Temporal Safety Checker for C

1. Translate pLTL into a SPIN "never" claim (a safety automata) that Moped can read
2. Translate CIL CFG into Moped format or into bddbddb
3. Extra credit: add Caret matching of call/returns.

Create User Documentation and Tutorial for bddbddb