katamaran-project/katamaran

Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.

Language: Coq - Size: 6.01 MB - Last synced: about 4 hours ago - Pushed: about 5 hours ago - Stars: 16 - Forks: 3

vorpal-research/kex

A platform for analysis of Java bytecode

Language: Kotlin - Size: 102 MB - Last synced: about 15 hours ago - Pushed: 1 day ago - Stars: 27 - Forks: 18

ucsb-seclab/greed

A symbolic execution engine for EVM smart contract binaries

Language: Python - Size: 9.91 MB - Last synced: about 7 hours ago - Pushed: 1 day ago - Stars: 36 - Forks: 2

AliveToolkit/alive2

Automatic verification of LLVM optimizations

Language: C++ - Size: 5.95 MB - Last synced: 1 day ago - Pushed: 1 day ago - Stars: 692 - Forks: 87

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 MB - Last synced: about 18 hours ago - Pushed: 2 days ago - Stars: 3,315 - Forks: 519

viperproject/silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.

Language: Scala - Size: 37.4 MB - Last synced: 1 day ago - Pushed: 1 day ago - Stars: 74 - Forks: 30

SVF-tools/Software-Security-Analysis

Software Security Analysis Course

Language: C++ - Size: 21.2 MB - Last synced: 2 days ago - Pushed: 2 days ago - Stars: 2 - Forks: 0

UnitTestBot/usvm

Universal Symbolic Virtual Machine

Language: Kotlin - Size: 59.1 MB - Last synced: 4 days ago - Pushed: 5 days ago - Stars: 9 - Forks: 6

ksluckow/awesome-symbolic-execution

A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.

Size: 44.9 KB - Last synced: 2 days ago - Pushed: 2 months ago - Stars: 1,264 - Forks: 134

cea-sec/miasm

Reverse engineering framework in Python

Language: Python - Size: 16.4 MB - Last synced: 4 days ago - Pushed: 14 days ago - Stars: 3,354 - Forks: 464

LEAFERx/Movable

A symbolic execution tool for Move, which is a smart contract language designed for Facebook Diem.

Language: Rust - Size: 385 KB - Last synced: 5 days ago - Pushed: 5 days ago - Stars: 1 - Forks: 0

BinaryAnalysisPlatform/bap

Binary Analysis Platform

Language: OCaml - Size: 8.07 MB - Last synced: 6 days ago - Pushed: 7 days ago - Stars: 1,986 - Forks: 271

jElhamm/Compiler

"This repository focuses on implementing Compiler-Related concepts."

Language: C++ - Size: 1.48 MB - Last synced: 8 days ago - Pushed: 8 days ago - Stars: 0 - Forks: 0

trailofbits/manticore

Symbolic execution tool

Language: Python - Size: 43.5 MB - Last synced: 8 days ago - Pushed: 8 months ago - Stars: 3,640 - Forks: 467

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.6 MB - Last synced: 9 days ago - Pushed: 9 days ago - Stars: 33 - Forks: 6

agra-uni-bremen/guix-symex

A Guix channel for reproducible symbolic execution research

Language: Scheme - Size: 137 KB - Last synced: 9 days ago - Pushed: 10 days ago - Stars: 0 - Forks: 0

SVF-tools/Teaching-Software-Verification

Teaching and Learning Software Verification via SVF

Language: C++ - Size: 10.5 MB - Last synced: 10 days ago - Pushed: 11 days ago - Stars: 28 - Forks: 20

Koukyosyumei/Gymbo

gradient-based symbolic execution engine implemented from scratch

Language: C++ - Size: 10.1 MB - Last synced: 10 days ago - Pushed: 5 months ago - Stars: 35 - Forks: 0

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: 3 days ago - Pushed: 3 days ago - Stars: 312 - Forks: 79

eth-sri/ilf

AI based fuzzer based on imitation learning

Language: Python - Size: 4.73 MB - Last synced: 4 days ago - Pushed: 10 months ago - Stars: 144 - Forks: 32

klee/klee

KLEE Symbolic Execution Engine

Language: C++ - Size: 8.9 MB - Last synced: 13 days ago - Pushed: 14 days ago - Stars: 2,457 - Forks: 656

