MiasmReverse engineering framework in Python
IdangrUse angr in the IDA Pro debugger generating a state from the current debug session
SymbioticSymbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
SymgdbSymGDB - symbolic execution plugin for gdb
Alive2Automatic verification of LLVM optimizations
ExropAutomatic ROPChain Generation
KleeflSeeding fuzzers with symbolic execution
SysSys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code
TritonTriton is a Dynamic Binary Analysis (DBA) framework. It provides internal components like a Dynamic Symbolic Execution (DSE) engine, a dynamic taint engine, AST representations of the x86, x86-64, ARM32 and AArch64 Instructions Set Architecture (ISA), SMT simplification passes, an SMT solver interface and, the last but not least, Python bindings.
KleeKLEE Symbolic Execution Engine
BapBinary Analysis Platform
PakalaOffensive vulnerability scanner for ethereum, and symbolic execution tool for the Ethereum Virtual Machine
ExposeA Dynamic Symbolic Execution (DSE) engine for JavaScript. ExpoSE is highly scalable, compatible with recent JavaScript standards, and supports symbolic modelling of strings and regular expressions.
EthenoSimplify Ethereum security analysis and testing
PonceIDA 2016 plugin contest winner! Symbolic Execution just one-click away!
ApisanAPISan: Sanitizing API Usages through Semantic Cross-Checking
MedusaAn open source interactive disassembler
Wasabi AegYet another implementation of AEG (Automated Exploit Generation) using symbolic execution engine Triton.
AngoraAngora is a mutation-based fuzzer. The main goal of Angora is to increase branch coverage by solving path constraints without symbolic execution.
Awesome Symbolic ExecutionA curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
DeepstateA unit test-like interface for fuzzing and symbolic execution
CrosshairAn analysis tool for Python that blurs the line between testing and type systems.
Tigress protectionPlaying 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.
Amocoyet another tool for analysing binaries
Symbolic ExecutionHistory of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)
CgpwnA lightweight VM for hardware hacking, RE (fuzzing, symEx, exploiting etc) and wargaming tasks
StpSimple Theorem Prover, an efficient SMT solver for bitvectors
MythrilSecurity analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains.
G2No description or website provided.
smooshThe Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.
malware-s2eCode for my blog post on using S2E for malware analysis
crusherNo description or website provided.
kleespectreKLEESpectre is a symbolic execution engine with speculation semantic and cache modelling
RelBinsec/Rel is an extension of Binsec that implements relational symbolic execution for constant-time verification and secret-erasure at binary-level.
KirenenkoSuper Fast Concolic Execution Engine based on Source Code Taint Tracing
SixtyPicalA 6502-oriented low-level programming language supporting advanced static analysis
TRACERTRACER Symbolic Execution Tool
seninjasymbolic execution plugin for binary ninja
surveyorA symbolic debugger for C/C++ (via LLVM), machine code, and JVM programs
CFI-LBAdaptive Callsite-sensitive Control Flow Integrity - EuroS&P'19
vigorMain repository of the Vigor NF verification project.
CRAXCRAX: software CRash analysis for Automatic eXploit generation
saiStaged Abstract Interpreters
steviaA simple (unfinished) SMT solver for QF_ABV.
angr-antievasionFinal project for the M.Sc. in Engineering in Computer Science at Università degli Studi di Roma "La Sapienza" (A.Y. 2016/2017).
UTBotCppTool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage