Goethe University Frankfurt Videos
This is an excellent series of videos, about 10 minutes each, which walk through the basics of program analysis. These videos are approachable, break down concepts easily with visual examples, and are in American (or English for you Brits).
- Program Analysis Overview #47
- Type and Effect Systems #48
- Dataflow Analysis #49
- Basic Intermediate Systems #50
- Foundations of Dataflow Analysis #51
- Computation #52
- Subtyping #53
- Precision of Data Flow Analysis #54
- Distributive Framework for Data Flow Analysis #55
- Qualities of Static Program Analysis #56
- Call Graphs #57
- Interprocedural Data Flow Analysis #58
- Procedure Summaries in Data Flow Analysis #59
- Program Analysis and the Heap #60
- Introduction to Points to Analysis #61
- Steensgaard’s Points to Analysis #62
- Andersen’s Points to Analysis #63
- Abstract Interpretation: Introduction #64
- Array-Out-Of-Bounds Checking #65
- Galois Connections #66
- A Catalogue of Galois Connections #67
- Refactoring #68
- Static Bug Checking #69
- Dynamic Program Analysis #70
Papers related to constraint-solving over binaries
- Adaptable Static Analysis of Executables for proving the Absence of Vulnerabilities - PhD thesis for bindead, RREIL. Great overview of several static analyses.
- All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but might have been afraid to ask)
- A Survey of Symbolic Execution Techniques
- Automated Whitebox Fuzz Testing - The paper that introduced SAGE.
- CAB-Fuzz: Practical Concolic Testing Techniques for COTS Operating Systems - On the reading list
- Driller: Augmenting Fuzzing Through Selective Symbolic Execution - AFL + Concolic Execution.
- Enhancing Symbolic Execution with Veritesting - MAYHEM improved.
- Mining Input Grammars from Dynamic Taints
- Precise static analysis of untrusted driver binaries - Bounded Address Tracking.
- Unleashing MAYHEM on Binary Code - ForAllSecure’s Symbolic Execution engine.
- Generic Windows Shellcoding
- Sysenter Based System Call Mechanism in Linux 2.6 - How Linux really does system calls.
- About ELF Auxiliary Vectors
Frameworks for binary constraint solving
- amoco - bdcht is a wizard, probably.
- angr - The framework UCSB went to CGC with.
- BAP - Ocaml…
- Triton - Jonathan Salwan’s Dynamic Symbolic Execution engine and framework.
Libraries for binary constraint solving
- llvm2smt - Experimental translation of llvm to smt.
- openreil - REIL lifter for x86 that seems to #justwork.
- remill - ToB’s latest framework to lift binary code to LLVM IR. Moving towards support of multiple architectures.
Non-binary program analysis frameworks
- pyt - Program analysis framework for python applications. Appears focused on taint analysis for web frameworks.
The standard toolkit
Interesting projects to bookmark
- firmadyne - Emulate embedded linux firmware.
- peda - Python Exploit Development Assistance for GDB.
- pycparser - C99 Parser in Python.
- snowman - Decompiler framewowrk.
- villoc - Heap visualization tool.
- voltron - Debugger UI.
- x64bdg - Windows debugger.
- xed - Intel’s x86 disassembler. ToB’s latest stuff is moving towards xed, as is binary.ninja.
- Vector35/community-plugins - Vector35’s official list of community plugins for Binary Ninja.
- hopper-plugins - Additional architectures/loaders for Hopper.