Displaying 1 to 7 from 7 results

manticore - Symbolic execution tool

  •    Python

Manticore is a symbolic execution tool for analysis of binaries and smart contracts. Manticore is supported on Linux and requires Python 2.7. Ubuntu 16.04 is strongly recommended. Ethereum smart contract analysis requires the solc program in your $PATH.

Casper - A compiler for automatically re-targeting sequential Java code to Apache Spark.

  •    Java

Casper is a compiler for automatically re-targeting sequential Java code fragments to Apache Spark. Casper works by synthesizing high level MapReduce program specifications from raw un-annotated sequential Java source code and using the synthesized specificiations to generate Apache Spark code. The most recent release version for Casper is v0.1.1.Casper has been implemented as an extension of Polyglot 2.6.1.

z3-mode - An interactive development environment for SMT-LIB files and Z3

  •    Emacs

z3-mode provides an interactive development environment for checking the satisfiability of logical formula written in SMTLIBv2 with backends such as Z3. If you use a version of Emacs prior to 24 that doesn’t include package.el, you can get it from here.




jfs - Constraint solver based on coverage-guided fuzzing

  •    C++

JFS (JIT Fuzzing Solver) is an experimental constraint solver designed to investigate using coverage guided fuzzing as an incomplete strategy for solving boolean, BitVector, and floating-point constraints. JFS supports constraints in the SMT-LIBv2 constraint langauge in the QF_BV, QF_BVFP, and QF_FP logics. JFS's primary purpose however is solve floating-point constraints.

vim-smt2 - A VIM plugin that adds support for the SMT-LIB2 format (including Z3's extensions)

  •    Vim

A VIM plugin that adds syntax highlighting for the SMT-LIB2 format, i.e. *.smt2 files. Although SMT-LIB2 is the standard language supported by most SMT solvers, some of them introduce custom language extensions. Such extensions may range from syntactical sugar to fine-grained control over the underlying solver-procedure. Besides the base SMT-LIB2 language, this plugin supports the extensions used by the Z3 SMT solver.

z3_and_angr_binary_analysis_workshop - Code and exercises for a workshop on z3 and angr

  •    Python

Originally delivered by Sam Brown at Steelcon and hack.lu 2018, this was a three hour workshop introducing attendees to using Z3 and angr for binary analysis. The workshop provided an introduction to SMT solvers, the Z3 SMT solver and its python library and the angr binary analysis framework. Through out the workshop exercises were provided which aimed to demonstrate potential applications of the technology to assist security researchers in carrying out reverse engineering and vulnerability research.