UnitTestBot/UTBotCpp

Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage

Language: C++ - Size: 21.6 MB - Last synced: 3 days ago - Pushed: 3 days ago - Stars: 120 - Forks: 23

crytic/optik

Optik is a set of symbolic execution tools that assist smart-contract fuzzers

Language: Python - Size: 592 KB - Last synced: about 16 hours ago - Pushed: 10 months ago - Stars: 90 - Forks: 12

csvl/SEMA-ToolChain

ToolChain using Symbolic Execution for Malware Analysis.

Language: Batchfile - Size: 1.08 GB - Last synced: 16 days ago - Pushed: 17 days ago - Stars: 40 - Forks: 12

Consensys/mythril

Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Rootstock, Tron and other EVM-compatible blockchains.

Language: Python - Size: 47.1 MB - Last synced: 19 days ago - Pushed: 30 days ago - Stars: 3,713 - Forks: 701

tracer-x/TracerX

TracerX Symbolic Virtual Machine

Language: C - Size: 208 MB - Last synced: 18 days ago - Pushed: 18 days ago - Stars: 26 - Forks: 10

HuantWang/CONCOCTION

CONCOCTION is an automated machine learning-based vulnerability detection framework that combines static source code information and dynamic program execution traces.

Language: C - Size: 664 MB - Last synced: 13 days ago - Pushed: about 2 months ago - Stars: 7 - Forks: 2

UnitTestBot/UTBotJava

Automated unit test generation and precise code analysis for Java

Language: Kotlin - Size: 204 MB - Last synced: 13 days ago - Pushed: 2 months ago - Stars: 129 - Forks: 38

VSharp-team/VSharp

Symbolic execution engine for .NET Core

Language: C++ - Size: 54.6 MB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 46 - Forks: 29

JuanmaCopia/spf-pli

PLI is an efficient symbolic execution approach for programs that manipulate complex heap-allocated data structures with rich structural constraints

Language: Java - Size: 52.7 MB - Last synced: 1 day ago - Pushed: 1 day ago - Stars: 0 - Forks: 0

kirasys/irec

A cross platform framework to recover driver's communication interface.

Language: Python - Size: 1.82 MB - Last synced: 19 days ago - Pushed: about 3 years ago - Stars: 8 - Forks: 6

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: 3 days ago - Pushed: over 1 year ago - Stars: 170 - Forks: 11

pschanely/CrossHair

An analysis tool for Python that blurs the line between testing and type systems.

Language: Python - Size: 4.61 MB - Last synced: 20 days ago - Pushed: 21 days ago - Stars: 945 - Forks: 47

gsvgit/PySymGym

Python infrastructure to train paths selectors for symbolic execution engines.

Language: Python - Size: 8.51 MB - Last synced: 26 days ago - Pushed: 26 days ago - Stars: 1 - Forks: 1

agra-uni-bremen/BinSym

Symbolic execution for RISC-V machine code based on the formal LibRISCV ISA model

Language: Haskell - Size: 103 KB - Last synced: 23 days ago - Pushed: 23 days ago - Stars: 13 - Forks: 1

lsrcz/grisette

A monadic library for symbolic evaluation

Language: Haskell - Size: 1.91 MB - Last synced: 27 days ago - Pushed: 29 days ago - Stars: 44 - Forks: 3

formalsec/smtml

A Multi Back-end Front-end for SMT Solvers in OCaml

Language: OCaml - Size: 1.43 MB - Last synced: 24 days ago - Pushed: 24 days ago - Stars: 9 - Forks: 6

ispras/oss-sydr-fuzz

OSS-Sydr-Fuzz - OSS-Fuzz fork for hybrid fuzzing (fuzzer+DSE) open source software.

Language: C - Size: 10.7 MB - Last synced: 25 days ago - Pushed: 25 days ago - Stars: 104 - Forks: 32

lojikil/uspno.9

Unnamed SymbEx Project No. 9

Language: Python - Size: 221 KB - Last synced: 25 days ago - Pushed: over 4 years ago - Stars: 2 - Forks: 1

