Topic: "symbolic-execution"
ConsenSysDiligence/mythril
Mythril is a symbolic-execution-based securty analysis tool for EVM bytecode. It detects security vulnerabilities in smart contracts built for Ethereum and other EVM-compatible blockchains.
Language: Python - Size: 47.4 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 4,039 - Forks: 773

trailofbits/manticore
Symbolic execution tool
Language: Python - Size: 43.5 MB - Last synced at: 22 days ago - Pushed at: over 1 year ago - Stars: 3,760 - Forks: 479

JonathanSalwan/Triton
Triton is a dynamic binary analysis library. Build your own program analysis tools, automate your reverse engineering, perform software verification or just emulate code.
Language: C++ - Size: 57.1 MB - Last synced at: 23 days ago - Pushed at: about 1 month ago - Stars: 3,729 - Forks: 550

cea-sec/miasm
Reverse engineering framework in Python
Language: Python - Size: 16.5 MB - Last synced at: 23 days ago - Pushed at: 5 months ago - Stars: 3,666 - Forks: 479

klee/klee
KLEE Symbolic Execution Engine
Language: C++ - Size: 8.99 MB - Last synced at: 22 days ago - Pushed at: about 1 month ago - Stars: 2,761 - Forks: 691

BinaryAnalysisPlatform/bap
Binary Analysis Platform
Language: OCaml - Size: 8.21 MB - Last synced at: 22 days ago - Pushed at: about 1 month ago - Stars: 2,136 - Forks: 277

illera88/Ponce
IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
Language: C++ - Size: 332 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 1,546 - Forks: 78

ksluckow/awesome-symbolic-execution
A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
Size: 49.8 KB - Last synced at: 20 days ago - Pushed at: 8 months ago - Stars: 1,396 - Forks: 141

JonathanSalwan/VMProtect-devirtualization
Playing with the VMProtect software protection. Automatic deobfuscation of pure functions using symbolic execution and LLVM.
Language: Roff - Size: 28.1 MB - Last synced at: 19 days ago - Pushed at: about 3 years ago - Stars: 1,252 - Forks: 195

pschanely/CrossHair
An analysis tool for Python that blurs the line between testing and type systems.
Language: Python - Size: 4.96 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 1,162 - Forks: 61

wisk/medusa
An open source interactive disassembler
Language: C++ - Size: 15.9 MB - Last synced at: 11 months ago - Pushed at: over 5 years ago - Stars: 1,039 - Forks: 92

AngoraFuzzer/Angora
Angora is a mutation-based fuzzer. The main goal of Angora is to increase branch coverage by solving path constraints without symbolic execution.
Language: C++ - Size: 13 MB - Last synced at: 2 months ago - Pushed at: almost 3 years ago - Stars: 941 - Forks: 170

AliveToolkit/alive2
Automatic verification of LLVM optimizations
Language: C++ - Size: 6.32 MB - Last synced at: 21 days ago - Pushed at: 28 days ago - Stars: 905 - Forks: 116

trailofbits/deepstate
A unit test-like interface for fuzzing and symbolic execution
Language: Python - Size: 1.44 MB - Last synced at: 21 days ago - Pushed at: 5 months ago - Stars: 831 - Forks: 97

JonathanSalwan/Tigress_protection
Playing with the Tigress software protection. Break some of its protections and solve their reverse engineering challenges. Automatic deobfuscation using symbolic execution, taint analysis and LLVM.
Language: LLVM - Size: 13.1 MB - Last synced at: 19 days ago - Pushed at: over 1 year ago - Stars: 831 - Forks: 145

huchenxucs/ChatDB
The official repository of "ChatDB: Augmenting LLMs with Databases as Their Symbolic Memory".
Language: Python - Size: 369 KB - Last synced at: about 1 month ago - Pushed at: almost 2 years ago - Stars: 576 - Forks: 52

Nalen98/AngryGhidra
Use angr in Ghidra
Language: Java - Size: 25.2 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 536 - Forks: 47

stp/stp
Simple Theorem Prover, an efficient SMT solver for bitvectors
Language: C++ - Size: 33.1 MB - Last synced at: 7 months ago - Pushed at: 9 months ago - Stars: 525 - Forks: 130

enzet/symbolic-execution
History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)
Language: Kotlin - Size: 14.9 MB - Last synced at: 17 days ago - Pushed at: 10 months ago - Stars: 493 - Forks: 56

