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).
- Types #21
- Primitive Types #22
- Product Types #23
- Type Checking #24
- Enumeration and Sum Types #25
- Parametric Polymorphism #26
- Reference Types #27
- Container Types #28
- Subtyping #29
- Type Inference #32
- 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
- Adaptable Static Analysis of Executables for proving the Absence of Vulnerabilities - PhD thesis for Bogdan Mihaila, covers bindead, RREIL.
- 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
- Analyzing Memory Accesses in X86 Code - Value-Set Analysis
- Automated Whitebox Fuzz Testing - SAGE, concolic execution.
- CAB-Fuzz: Practical Concolic Testing Techniques for COTS Operating Systems
- Driller: Augmenting Fuzzing Through Selective Symbolic Execution - AFL + Concolic Execution.
- Enhancing Symbolic Execution with Veritesting - MAYHEM improved.
- Intermediate Representation Recovery from Low-Level Code - Strided Intervals.
- Mining Input Grammars from Dynamic Taints
- Precise Static Analysis of Untrusted Driver Binaries - Bounded Address Tracking
- Static Analysis of x86 Executables - Jakstab, Johnannes Kinder PhD Thesis.
- Unleashing MAYHEM on Binary Code - MAYHEM, hybrid concolic execution.
- What You See Is Not What You Execute
- 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 analysis
- amoco - bdcht is a wizard, probably.
- angr - The framework UCSB went to CGC with.
- 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.