wisk/medusa

An open source interactive disassembler

Language: C++ - Size: 15.9 MB - Last synced: 26 days ago - Pushed: over 4 years ago - Stars: 1,031 - Forks: 91

BillHallahan/G2

Language: Haskell - Size: 57.6 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 28 - Forks: 6

metagon/ithildin

Semantic analyzer of EVM bytecode based on Mythril

Language: Python - Size: 172 KB - Last synced: 3 days ago - Pushed: about 3 years ago - Stars: 8 - Forks: 2

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: 26 days ago - Pushed: almost 2 years ago - Stars: 909 - Forks: 168

Nalen98/AngryGhidra

Use angr in Ghidra

Language: Java - Size: 25.3 MB - Last synced: about 1 month ago - Pushed: 3 months ago - Stars: 521 - Forks: 45

illera88/Ponce

IDA 2016 plugin contest winner! Symbolic Execution just one-click away!

Language: C++ - Size: 332 MB - Last synced: about 1 month ago - Pushed: 12 months ago - Stars: 1,432 - Forks: 68

crytic/etheno

Simplify Ethereum security analysis and testing

Language: Python - Size: 733 KB - Last synced: 21 days ago - Pushed: 11 months ago - Stars: 330 - Forks: 32

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 MB - Last synced: about 1 month ago - Pushed: 7 months ago - Stars: 175 - Forks: 32

thisisnotcsarg/ODC_23-24-CTFs

All CTFs solved in Offensive and Defensive Cyber Security course of Polytechnic of Milan 23/24 edition

Language: Python - Size: 12.1 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 0 - Forks: 0

Generative-Program-Analysis/GenSym

A high-performance, parallel, compilation-based symbolic execution engine

Language: Java - Size: 21.7 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 110 - Forks: 3

tum-i4/obfuscation-benchmarks

A set of programs used for benchmarking the strength of obfuscation

Language: C - Size: 46.5 MB - Last synced: 18 days ago - Pushed: about 6 years ago - Stars: 81 - Forks: 20

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: about 1 month ago - Pushed: almost 3 years ago - Stars: 121 - Forks: 17

FuzzingLabs/thoth

Cairo/Starknet security toolkit (bytecode analyzer, disassembler, decompiler, symbolic execution, SBMC)

Language: Python - Size: 5.62 MB - Last synced: about 1 month ago - Pushed: 6 months ago - Stars: 235 - Forks: 21

ispras/juliet-dynamic

Juliet C/C++ Dynamic Test Suite

Size: 38.7 MB - Last synced: 25 days ago - Pushed: about 1 year ago - Stars: 20 - Forks: 6

Symbolica/Symbolica

Symbolica's open-source symbolic execution engine.

Language: C# - Size: 1.79 MB - Last synced: 12 days ago - Pushed: over 1 year ago - Stars: 60 - Forks: 6

stp/stp

Simple Theorem Prover, an efficient SMT solver for bitvectors

Language: C++ - Size: 33.1 MB - Last synced: about 2 months ago - Pushed: 5 months ago - Stars: 482 - Forks: 129

agra-uni-bremen/symex-vp-riot

RIOT example applications for symex-vp

Language: C - Size: 9.77 KB - Last synced: about 2 months ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

agra-uni-bremen/sisl

Scheme-based Input Specification language for Concolic Testing

Language: Scheme - Size: 49.8 KB - Last synced: about 2 months ago - Pushed: almost 2 years ago - Stars: 1 - Forks: 0

agra-uni-bremen/hardbound-vp

Virtual Prototype with symbolic execution support and HardBound path analyzer

Language: C++ - Size: 31.3 MB - Last synced: about 2 months ago - Pushed: about 1 year ago - Stars: 0 - Forks: 1

agra-uni-bremen/clover

A library for concolic execution of RV32 instruction set simulators

Language: C++ - Size: 478 KB - Last synced: about 2 months ago - Pushed: 10 months ago - Stars: 1 - Forks: 1

wsong-nj/TransRacer

A symbolic analysis tool that detects transaction races for Ethereum smart contracts.

