Papers

From Practical Software Verification

Jump to: navigation, search

Add links to papers you have found useful or interesting here. Try to keep the subject area related to papers that are based on formal verification or to topics that might help in building a functional implementation. If you have time it would also be useful to fill out the template for the paper and provide as much information on as possible. That way we can hopefully minimise the amount of time people spend reading papers unrelated to what they are looking for. View the source of one of the existing articles and copy the template from there.

The table headings were picked fairly arbitrarily. If anyone can think of more informative headings then feel free to edit. The author heading is the primary paper author, I haven't bothered to include any others. List them on the paper description page if you want. The PoC field indicates whether a tool was created as part of the paper and the Released field indicates whether this tool was released publicly or not.

Contents

Fundamental theory and survey papers

Title Link New theory PoC Released Author Year
Formal verification at higher levels of abstraction [1] no no - Kroening D 2007
A Survey of Automated Techniques for Formal Software Verification [2] no no - D'Silva VJ 2008
Lecture notes on static analysis [3] no no - Schwartzbach M 2008
Loop summarization using abstract transformers [4] yes yes yes Kroening D 2008
A theory of type qualifiers (foundation for the Cqual and Cqual++ tools) [5] yes yes yes Foster J 1999
Static Analysis Tool Exposition 2008 [6] no no - NIST 2008

Formal Program Specification

Title Link New theory PoC Released Author Year
Z Notation (a formal specification language based on logic and ZF set theory) [7] [8] [9] yes yes yes ISO 2002
Guarded commands, non-determinacy and formal derivation of programs [10] yes no - Dijkstra 1975

Model Extraction and Checking; and Formal Program Specification

Title Link New theory PoC Released Author Year
Introduction to CMBC [11] yes yes yes Kroening D 2007
Integrated Static Analysis for Linux Device Driver Verification (CBMC extension, similar to SLAM) [12] no yes no Post H 2007
Counterexample-Guided Abstraction Refinement for Symbolic Model Checking [13] yes no no Clarke E 2003
Symbolic model checking using SAT procedures instead of BDDs [14] yes yes no Biere A 1999
Scalable and precise buffer overflow detection via Model Checking [15] no yes no Chaki S 2005
Automated formal verification and testing of C programs for embedded systems [16] yes yes no Kandl S 2007

Decision procedures

Title Link New theory PoC Released Author Year
A decision procedure for bit-vectors and arrays (STP) [17] yes yes yes Ganesh V 2007
Deciding bit-vector arithmetic with abstraction (UCLID) [18] yes yes yes Bryant R 2007
An extensible SAT solver (MiniSat) [19] yes yes yes Eén N 2003
Existential heap abstraction entailment is undecidable [20] yes yes yes Kuncak V 2003
Metamorphism, Formal Grammars and Undecidable Code Mutation [21] yes yes yes Filiol E 2007
Hampi: A Solver For String Constraints [22] yes yes yes Kiezun A 2009

Bug hunting

Title Link New theory PoC Released Author Year
KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs [23] no yes yes Dunbar D 2008
EXE: Automatically generating inputs of death [24] no yes no Cadar C 2006
DART: Directed automated random testing [25] yes yes no Godefroid P 2005
Automated whitebox fuzz testing [26] yes yes no Godefroid P 2008
IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution [27] yes yes no Zhiqiang L 2009
Improving Computer Security using Extended Static Checking [28] yes yes no Chess B 2002
A smart fuzzer for x86 executables [29] yes yes no Lanzi A 2007
Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions [30] yes yes no Engler D 2000
Catchconv: Symbolic execution and run-time type inference for integer conversion errors [31] yes yes yes Molnar D 2007
Loop-extended symbolic execution on binary programs [32] yes yes no Saxena P 2009
ARCHER: Using Symbolic, Path-sensitive Analysis to Detect Memory Access Errors [33] no yes no Xie Y 2003
Automated vulnerability auditing in machine code [34] no yes yes Durden T 2007
Grammar-Based Whitebox Fuzzing [35] yes yes no Godefroid P 2008
Finding User/Kernel Pointer Bugs With Type Inference (Cqual, static analysis) [36] no yes yes Johnson R 2004
Large-Scale Analysis of Format String Vulnerabilities in Debian Linux (Cqual++, static analysis) [37] yes yes yes Chen K 2007
Detecting Format String Vulnerabilities With Type Qualifiers [38] yes yes yes Shankar U 2001

Exploit Generation

Title Link New theory PoC Released Author Year
Automatic patch based exploit generation is possible: Techniques and implications [39] yes yes no Brumley D 2008
Automated exploit development: The future of exploitation is here [40] no yes no Medeiros J 2007
Automatic discovery of API level exploits [41] yes yes no Ganapathy V 2005
Convicting exploitable software vulnerabilities: An efficient input provenance based approach [42] yes yes no Zhiqiang L 2008
The Geometry of Innocent Flesh on the Bone: Return-into-libc without Function Calls (on the x86) [43] yes yes no Shacham H 2008
Automating Mimicry Attacks Using Static Binary Analysis [44] yes yes no Kruegel C 2005

Intermediate Representations and Binary Instrumentation Frameworks

Title Link New theory PoC Released Author Year
REIL: A platform-independent intermediate representation of disassembled code for static code analysis [45] no yes no Dullien T 2009
VinE, project documentation [46] no yes no Brumley D 2007
How the LLVM compiler infrastructure works (InformIT article) [47] no yes yes Chisnall D 2008
Pin: Building customized program analysis tools with dynamic instrumentation [48] yes yes yes Luk C 2005
Framework for Instruction-level Tracing and Analysis of Program Executions (Nirvana/iDNA) [49] yes yes no Bhansali S 2006
BAP: The Next-Generation Binary Analysis Platform [50] no yes yes Brumley D 2009

Dataflow analysis

Title Link New theory PoC Released Author Year
Dynamic Taint Analysis for Automatic Detection, Analysis, and Signature Generation of Exploits on Commodity Software [51] yes yes no Newsome J 2006
How to Shadow Every Byte of Memory Used by a Program [52] yes yes yes Nethercote N 2007
Generalizing Data Flow Information [53] no yes yes Skape 2007
Efficient fine-grained binary instrumentation with applications to taint-tracking [54] yes yes no Saxena P 2008
Parallelizing security checks on commodity hardware [55] no yes no Nightingale E 2008

Other program analysis

Title Link New theory PoC Released Author Year
Creating vulnerability signatures using weakest preconditions [56] yes yes no Brumley D 2007
Towards automatic generation of vulnerability based signatures [57] yes yes no Brumley D 2006
Vulnerability-Specific Execution Filtering for Exploit Prevention on Commodity Software [58] yes yes no Newsome J 2008
Replayer: Automatic protocol replay by binary analysis [59] no yes no Newsome J 2006
Shape Analysis for Composite Data Structures [60] yes yes no Josh Berdine 2007
Memalyze: Dynamic Analysis of Memory Access Behavior in Software [61] no yes yes Skape 2007
Program Analysis as Constraint Solving [62] yes yes no Gulwani S 2008
Digging for Data Structures [63] yes no no Cozzie A 2008

Other

Title Link New theory PoC Released Author Year
Static disassembly of obfuscated binaries [64] yes yes no Kruegel C 2004
Analysis-Resistant Malware [65] no yes yes Bethencourt J 2008
Retrieved from "http://www.unprotectedhex.com/psv/index.php/Papers"
Personal tools