bdcht/amoco
yet another tool for analysing binaries
Language: Python - Size: 3.18 MB - Last synced at: 20 days ago - Pushed at: 4 months ago - Stars: 483 - Forks: 64

mazeppa-dev/mazeppa
A modern supercompiler for call-by-value functional languages
Language: OCaml - Size: 664 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 407 - Forks: 9

0xM3R/cgPwn
A lightweight VM for hardware hacking, RE (fuzzing, symEx, exploiting etc) and wargaming tasks
Language: Shell - Size: 10.7 KB - Last synced at: 23 days ago - Pushed at: almost 6 years ago - Stars: 357 - Forks: 59

palkeo/pakala
Offensive vulnerability scanner for ethereum, and symbolic execution tool for the Ethereum Virtual Machine
Language: Python - Size: 204 KB - Last synced at: 21 days ago - Pushed at: about 3 years ago - Stars: 343 - Forks: 29

crytic/etheno 📦
Simplify Ethereum security analysis and testing
Language: Python - Size: 738 KB - Last synced at: 27 days ago - Pushed at: 4 months ago - Stars: 340 - Forks: 33

borzacchiello/seninja
symbolic execution plugin for binary ninja
Language: Python - Size: 2.34 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 320 - Forks: 24

staticafi/symbiotic
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
Language: Python - Size: 2.13 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 320 - Forks: 57

cleanunicorn/karl
Monitor smart contracts deployed on blockchain and test against vulnerabilities with Mythril. It was presented at DEFCON 2019.
Language: Python - Size: 4.3 MB - Last synced at: 19 days ago - Pushed at: 20 days ago - Stars: 318 - Forks: 78

ergrelet/themida-unmutate
Static deobfuscator for Themida, WinLicense and Code Virtualizer 3.x's mutation-based obfuscation.
Language: Python - Size: 1.1 MB - Last synced at: 18 days ago - Pushed at: 11 months ago - Stars: 281 - Forks: 25

d4em0n/exrop 📦
Automatic ROPChain Generation
Language: Python - Size: 1.39 MB - Last synced at: 7 months ago - Pushed at: over 5 years ago - Stars: 280 - Forks: 23

andreafioraldi/IDAngr
Use angr in the IDA Pro debugger generating a state from the current debug session
Language: Python - Size: 30.1 MB - Last synced at: about 1 month ago - Pushed at: almost 5 years ago - Stars: 277 - Forks: 31

FuzzingLabs/thoth
Cairo/Starknet security toolkit (bytecode analyzer, disassembler, decompiler, symbolic execution, SBMC)
Language: Python - Size: 5.63 MB - Last synced at: about 2 months ago - Pushed at: 5 months ago - Stars: 254 - Forks: 23

PLSysSec/sys
Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code
Language: LLVM - Size: 4.55 MB - Last synced at: 2 months ago - Pushed at: about 3 years ago - Stars: 227 - Forks: 41

OCamlPro/owi
Symbolic execution for Wasm, C, C++, Rust and Zig
Language: OCaml - Size: 19 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 222 - Forks: 31

SQLab/symgdb
SymGDB - symbolic execution plugin for gdb
Language: Python - Size: 1.79 MB - Last synced at: 11 months ago - Pushed at: about 7 years ago - Stars: 213 - Forks: 26

ExpoSEJS/ExpoSE
A 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.
Language: JavaScript - Size: 12.1 MB - Last synced at: 30 days ago - Pushed at: 5 months ago - Stars: 202 - Forks: 40

julieeen/kleefl
Seeding fuzzers with symbolic execution
Language: Python - Size: 1.93 MB - Last synced at: about 1 year ago - Pushed at: over 7 years ago - Stars: 197 - Forks: 25

GaloisInc/MATE
MATE is a suite of tools for interactive program analysis with a focus on hunting for bugs in C and C++ code using Code Property Graphs.
Language: Python - Size: 117 MB - Last synced at: 2 days ago - Pushed at: over 2 years ago - Stars: 193 - Forks: 12

quarkslab/pastis
PASTIS: Collaborative Fuzzing Framework
Language: Python - Size: 63.4 MB - Last synced at: 2 days ago - Pushed at: about 1 month ago - Stars: 164 - Forks: 10