Language: Python - Size: 331 KB - Last synced: 19 days ago - Pushed: 6 months ago - Stars: 2 - Forks: 0

ispras/crusher

Language: Python - Size: 21 MB - Last synced: 20 days ago - Pushed: 20 days ago - Stars: 34 - Forks: 13

ntddk/binsec-vagrant

Easy to use BINSEC Vagrant image.

Language: Shell - Size: 1000 Bytes - Last synced: about 2 months ago - Pushed: over 6 years ago - Stars: 5 - Forks: 0

lokegustafsson/amba

Bachelor thesis, combining automatic and manual methods for binary analysis

Language: Rust - Size: 6.22 MB - Last synced: about 2 months ago - Pushed: 11 months ago - Stars: 3 - Forks: 0

fugue-re/fugue-concolic

A concolic interpreter backend for Fugue.

Language: Rust - Size: 267 KB - Last synced: 18 days ago - Pushed: 11 months ago - Stars: 4 - Forks: 1

open-crs/vulnerability_detection

Module for discovering vulnerabilities in executables 🧨

Language: Python - Size: 1.56 MB - Last synced: about 2 months ago - Pushed: 3 months ago - Stars: 2 - Forks: 1

season-lab/fuzzolic

fuzzing + concolic = fuzzolic :)

Language: C - Size: 23.8 MB - Last synced: 20 days ago - Pushed: 3 months ago - Stars: 112 - Forks: 6

trailofbits/deepstate

A unit test-like interface for fuzzing and symbolic execution

Language: Python - Size: 1.38 MB - Last synced: about 2 months ago - Pushed: 9 months ago - Stars: 804 - Forks: 99

0cherry/miasm Fork of cea-sec/miasm

Reverse engineering framework in Python

Language: Python - Size: 14.8 MB - Last synced: about 2 months ago - Pushed: over 4 years ago - Stars: 1 - Forks: 0

agra-uni-bremen/symex-vp

A concolic testing engine for RISC-V embedded software with support for SystemC peripherals

Language: C++ - Size: 31.7 MB - Last synced: about 1 month ago - Pushed: 7 months ago - Stars: 16 - Forks: 4

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: about 2 months ago - Pushed: 6 months ago - Stars: 771 - Forks: 142

FZhg/DSE-Wlang

A vanilla DSE for WLang

Language: Python - Size: 25 MB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 0 - Forks: 0

SWAT-project/SWAT

SWAT, a dynamic symbolic execution engine for Java Applications that uses ASM for on-the-fly byte code instrumentation.

Language: Java - Size: 238 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 3 - Forks: 0

quarkslab/pastis

PASTIS: Collaborative Fuzzing Framework

Language: Python - Size: 60.8 MB - Last synced: 10 days ago - Pushed: 3 months ago - Stars: 147 - Forks: 8

mgree/smoosh

The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.

Language: OCaml - Size: 3.66 MB - Last synced: about 1 month ago - Pushed: about 1 year ago - Stars: 111 - Forks: 4

PLSysSec/sys

Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code

Language: LLVM - Size: 4.55 MB - Last synced: 29 days ago - Pushed: about 2 years ago - Stars: 215 - Forks: 43

mustakimur/COIN-Attacks

COIN Attacks: on Insecurity of Enclave Untrusted Interfaces in SGX - ASPLOS 2020

Language: C++ - Size: 132 MB - Last synced: 42 minutes ago - Pushed: over 1 year ago - Stars: 26 - Forks: 12

SoftSec-KAIST/MeanDiff

