symbolic-execution | Topic | Ecosyste.ms: Repos

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

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