General
Symbolic Execution
Lectures & Courses
- Foundations of Programming Languages
- Static Program Analysis
- 25 Years of Program Analysis
- Software Analysis and Testing - Mayur Naik
- Program Analysis and Reliability - Nick Sumner, CMPT 886, Spring 2015, SFU
- Program analysis for reverse engineers: from T to ⊥
- CS 252r: Advanced Topics in Programming Languages
- A Gentle Introduction to Program Analysis
Software
- SPARTA: a library that provides the basic blocks for building high-performance static code analyzers based on Abstract Interpretation
- Bill Torpey - static analysis posts
LLVM
- awesome-llvm: A curated list of awesome LLVM related docs, tools, and other resources
- LLVM Weekly - http://llvmweekly.org/
- https://eli.thegreenplace.net/tag/llvm-clang
- Building a Checker in 24 hours
- Code transformation and analysis using Clang and LLVM
- Compiler-assisted Performance Analysis
- Dg: LLVM Static Slicer
- FPSCEV: Floating-Point Scalar Evolution in LLVM
- LLVM Dataflow Info Printer Pass
- https://github.com/regehr/llvm-dataflow-info
- Tell us what some of LLVM's dataflow analyses think about the code being compiled.
- Testing Dataflow Analyses for Precision and Soundness
- Testing Static Analyses for Precision and Soundness
- LLVM Debugging Tips and Tricks
- Phasar - A LLVM-based static code analysis framework
- SVF: Interprocedural Static Value-Flow Analysis in LLVM
LLVM - Symbolic Execution
- haybale: Symbolic execution of LLVM IR with an engine written in Rust
- KLEE Symbolic Virtual Machine
LLVM - Verification
- LLBMC: The Low-Level Bounded Model Checker
- llrêve: Automatic regression verification for LLVM programs
- SAW: Software Analysis Workbench
- SeaHorn Verification Framework: A fully automated analysis framework for LLVM-based languages
- SMACK Software Verifier and Verification Toolchain
Clang
- clang-tutor: A collection of Clang plugins - learn the API through examples
- My First Clang Warning
Clang Static Analyzer
- Developing the Clang Static Analyzer
- Faster, Stronger C++ Analysis with the Clang Static Analyzer
Introduction
- Building Program Reasoning Tools using LLVM and Z3
- Getting Started With LLVM: Basics
- How to Contribute to LLVM
- Introduction to LLVM
- Intrinsics, Metadata, and Attributes: The story continues!
- LLVM IR Tutorial - Phis, GEPs and other things, oh my!
- LLVM Seminar - Northeastern+MIT
- Security Research and Development with LLVM - Andrew Reiter
- clang-llvm-tutorial
- Custom Alias Analysis in LLVM
- Introduction to LLVM: Building simple program analysis tools and instrumentation
- LLVMPlayground: Small sample programs that use LLVM and Clang APIs.
- Mapping High Level Constructs to LLVM IR
- Nick Sumner's Examples
- slides: https://www.cs.sfu.ca/~wsumner/teaching/886/llvm.pdf
- llvm-demo: A simple example of how LLVM can be used to gather static or dynamic facts about a program.
- callgraph-profiler-template: A template for an introductory project on dynamic analysis using LLVM
- clang-plugins-demo: A simple example of defining custom plugins for Clang and the Clang Static Analyzer
- llvm-dataflow-analysis: (very simple) static intraprocedural dataflow analyses
- overflower-template: Template for a project to teach basic static dataflow analysis using LLVM
- path-profiler-template: A template for a path profiling project using LLVM
- Quarkslab blog
- Writing a basic clang static analysis check
Instrumentation
- Creating an LLVM Sanitizer from Hopes and Dreams
- Instrew: Leveraging LLVM for High Performance Dynamic Binary Instrumentation
- Loom: LLVM instrumentation library
- PolyTracker: An LLVM-based instrumentation tool for universal taint analysis.
- QBDI (QuarkslaB Dynamic binary Instrumentation): A Dynamic Binary Instrumentation framework based on LLVM
- sbt-instrumentation: Configurable instrumentation of LLVM bitcode
Lifting
Lifting: Disassembly, Decompilation, Recompilation, Reverse Engineering
- ANVILL Decompiler Toolchain
- decomp: Compositional Decompilation using LLVM IR
- llvm-mctoll
- McSema: Framework for lifting x86, amd64, and aarch64 program binaries to LLVM bitcode
- Rellic: produces goto-free C output from LLVM bitcode
- Rellume — Lifts x86-64 to LLVM IR
- https://github.com/aengelke/rellume
- Rellume is a lifter for x86-64 machine code to LLVM IR with focus on the performance of the lifted code. The generated LLVM IR can be compiled and executed again, for example using LLVM's JIT compiler, ideally having the same (or even better) performance as the original code.
- Remill: Library for lifting of x86, amd64, and aarch64 machine code to LLVM bitcode
- RetDec: a retargetable machine-code decompiler based on LLVM
- revng: a static binary translator
- revng is a static binary translator. Given a input ELF binary for one of the supported architectures (currently MIPS, ARM and x86-64) it will analyze it and emit an equivalent LLVM IR. To do so, revng employs the QEMU intermediate representation (a series of TCG instructions) and then translates them to LLVM IR.
- https://rev.ng/
- https://github.com/revng/revng
Passes
- Building, Testing and Debugging a Simple out-of-tree LLVM Pass
- llvm-pass-tutorial: A step-by-step tutorial for building an LLVM sample pass
- llvm-tutor: Basic LLVM passes for learning the API
Legacy Pass Manager
- 2007 LLVM Developer's Meeting
New Pass Manager
- New PM: taming a custom pipeline of Falcon JIT
- The LLVM Pass Manager, Part 2
- Passes in LLVM, Part 1
- Writing LLVM Pass in 2018
Readings
- A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World
- Communications of the ACM, Vol. 53 No. 2, 2010
- Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, Dawson Engler
- https://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext
- Analysing the Program Analyser
- Continuous Reasoning: Scaling the Impact of Formal Methods
- From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis
- How to Prevent the next Heartbleed
- Lessons from Building Static Analysis Tools at Google (2018)
- Pointer analysis: haven't we solved this problem yet?
- Righting Software
- Source Code Analysis: A Road Map
- Static versus dynamic analysis---an illusory distinction?
Tags:
reading
language
tool
Last modified 07 October 2024