Displaying 1 to 9 from 9 results

Triton - Triton is a Dynamic Binary Analysis (DBA) framework

  •    C++

Triton is a dynamic binary analysis (DBA) framework. It provides internal components like a Dynamic Symbolic Execution (DSE) engine, a Taint engine, AST representations of the x86 and the x86-64 instructions set semantics, SMT simplification passes, an SMT Solver Interface and, the last but not least, Python bindings. Based on these components, you are able to build program analysis tools, automate reverse engineering and perform software verification. As Triton is still a young project, please, don't blame us if it is not yet reliable. Open issues or pull requests are always better than troll =).

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.

FStar - Verification system for effectful programs

  •    OCaml

The F* tutorial provides a first taste of verified programming in F*, explaining things by example. The F* wiki contains additional, usually more in-depth, technical documentation on F*.

sbv - SMT Based Verification in Haskell

  •    Haskell

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

sbvPlugin - Formally prove properties of Haskell programs using SBV/SMT.

  •    Haskell

Note the GHC option on the very first line. Either add this to your file, or pass -fplugin=Data.SBV.Plugin as an argument to GHC, either on the command line or via cabal. Same trick also works for GHCi. Note that the compilation will be aborted, since the theorem doesn't hold. If you load this file in GHCi, it will simply fail and drop you back to the GHCi prompt.

deepblockchains - Deep Blockchains - reference implementation of Plasma, Stark, SMT and more

  •    Go

In this research, We describe how a deep blockchain architecture can address bottlenecks of a modern single-layer blockchain without sacrificing their core benefits of immutability, security, or trustlessness. Layer 1: Root Chain - which stores/publishes the SMT (Sparse Merkle Tree) root of {Plasma Transactions, and Anchor Transactions, Plasma Accounts} etc.

go-plasma - Deep Blockchains - reference implementation of Plasma

  •    Go

Reference implementation of plasma and DeepBlockchain in Go. Wolk has augmented Plasma to support the Deep Blockchain Architecture described in this paper. Wolk is exploring a "Plasma Hybrid" implementation, where Sparse Merkle Trees are built to keep track both the canonical transactions included in each block and the latest full states. Hence the name plasma-hybrid.

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.

monosat - MonoSAT - An SMT solver for Monotonic Theories

  •    C++

MonoSAT is a SAT Modulo Theory solver for monotonic theories, over Booleans and bitvectors. It supports a wide set of graph predicates (including reachability, shortest paths, maximum s-t flow, minimum spanning tree, and acyclicity constraints). MonoSAT supports reasoning about graphs that are either directed or undirected (including graphs that may have cycles). Edges may (optionally) have constant or Bitvector weights. MonoSAT also has experimental support for constraints on finite state machines. MonoSAT can be used from the command line, or as a Python 3 library. See the installation instructions below; see also the tutorial.