Testing Intermediate Representations for Binary Analysis (ASE '17)

Language: F# - Size: 369 KB - Last synced: 20 days ago - Pushed: over 5 years ago - Stars: 77 - Forks: 11

eth-sc-comp/benchmarks

Symbolic Execution Benchmarks for Ethereum Smart Contracts

Language: Solidity - Size: 124 KB - Last synced: 4 days ago - Pushed: 4 days ago - Stars: 17 - Forks: 1

xlauko/lart

LLVM Abstraction & Refinement Tool. The goal of this tool is to provide LLVM-to-LLVM transformations that implement various program abstractions. In terms of the instruction set, the resulting programs are normal, concrete LLVM programs that can be executed and analyzed.

Language: C++ - Size: 1.06 MB - Last synced: 14 days ago - Pushed: about 1 year ago - Stars: 18 - Forks: 2

jordan9001/dobby2

Build your emulation environment as needed

Language: Python - Size: 495 KB - Last synced: 9 days ago - Pushed: about 3 years ago - Stars: 63 - Forks: 8

gio-del/ODC-Challenges-CTF

Offensive and Defensive Cybersecurity Course Challenges at polimi

Language: Python - Size: 15 MB - Last synced: 18 days ago - Pushed: 2 months ago - Stars: 0 - Forks: 0

kframework/p4-semantics

Formal Semantics of P4 in K

Language: P4 - Size: 1.01 MB - Last synced: about 2 months ago - Pushed: almost 3 years ago - Stars: 18 - Forks: 2

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: about 2 months ago - Pushed: over 1 year ago - Stars: 95 - Forks: 16

borzacchiello/seninja

symbolic execution plugin for binary ninja

Language: Python - Size: 2.46 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 226 - Forks: 22

bdcht/amoco

yet another tool for analysing binaries

Language: Python - Size: 2.84 MB - Last synced: 9 days ago - Pushed: 2 months ago - Stars: 450 - Forks: 69

HarvardPL/formulog

Datalog with support for SMT queries and first-order functional programming

Language: Java - Size: 2.85 MB - Last synced: 3 months ago - Pushed: 7 months ago - Stars: 140 - Forks: 8

palkeo/pakala

Offensive vulnerability scanner for ethereum, and symbolic execution tool for the Ethereum Virtual Machine

Language: Python - Size: 204 KB - Last synced: 2 months ago - Pushed: almost 2 years ago - Stars: 331 - Forks: 30

shafiuzzaman-md/install-klee-edk2

Install and run KLEE on edk2

Language: C - Size: 104 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 1 - Forks: 0

mximp/se-limitations-slr

Symbolic Execution Limitations - Systematic Literature Review

Size: 1.2 MB - Last synced: 18 days ago - Pushed: 10 months ago - Stars: 1 - Forks: 5

Kraks/sai

Staged Abstract Interpreters

Language: Scala - Size: 18.1 MB - Last synced: 6 days ago - Pushed: about 1 year ago - Stars: 63 - Forks: 8

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: 3 months ago - Pushed: almost 2 years ago - Stars: 96 - Forks: 10

casm-lang/casmi

CASM Numeric and Symbolic Interpreter

Language: C++ - Size: 493 KB - Last synced: 9 days ago - Pushed: 3 months ago - Stars: 1 - Forks: 0

d4em0n/exrop

Automatic ROPChain Generation

Language: Python - Size: 1.39 MB - Last synced: 3 months ago - Pushed: about 4 years ago - Stars: 272 - Forks: 27

praise106-research/Plinko-KLEE-Clang

Examples and Programs for Probabilistic Symbolic Execution project. This has been built using KLEE, LLVM, Haskell & python3.

Language: LLVM - Size: 75.1 MB - Last synced: 3 months ago - Pushed: 10 months ago - Stars: 0 - Forks: 0

tkhang1999/mini-symex-js

A mini symbolic execution engine for simple JavaScript programs

Language: JavaScript - Size: 20.5 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0

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: 3 months ago - Pushed: almost 4 years ago - Stars: 264 - Forks: 32

SQLab/CRAX Fork of S2E/s2e-old

CRAX: software CRash analysis for Automatic eXploit generation

Language: C - Size: 53.1 MB - Last synced: about 2 months ago - Pushed: over 8 years ago - Stars: 46 - Forks: 12

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: 4 months ago - Pushed: over 2 years ago - Stars: 474 - Forks: 60

HNYuuu/SeeWasm

A native symbolic execution engine for WebAssembly

Language: Python - Size: 15.5 MB - Last synced: 19 days ago - Pushed: about 1 year ago - Stars: 29 - Forks: 2

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: 21 days ago - Pushed: over 6 years ago - Stars: 35 - Forks: 9