GitHub topics: symbolic-execution
mustakimur/COIN-Attacks
COIN Attacks: on Insecurity of Enclave Untrusted Interfaces in SGX - ASPLOS 2020
Language: C++ - Size: 132 MB - Last synced at: 22 days ago - Pushed at: over 2 years ago - Stars: 25 - Forks: 12
RadeelAhmad/Sym-Link
This repository demonstrates the creation of symbolic links, providing examples and tools to exploit this.
Language: Python - Size: 36.3 MB - Last synced at: 27 days ago - Pushed at: 6 months ago - Stars: 1 - Forks: 0
PKU-ASAL/SeeWasm
A native symbolic execution engine for WebAssembly
Language: Python - Size: 15.1 MB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 43 - Forks: 3
Koukyosyumei/rhoevm
symbolic EVM execution engine written in Rust
Language: Rust - Size: 1.73 MB - Last synced at: 6 days ago - Pushed at: 11 months ago - Stars: 3 - Forks: 1
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: 7 months ago - Pushed at: 7 months ago - Stars: 73 - Forks: 10
sslab-gatech/apisan
APISan: Sanitizing API Usages through Semantic Cross-Checking
Language: C++ - Size: 34 MB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 63 - Forks: 27
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: 7 months ago - Pushed at: 9 months ago - Stars: 159 - Forks: 27
cyber-defence-campus/netgear_r6700v3_circled
Demonstrate some functionalities of Morion by generating an exploit for CVE-2022-27646 (stack buffer overflow on Netgear R6700v3 routers).
Language: Python - Size: 57.7 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 3 - Forks: 0
echancrure/Sikraken
Sikraken: A Test Suites Generator for C Code
Language: C - Size: 32.7 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 1 - Forks: 2
PKU-ASAL/WASEM
WASEM - a general symbolic execution framework for WebAssembly (WASM) binaries
Language: WebAssembly - Size: 2.34 MB - Last synced at: 3 months ago - Pushed at: 10 months ago - Stars: 13 - Forks: 6
ispras/sydr-benchmark
Sydr benchmark applications
Language: C++ - Size: 35.1 MB - Last synced at: 3 months ago - Pushed at: almost 3 years ago - Stars: 17 - Forks: 7
umutoztunc/whitesymex
Symbolic execution engine for Whitespace.
Language: Python - Size: 89.8 KB - Last synced at: 12 days ago - Pushed at: about 4 years ago - Stars: 13 - Forks: 0
PrithwishJana/CoTran
Official repository for CoTran: An LLM-based code translator for whole-program translation, fine-tuned using feedback from compiler and symbolic execution
Language: Java - Size: 183 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 2 - Forks: 0
adrianherrera/malware-s2e
Code for my blog post on using S2E for malware analysis
Language: C++ - Size: 17.6 KB - Last synced at: 3 months ago - Pushed at: about 6 years ago - Stars: 25 - Forks: 4
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 at: 3 months ago - Pushed at: over 2 years ago - Stars: 19 - Forks: 2
tniessen/hyena0
Prototype implementation of a hyperbug finder for ∀∃-safety hyperproperties to accompany the OOPSLA 2024 paper "Finding ∀∃ Hyperbugs using Symbolic Execution" by Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, and Georg Weissenbacher.
Language: C++ - Size: 52.7 KB - Last synced at: about 1 month ago - Pushed at: 9 months ago - Stars: 2 - Forks: 0
Symbolica/Symbolica
Symbolica's open-source symbolic execution engine.
Language: C# - Size: 1.79 MB - Last synced at: 6 days ago - Pushed at: 11 months ago - Stars: 65 - Forks: 6
nmeum/qsym
A symbolic executor for the QBE intermediate language
Language: Rust - Size: 107 KB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 0
praise106-research/Plinko-KLEE-Clang
Examples and Programs for Probabilistic Symbolic Execution project. This has been built using KLEE, LLVM, Haskell & python3.
Language: C++ - Size: 76.1 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 1 - Forks: 0
Research-Tools-PAVT/klee Fork of klee/klee
KLEE Symbolic Execution Engine
Language: C++ - Size: 8.38 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0
w4z3d/JBMF
A java bytecode manipulation library written in rust
Language: Rust - Size: 53.7 KB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 4 - Forks: 1
formalsec/wasp
WASP was superseded by: https://github.com/OCamlPro/owi
Language: OCaml - Size: 152 MB - Last synced at: 3 months ago - Pushed at: 11 months ago - Stars: 14 - Forks: 1
cyber-defence-campus/morion
Morion is a PoC tool to experiment with symbolic execution on real-word (ARMv7) binaries.
Language: Python - Size: 546 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 4 - Forks: 0
vorpal-research/kex
A platform for analysis of Java bytecode
Language: Kotlin - Size: 102 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 27 - Forks: 20
eth-sc-comp/benchmarks
Symbolic Execution Benchmarks for Ethereum Smart Contracts
Language: Solidity - Size: 142 KB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 17 - Forks: 3
cleanunicorn/mythos
CLI client for the MythX API
Language: TypeScript - Size: 1.11 MB - Last synced at: 16 days ago - Pushed at: over 2 years ago - Stars: 20 - Forks: 6
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 at: 11 months ago - Pushed at: 11 months ago - Stars: 13 - Forks: 5
shba24/BinClass
Recovering Object information from a C++ compiled Binary/Malware (mainly written for PE files) , linked dynamically and completely Stripped.
Language: C - Size: 18 MB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 7 - Forks: 0
Nalen98/AngryGhidra
Use angr in Ghidra
Language: Java - Size: 25.2 MB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 536 - Forks: 47
wisk/medusa
An open source interactive disassembler
Language: C++ - Size: 15.9 MB - Last synced at: 12 months ago - Pushed at: almost 6 years ago - Stars: 1,039 - Forks: 92
iamywang/bp-security-framework
Research Artifact of HPCA 2024 Paper: *Modeling, Derivation, and Automated Analysis of Branch Predictor Security Vulnerabilities*.
Language: Rust - Size: 153 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 5 - Forks: 1
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: about 1 year ago - Pushed at: about 1 year ago - Stars: 35 - Forks: 1
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 at: about 1 year ago - Pushed at: over 1 year ago - Stars: 23 - Forks: 0
agra-uni-bremen/guix-symex
A Guix channel for reproducible symbolic execution research
Language: Scheme - Size: 163 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
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
SQLab/symgdb
SymGDB - symbolic execution plugin for gdb
Language: Python - Size: 1.79 MB - Last synced at: about 1 year ago - Pushed at: about 7 years ago - Stars: 213 - Forks: 26
jElhamm/Compiler-Design
"This repository focuses on implementing Compiler-Related concepts."
Language: C++ - Size: 1.48 MB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
trailofbits/deepstate-test-suite
Automated continuous testing integration using DeepState
Language: C++ - Size: 177 KB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 5 - Forks: 3
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: about 3 years ago - Stars: 98 - Forks: 10
Koukyosyumei/Gymbo
gradient-based symbolic execution engine implemented from scratch
Language: C++ - Size: 10.1 MB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 35 - Forks: 0
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
VSharp-team/VSharp
Symbolic execution engine for .NET Core
Language: C++ - Size: 54.6 MB - Last synced at: over 1 year ago - Pushed at: over 1 year 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.4 MB - Last synced at: 6 months ago - Pushed at: 6 months 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 at: about 1 year ago - Pushed at: over 4 years ago - Stars: 8 - Forks: 6
lojikil/uspno.9
Unnamed SymbEx Project No. 9
Language: Python - Size: 221 KB - Last synced at: about 1 year ago - Pushed at: over 5 years ago - Stars: 2 - Forks: 1
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
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
agra-uni-bremen/symex-vp-riot
RIOT example applications for symex-vp
Language: C - Size: 9.77 KB - Last synced at: over 1 year ago - Pushed at: over 2 years 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 at: over 1 year ago - Pushed at: almost 3 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 at: over 1 year ago - Pushed at: over 2 years 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 at: over 1 year ago - Pushed at: about 2 years 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 at: about 1 year ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0
ntddk/binsec-vagrant
Easy to use BINSEC Vagrant image.
Language: Shell - Size: 1000 Bytes - Last synced at: over 1 year ago - Pushed at: over 7 years ago - Stars: 5 - Forks: 0
fugue-re/fugue-concolic
A concolic interpreter backend for Fugue.
Language: Rust - Size: 267 KB - Last synced at: about 1 year ago - Pushed at: about 2 years ago - Stars: 4 - Forks: 1
0cherry/miasm Fork of cea-sec/miasm
Reverse engineering framework in Python
Language: Python - Size: 14.8 MB - Last synced at: over 1 year ago - Pushed at: almost 6 years ago - Stars: 1 - Forks: 0
FZhg/DSE-Wlang
A vanilla DSE for WLang
Language: Python - Size: 25 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
gio-del/ODC-Challenges-CTF
Offensive and Defensive Cybersecurity Course Challenges at polimi
Language: Python - Size: 15 MB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
kframework/p4-semantics
Formal Semantics of P4 in K
Language: P4 - Size: 1.01 MB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 18 - Forks: 2
tweag/pirouette 📦
Language-generic workbench for building static analysis
Language: Haskell - Size: 1.54 MB - Last synced at: 3 months ago - Pushed at: almost 2 years ago - Stars: 47 - Forks: 2
liuzikai/klc3
"KLEE on LC-3," Symbolic Execution Engine for LC-3 Programs
Language: C++ - Size: 17.7 MB - Last synced at: 25 days ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0
shafiuzzaman-md/install-klee-edk2
Install and run KLEE on edk2
Language: C - Size: 104 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
mximp/se-limitations-slr
Symbolic Execution Limitations - Systematic Literature Review
Size: 1.2 MB - Last synced at: 5 months ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 5
formalsec/waspc 📦
OWI's C frontend now in https://github.com/OCamlPro/owi/pull/100
Language: C - Size: 305 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 2
tkhang1999/mini-symex-js
A mini symbolic execution engine for simple JavaScript programs
Language: JavaScript - Size: 20.5 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
SQLab/CRAX Fork of S2E/s2e-old
CRAX: software CRash analysis for Automatic eXploit generation
Language: C - Size: 53.1 MB - Last synced at: over 1 year ago - Pushed at: almost 10 years ago - Stars: 46 - Forks: 12
giladreich/angr_ctf Fork of jakespringer/angr_ctf
Angr CTFs covering topics from basics to intermediate.
Language: Python - Size: 3.29 MB - Last synced at: 2 days ago - Pushed at: almost 4 years ago - Stars: 10 - Forks: 1
JacquesCarette/Retrodictive
For exploring Symbolic Evaluation of Quantum Circuits, forwards and BACKWARDS
Language: TeX - Size: 49.6 MB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 0
one2blame/the-dark-arts
Repository to contain my notes from my self-study of binary exploitation and reverse engineering.
Size: 1.54 MB - Last synced at: 4 months ago - Pushed at: over 3 years ago - Stars: 3 - Forks: 2
can-lehmann/pathbeaver
Symbolic execution of LLVM IR
Language: C++ - Size: 58.6 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 13 - Forks: 1
polystat/symex
Symbolic Execution engine for finding bugs in EO programs
Language: Java - Size: 15.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0
rvprasad/verification-validation-course 📦
Verification and Validation course offered at Kansas State University in Fall'15, '16, and '17
Size: 37 MB - Last synced at: over 1 year ago - Pushed at: almost 8 years ago - Stars: 1 - Forks: 0
sambacha/hevm-ts
symbolic evm in typescript
Language: TypeScript - Size: 209 KB - Last synced at: 3 days ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
shalan12/UserGuided-SymbolicExecution
A framework for user-guided symbolic execution (with visualization) of LLVM Bitcode. A demo of the project can be viewed at https://www.youtube.com/watch?v=0VNe4BjjF90
Language: C++ - Size: 84.8 MB - Last synced at: 12 months ago - Pushed at: over 8 years ago - Stars: 6 - Forks: 1
mchalupa/bubaak-lee Fork of klee/klee
BubaaK-LEE: A fork of KLEE Symbolic Execution Engine used in the tool Bubaak
Language: C++ - Size: 9.43 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0
sh4m2hwz/triton_ast_llvm_ir_translator
pluggable tool to convert an unrolled TritonAST to LLVM-IR, optimize it and get back to TritonAST
Language: C++ - Size: 20.5 KB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 5 - Forks: 2
boogie-org/symbooglix
Symbolic Execution Engine for Boogie
Language: C# - Size: 2.26 MB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 27 - Forks: 4
enzet/program-model
Formal model of program execution, symbolic execution, and taint tracking
Language: TeX - Size: 1.02 MB - Last synced at: 3 months ago - Pushed at: over 4 years ago - Stars: 7 - Forks: 2
karthik-d/type-inference-tools-playground
Resource compilation, experiments, and tests on Symbolic Execution, Type Inference and Property-Guided Testing of python programs
Language: Python - Size: 3.79 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
Pigrecos/Triton4Delphi
The Triton - Dynamic Binary Analysis (DBA) framework - by JonathanSalwan binding for Delphi
Language: Pascal - Size: 181 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 8 - Forks: 5
nju-Nicko/MethodInvocationSequenceTracer
基于符号执行的方法调用序列追踪工具
Language: Java - Size: 120 KB - Last synced at: over 1 year ago - Pushed at: almost 7 years ago - Stars: 3 - Forks: 0
ppmx/sudoku-solver
Sudoku Solver using Z3
Language: C++ - Size: 90.8 KB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 18 - Forks: 7
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
adrianherrera/kaitai-s2e
Code for my blog post on combining S2E and Kaitai Struct
Language: C++ - Size: 8.79 KB - Last synced at: 3 months ago - Pushed at: about 6 years ago - Stars: 15 - Forks: 1
GaloisInc/surveyor
A symbolic debugger for C/C++ (via LLVM), machine code, and JVM programs
Language: Haskell - Size: 802 KB - Last synced at: 16 days ago - Pushed at: over 4 years ago - Stars: 18 - Forks: 1
season-lab/SymFusion
SymFusion: Hybrid Instrumentation for Concolic Execution
Language: C - Size: 2.85 MB - Last synced at: about 1 year ago - Pushed at: about 2 years ago - Stars: 18 - Forks: 5
COMSYS/SymbolicLivenessAnalysis
Symbolic Liveness Analysis of real-world software building upon KLEE to detect liveness violations (e.g. infinite loop bugs)
Language: C++ - Size: 6.34 MB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 14 - Forks: 1
binsec/haunted
Binsec/Haunted is an extension of Binsec to verify speculative constant-time and detect Spectre attacks.
Language: OCaml - Size: 860 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 15 - Forks: 1
BanafshehAzizi/SEET
A symbolic executor for ETL transformations
Language: Java - Size: 52.9 MB - Last synced at: almost 2 years ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0
zhangysh1995/smt-data-processing
several scripts to process data from SMT solvers
Language: Python - Size: 454 KB - Last synced at: almost 2 years ago - Pushed at: almost 8 years ago - Stars: 0 - Forks: 0
isstac/spf-wca
Tool for algorithmic complexity analysis based on symbolic execution
Language: Java - Size: 6.05 MB - Last synced at: almost 2 years ago - Pushed at: almost 7 years ago - Stars: 9 - Forks: 9
calincru/diploma-thesis
Bachelor thesis: Formal analysis of iptables configurations for network verification
Language: TeX - Size: 8.1 MB - Last synced at: almost 2 years ago - Pushed at: about 8 years ago - Stars: 2 - Forks: 0
wy7980/Notes
Some notes about computer science，software engineering and research.
Size: 583 KB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 0
sciencemanx/symexec
Basic x86 Symbolic Execution for educational purposes
Language: Python - Size: 8.79 KB - Last synced at: almost 2 years ago - Pushed at: about 8 years ago - Stars: 18 - Forks: 3
Futaki-Futaba/angr-sample
angr 7向けのサンプルプログラムです
Language: Python - Size: 5.86 KB - Last synced at: almost 2 years ago - Pushed at: over 7 years ago - Stars: 4 - Forks: 0
ertlnagoya/lwip-bug-finder
lwipのバグを半自動検出くん。First introduced in 「2018年 暗号と情報セキュリティシンポジウム」（SCIS2018).
Language: Python - Size: 549 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 13 - Forks: 0
JuanmaCopia/lissa
LISSA: An efficient symbolic execution approach for programs manipulating complex heap-allocated data structures.
Language: Java - Size: 43.1 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 0
JuanmaCopia/SymSolve
SymSolve is an efficient bounded exhaustive solver for symbolic structures with complex representation invariants.
Language: Java - Size: 3.01 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0
George056/Symbolic_Math
This is a simple Common Lisp program that perform simple calculus calculations.
Language: Common Lisp - Size: 35.2 KB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 4 - Forks: 0
porglezomp/hyalite
A bounded model checker for an IMP-style imperative language.
Language: Rust - Size: 10.7 KB - Last synced at: 4 months ago - Pushed at: over 6 years ago - Stars: 7 - Forks: 0
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
