ksluckow / Awesome Symbolic Execution
Licence: cc0-1.0
A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
Stars: ✭ 634
Projects that are alternatives of or similar to Awesome Symbolic Execution
Crosshair
An analysis tool for Python that blurs the line between testing and type systems.
Stars: ✭ 586 (-7.57%)
Mutual labels: dynamic-analysis, symbolic-execution
Symbolic Execution
History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)
Stars: ✭ 395 (-37.7%)
Mutual labels: dynamic-analysis, symbolic-execution
Bap
Binary Analysis Platform
Stars: ✭ 1,385 (+118.45%)
Mutual labels: dynamic-analysis, symbolic-execution
smoosh
The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.
Stars: ✭ 86 (-86.44%)
Mutual labels: symbolic-execution
Compiler Rt
Project moved to: https://github.com/llvm/llvm-project
Stars: ✭ 272 (-57.1%)
Mutual labels: dynamic-analysis
malware-s2e
Code for my blog post on using S2E for malware analysis
Stars: ✭ 21 (-96.69%)
Mutual labels: symbolic-execution
Tigress protection
Playing with the Tigress binary protection. Break some of its protections and solve some of its challenges. Automatic deobfuscation using symbolic execution, taint analysis and LLVM.
Stars: ✭ 550 (-13.25%)
Mutual labels: symbolic-execution
Enlightn
Your performance & security consultant, an artisan command away.
Stars: ✭ 378 (-40.38%)
Mutual labels: dynamic-analysis
Cgpwn
A lightweight VM for hardware hacking, RE (fuzzing, symEx, exploiting etc) and wargaming tasks
Stars: ✭ 345 (-45.58%)
Mutual labels: symbolic-execution
Wasabi
A dynamic analysis framework for WebAssembly programs.
Stars: ✭ 279 (-55.99%)
Mutual labels: dynamic-analysis
Amoco
yet another tool for analysing binaries
Stars: ✭ 413 (-34.86%)
Mutual labels: symbolic-execution
Fromjs
See where each character on the screen came from in code.
Stars: ✭ 537 (-15.3%)
Mutual labels: dynamic-analysis
Dynamic Analysis
A curated list of dynamic analysis tools for all programming languages, binaries, and more.
Stars: ✭ 340 (-46.37%)
Mutual labels: dynamic-analysis
Stp
Simple Theorem Prover, an efficient SMT solver for bitvectors
Stars: ✭ 341 (-46.21%)
Mutual labels: symbolic-execution
Engine
Droidefense: Advance Android Malware Analysis Framework
Stars: ✭ 386 (-39.12%)
Mutual labels: dynamic-analysis
Habomalhunter
HaboMalHunter is a sub-project of Habo Malware Analysis System (https://habo.qq.com), which can be used for automated malware analysis and security assessment on the Linux system.
Stars: ✭ 627 (-1.1%)
Mutual labels: dynamic-analysis
Deepstate
A unit test-like interface for fuzzing and symbolic execution
Stars: ✭ 603 (-4.89%)
Mutual labels: symbolic-execution
Awesome Symbolic Execution 
A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
Table of Contents
Papers
- Symbolic Execution and Program Testing, James C. King.
- A system to generate test data and symbolically execute programs, L. A. Clarke.
- All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask), Edward J. Schwartz, Thanassis Avgerinos, David Brumley.
- A Survey of Symbolic Execution Techniques, Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Demetrescu, and Irene Finocchi.
Courses
- Symbolic Execution Lecture at Harvard.
- Symbolic Execution Lecture at Iowa State University.
- Symbolic Execution Lecture at University of Maryland.
Videos
- Symbolic Execution Lecture at MIT.
- Symbolic Execution Lecture (part of Software Security course on Coursera).
Tools
Java
- JPF-Symbc - Symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers, lazy initialization, etc.
- JDart - Dynamic symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers using JConstraints.
- CATG - Concolic execution tool that uses ASM for instrumentation. Uses CVC4.
- LimeTB - Concolic execution tool that uses Soot for instrumentation. Supports Yices and Boolector. Concolic execution can be distributed.
- Acteve - Concolic execution tool that uses Soot for instrumentation. Originally for Android analysis. Supports Z3.
- jCUTE - Concolic execution tool that uses Soot for instrumentation. Supports lp_solve.
- JFuzz - Concolic execution tool built on Java PathFinder.
- JBSE - Symbolic execution tool that uses a custom JVM. Supports CVC3, CVC4, Sicstus, and Z3.
- Key - Theorem Prover that uses specifications written in Java Modeling Language (JML).
LLVM
- KLEE - Symbolic execution engine built on LLVM.
- Cloud9 - Parallel symbolic execution engine built on KLEE.
- Kite - Based on KLEE and LLVM.
.NET
- PEX - Dynamic symbolic execution tool for .NET.
C
- CREST.
- Otter.
- CIVL - A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool.
JavaScript
Python
- PyExZ3 - Symbolic execution of Python functions. A rewrite of the NICE project's symbolic execution tool.
Ruby
- Rubyx - Symbolic execution tool for Ruby on Rails web apps.
Android
Binaries
- Mayhem.
- SAGE - Whitebox file fuzzing tool for X86 Windows applications.
- DART.
- BitBlaze.
- PathGrind - Path-based dynamic analysis for 32-bit programs.
- FuzzBALL - Symbolic execution tool built on the BitBlaze Vine component.
- S2E - Symbolic execution platform supporting x86, x86-64, or ARM software stacks.
- miasm - Reverse engineering framework. Includes symbolic execution.
- pysymemu - Supports x86/x64 binaries.
- BAP - Binary Analysis Platform provides a framework for writing program analysis tools.
- angr - Python framework for analyzing binaries. Includes a symbolic execution tool.
- Triton - Dynamic binary analysis platform that includes a dynamic symbolic execution tool.
- manticore - Symbolic execution tool for binaries (x86, x86_64 and ARMV7) and Ethereum smart contract bytecode.
Misc
- Symbooglix - Symbolic execution tool for Boogie programs.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].