All Projects → klee → Klee

klee / Klee

Licence: other
KLEE Symbolic Execution Engine

Programming Languages

C++
36643 projects - #6 most used programming language
c
50402 projects - #5 most used programming language
CMake
9771 projects
python
139335 projects - #7 most used programming language
LLVM
166 projects
shell
77523 projects

Projects that are alternatives of or similar to Klee

G2
No description or website provided.
Stars: ✭ 24 (-98.7%)
Mutual labels:  symbolic-execution
Awesome Symbolic Execution
A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
Stars: ✭ 634 (-65.75%)
Mutual labels:  symbolic-execution
Etheno
Simplify Ethereum security analysis and testing
Stars: ✭ 77 (-95.84%)
Mutual labels:  symbolic-execution
Cgpwn
A lightweight VM for hardware hacking, RE (fuzzing, symEx, exploiting etc) and wargaming tasks
Stars: ✭ 345 (-81.36%)
Mutual labels:  symbolic-execution
Crosshair
An analysis tool for Python that blurs the line between testing and type systems.
Stars: ✭ 586 (-68.34%)
Mutual labels:  symbolic-execution
Wasabi Aeg
Yet another implementation of AEG (Automated Exploit Generation) using symbolic execution engine Triton.
Stars: ✭ 23 (-98.76%)
Mutual labels:  symbolic-execution
malware-s2e
Code for my blog post on using S2E for malware analysis
Stars: ✭ 21 (-98.87%)
Mutual labels:  symbolic-execution
Bap
Binary Analysis Platform
Stars: ✭ 1,385 (-25.18%)
Mutual labels:  symbolic-execution
Deepstate
A unit test-like interface for fuzzing and symbolic execution
Stars: ✭ 603 (-67.42%)
Mutual labels:  symbolic-execution
Ponce
IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
Stars: ✭ 1,066 (-42.41%)
Mutual labels:  symbolic-execution
Symbolic Execution
History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)
Stars: ✭ 395 (-78.66%)
Mutual labels:  symbolic-execution
Tigress protection
Playing 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.
Stars: ✭ 550 (-70.29%)
Mutual labels:  symbolic-execution
Medusa
An open source interactive disassembler
Stars: ✭ 946 (-48.89%)
Mutual labels:  symbolic-execution
Stp
Simple Theorem Prover, an efficient SMT solver for bitvectors
Stars: ✭ 341 (-81.58%)
Mutual labels:  symbolic-execution
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.
Stars: ✭ 94 (-94.92%)
Mutual labels:  symbolic-execution
smoosh
The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.
Stars: ✭ 86 (-95.35%)
Mutual labels:  symbolic-execution
Angora
Angora is a mutation-based fuzzer. The main goal of Angora is to increase branch coverage by solving path constraints without symbolic execution.
Stars: ✭ 669 (-63.86%)
Mutual labels:  symbolic-execution
Mythril
Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains.
Stars: ✭ 1,968 (+6.32%)
Mutual labels:  symbolic-execution
Pakala
Offensive vulnerability scanner for ethereum, and symbolic execution tool for the Ethereum Virtual Machine
Stars: ✭ 97 (-94.76%)
Mutual labels:  symbolic-execution
Apisan
APISan: Sanitizing API Usages through Semantic Cross-Checking
Stars: ✭ 46 (-97.51%)
Mutual labels:  symbolic-execution

KLEE Symbolic Virtual Machine

Build Status Build Status Build Status Coverage

KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure. Currently, there are two primary components:

  1. The core symbolic virtual machine engine; this is responsible for executing LLVM bitcode modules with support for symbolic values. This is comprised of the code in lib/.

  2. A POSIX/Linux emulation layer oriented towards supporting uClibc, with additional support for making parts of the operating system environment symbolic.

Additionally, there is a simple library for replaying computed inputs on native code (for closed programs). There is also a more complicated infrastructure for replaying the inputs generated for the POSIX/Linux emulation layer, which handles running native programs in an environment that matches a computed test input, including setting up files, pipes, environment variables, and passing command line arguments.

For further information, see the webpage.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].