yuawn/Fuzzing
Fuzzing tutorial with easy-to-learn labs 🚀
Language: C++ - Size: 78.1 KB - Last synced at: about 18 hours ago - Pushed at: almost 3 years ago - Stars: 161 - Forks: 18

UnitTestBot/UTBotCpp
Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage
Language: C++ - Size: 22 MB - Last synced at: 6 months ago - Pushed at: 8 months ago - Stars: 159 - Forks: 27

HarvardPL/formulog
Datalog with support for SMT queries and first-order functional programming
Language: Java - Size: 2.94 MB - Last synced at: 20 days ago - Pushed at: 8 months ago - Stars: 157 - Forks: 10

eth-sri/ilf
AI based fuzzer based on imitation learning
Language: Python - Size: 4.73 MB - Last synced at: about 1 year ago - Pushed at: almost 2 years ago - Stars: 144 - Forks: 32

ispras/oss-sydr-fuzz
OSS-Sydr-Fuzz - OSS-Fuzz fork for hybrid fuzzing (fuzzer+DSE) open source software.
Language: C - Size: 12 MB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 138 - Forks: 33

UnitTestBot/UTBotJava
Automated unit test generation and precise code analysis for Java
Language: Kotlin - Size: 204 MB - Last synced at: 2 days ago - Pushed at: about 1 year ago - Stars: 138 - Forks: 46

ercoppa/symbolic-execution-tutorial
Tutorial on Symbolic Execution. Hands-on session is based on the angr framework.
Language: Python - Size: 2.92 MB - Last synced at: about 12 hours ago - Pushed at: about 4 years ago - Stars: 132 - Forks: 18

Generative-Program-Analysis/GenSym
A high-performance, parallel, compilation-based symbolic execution engine
Language: Java - Size: 21.4 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 130 - Forks: 5

season-lab/fuzzolic
fuzzing + concolic = fuzzolic :)
Language: C - Size: 23.6 MB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 121 - Forks: 7

mgree/smoosh
The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.
Language: OCaml - Size: 3.66 MB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 118 - Forks: 5

csvl/SEMA
SEMA is based on angr, a symbolic execution engine used to extract API calls. Especially, we extend ANGR with strategies to create representative signatures based on System Call Dependency graph (SCDG). Those SCDGs can be exploited in machine learning modules to do classification/detection.
Language: Python - Size: 1.42 GB - Last synced at: 2 days ago - Pushed at: 3 months ago - Stars: 115 - Forks: 23

GaloisInc/grease
CLI tool and Ghidra plug-in for analyzing binaries using under-constrained symbolic execution
Language: Haskell - Size: 1.45 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 111 - Forks: 7

viperproject/silicon
Symbolic-execution-based verifier for the Viper intermediate verification language.
Language: Scala - Size: 39.3 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 105 - Forks: 37

ucsb-seclab/greed
A symbolic execution engine for EVM smart contract binaries.
Language: Python - Size: 10.1 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 104 - Forks: 16

SQLab/CRAXplusplus
The exploit generator CRAX++ is CRAX with a plugin system, s2e 2.0 upgrade, dynamic ROP, code selection, and I/O states (HITCON 2022)
Language: C++ - Size: 4.18 MB - Last synced at: 1 day ago - Pushed at: over 2 years ago - Stars: 102 - Forks: 15

ChengyuSong/Kirenenko Fork of AngoraFuzzer/Angora 📦
Super Fast Concolic Execution Engine based on Source Code Taint Tracing
Language: C++ - Size: 19.6 MB - Last synced at: about 1 year ago - Pushed at: almost 3 years ago - Stars: 98 - Forks: 10

crytic/optik
Optik is a set of symbolic execution tools that assist smart-contract fuzzers
Language: Python - Size: 594 KB - Last synced at: about 1 month ago - Pushed at: 9 months ago - Stars: 94 - Forks: 12

tum-i4/obfuscation-benchmarks
A set of programs used for benchmarking the strength of obfuscation
Language: C - Size: 46.5 MB - Last synced at: about 1 year ago - Pushed at: over 7 years ago - Stars: 81 - Forks: 20

