/Movable

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

Primary LanguageRustOtherNOASSERTION

Movable

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

Diem Setup

Clone Diem to the parent directory of Movable. The directory structure should look like:

|_ diem
|_ Movable

Diem repository should be checkout to tag diem-framework-v1.2.0. Other versions are untested.

Usage

cargo run <BYTECODE_FILE> -f <FUNCTION_NAME>

Roadmap

Engine

  • Transaction configuration
  • Symbolic execution configuration

Symbolic Chain State

  • Start from states other than genesis
  • Symbolic writeset
  • Custom data store

Symbolic VM

  • Vector bound check (in plugin or not?)
  • Native function modelling
  • Stdlib test
  • More benchmarks
  • Docking with plugin system (intarith plugin running)
  • Gas infrastructure
  • Debug and log infrastructure

Plugin System

  • Single instruction listening support (intarith plugin added)
  • Verification plugin support