SoftSec-KAIST/MeanDiff
Testing Intermediate Representations for Binary Analysis (ASE '17)
Language: F# - Size: 369 KB - Last synced at: about 20 hours ago - Pushed at: over 6 years ago - Stars: 80 - Forks: 11

JonathanSalwan/ttexplore
TTexplore is a library that performs path exploration on binary code using symbolic execution
Language: C++ - Size: 552 KB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 76 - Forks: 7

borzacchiello/naaz
Symbolic Execution Engine based on Ghidra's PCode
Language: C++ - Size: 291 KB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 75 - Forks: 4

purseclab/DnD
A decompiler to automatically reverse-engineer the DNN semantics from its compiled binary using program analysis
Language: Python - Size: 3.87 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 73 - Forks: 10

WilfredTA/symbolic-stack-machines
Library for building symbolically executable stack-based virtual machines
Language: Rust - Size: 125 KB - Last synced at: over 2 years ago - Pushed at: over 2 years ago - Stars: 68 - Forks: 8

SVF-tools/Software-Security-Analysis
Static Analysis Course
Language: C++ - Size: 73.6 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 67 - Forks: 25

feliam/klee-taint Fork of klee/klee
KLEE-TAINT - Klee with taint analysis support
Language: C++ - Size: 4.59 MB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 67 - Forks: 13

lsrcz/grisette
A monadic library for symbolic evaluation
Language: Haskell - Size: 34.9 MB - Last synced at: 9 days ago - Pushed at: 22 days ago - Stars: 66 - Forks: 3

sjmikler/pytorch-symbolic
Symbolic API for model creation in PyTorch.
Language: Jupyter Notebook - Size: 5.39 MB - Last synced at: 17 days ago - Pushed at: 3 months ago - Stars: 66 - Forks: 3

Kraks/sai
Staged Abstract Interpreters
Language: Scala - Size: 18.1 MB - Last synced at: 4 days ago - Pushed at: about 2 years ago - Stars: 66 - Forks: 8

Symbolica/Symbolica
Symbolica's open-source symbolic execution engine.
Language: C# - Size: 1.79 MB - Last synced at: 8 days ago - Pushed at: 9 months ago - Stars: 65 - Forks: 6

sdasgup3/binary-decompilation
Extracting high level semantic information from binary code
Language: Assembly - Size: 244 MB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 65 - Forks: 8

jordan9001/dobby2
Build your emulation environment as needed
Language: Python - Size: 495 KB - Last synced at: 7 months ago - Pushed at: about 4 years ago - Stars: 64 - Forks: 10

sslab-gatech/apisan
APISan: Sanitizing API Usages through Semantic Cross-Checking
Language: C++ - Size: 34 MB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 63 - Forks: 27

p4pktgen/p4pktgen
Automatic test case generator for P4 programs
Language: Python - Size: 11.9 MB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 58 - Forks: 15

SVL-PSU/crete-dev
CRETE under development
Language: C - Size: 227 MB - Last synced at: almost 2 years ago - Pushed at: almost 5 years ago - Stars: 56 - Forks: 15

redtrama/awesome-halmos
List of Halmos resources.
Size: 27.3 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 53 - Forks: 7

JonathanSalwan/X-Tunnel-Opaque-Predicates
IDA+Triton plugin in order to extract opaque predicates using a Forward-Bounded DSE. Example with X-Tunnel.
Language: Python - Size: 83 KB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 52 - Forks: 16

tweag/pirouette 📦
Language-generic workbench for building static analysis
Language: Haskell - Size: 1.54 MB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 47 - Forks: 2

VSharp-team/VSharp
Symbolic execution engine for .NET Core
Language: C++ - Size: 54.6 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 46 - Forks: 29

SQLab/CRAX Fork of S2E/s2e-old
CRAX: software CRash analysis for Automatic eXploit generation
Language: C - Size: 53.1 MB - Last synced at: about 1 year ago - Pushed at: almost 10 years ago - Stars: 46 - Forks: 12

vigor-nf/vigor
Main repository of the Vigor NF verification project.
Language: C - Size: 9.54 MB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 45 - Forks: 13

PKU-ASAL/SeeWasm
A native symbolic execution engine for WebAssembly
Language: Python - Size: 15.1 MB - Last synced at: about 2 months ago - Pushed at: 11 months ago - Stars: 43 - Forks: 3

dynaroars/dig
DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.
Language: Python - Size: 80.8 MB - Last synced at: 20 days ago - Pushed at: 20 days ago - Stars: 41 - Forks: 6

formalsec/smtml
An SMT solver frontend for OCaml
Language: OCaml - Size: 2.75 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 39 - Forks: 11

ispras/crusher
Language: Python - Size: 32 MB - Last synced at: 8 days ago - Pushed at: 29 days ago - Stars: 39 - Forks: 16

SoftwareSecurityLab/UbSym
A Unit-Based Symbolic Execution Method for Detecting Memory Corruption Vulnerabilities in Executable Codes
Language: C - Size: 3.47 MB - Last synced at: almost 2 years ago - Pushed at: about 2 years ago - Stars: 37 - Forks: 8

BillHallahan/G2
Language: Haskell - Size: 60.2 MB - Last synced at: about 6 hours ago - Pushed at: about 8 hours ago - Stars: 36 - Forks: 6

Robbepop/stevia
A simple (unfinished) SMT solver for QF_ABV.
Language: Rust - Size: 1.38 MB - Last synced at: 1 day ago - Pushed at: about 6 years ago - Stars: 36 - Forks: 5

ioterw/tracevm
Track the values and addresses of slots (storage variables in Solidity) inside the Ethereum contract, as well as tracking logs (Solidity events).
Language: Go - Size: 30.3 MB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 35 - Forks: 1

Koukyosyumei/Gymbo
gradient-based symbolic execution engine implemented from scratch
Language: C++ - Size: 10.1 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 35 - Forks: 0

tum-i4/munch
Greybox fuzzer for optimizing function coverage and finding low-level vulnerabilities in C programs
Language: Makefile - Size: 10 MB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 35 - Forks: 8

SVF-tools/Teaching-Software-Verification
Teaching and Learning Software Verification via SVF
Language: C++ - Size: 10.8 MB - Last synced at: 1 day ago - Pushed at: 18 days ago - Stars: 34 - Forks: 23

farosato/angr-antievasion
Final project for the M.Sc. in Engineering in Computer Science at Università degli Studi di Roma "La Sapienza" (A.Y. 2016/2017).
Language: Python - Size: 1.94 MB - Last synced at: about 12 hours ago - Pushed at: over 7 years ago - Stars: 34 - Forks: 7

tracer-x/TracerX
TracerX Symbolic Virtual Machine
Language: C - Size: 209 MB - Last synced at: 27 days ago - Pushed at: 27 days ago - Stars: 33 - Forks: 11

binsec/Rel
Binsec/Rel is an extension of Binsec that implements relational symbolic execution for constant-time verification and secret-erasure at binary-level.
Language: OCaml - Size: 1.01 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 33 - Forks: 2

catseye/SixtyPical
MIRROR of https://codeberg.org/catseye/SixtyPical : A 6502-oriented low-level programming language supporting advanced static analysis
Language: Python - Size: 1010 KB - Last synced at: 2 months ago - Pushed at: about 1 year ago - Stars: 33 - Forks: 3

winter2020/kleespectre
KLEESpectre is a symbolic execution engine with speculation semantic and cache modelling
Language: C - Size: 1.45 MB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 32 - Forks: 11

macaron-et/wasabi-aeg
Yet another implementation of AEG (Automated Exploit Generation) using symbolic execution engine Triton.
Language: Python - Size: 398 KB - Last synced at: almost 2 years ago - Pushed at: almost 7 years ago - Stars: 32 - Forks: 3

agra-uni-bremen/BinSym
Symbolic execution for RISC-V machine code based on the formal LibRISCV ISA model
Language: Haskell - Size: 116 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 31 - Forks: 3

ergrelet/themida-unmutate-bn
A Binary Ninja plugin to deobfuscate Themida, WinLicense and Code Virtualizer 3.x's mutation-based obfuscation.
Language: Python - Size: 27.3 KB - Last synced at: about 2 months ago - Pushed at: 11 months ago - Stars: 29 - Forks: 3

ispras/juliet-dynamic
Juliet C/C++ Dynamic Test Suite
Size: 38.7 MB - Last synced at: about 2 hours ago - Pushed at: about 2 years ago - Stars: 29 - Forks: 7

vorpal-research/kex
A platform for analysis of Java bytecode
Language: Kotlin - Size: 102 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 27 - Forks: 20

kyle-elliott/DVM
Symbolic Execution based on lifting amd64 to z3
Language: C# - Size: 55.7 KB - Last synced at: 4 days ago - Pushed at: 11 months ago - Stars: 27 - Forks: 2
