Skip to content

Latest commit

 

History

History
255 lines (166 loc) · 11.8 KB

README.md

File metadata and controls

255 lines (166 loc) · 11.8 KB
Raw

Motoko-san

Disclaimer — this is an early prototype; in particular:

  • This project comes with no guarantees whatsoever.
  • The currently supported subset of Motoko is insufficient for most real-world applications.
  • DFINITY currently has no plans to continue the development of Motoko-san.

Motoko-san is a prototype code-level verifier for Motoko. The project started at the DFINITY Foundation as a way to demonstrate that Motoko (and the Internet Computer in general) are well-suited for developing formally verified Web3 software.

Jump to:

Introduction — Overview | Formal specification | Static vs. dynamic assertions | Testing vs. formal verification | Precondition of public functions | Examples

Contributing — Building | Running | Testing | File structure

Currently supported features

Further information

Introduction

Overview

The verifier is implemented as a moc compiler feature. When moc --viper $FILE is invoked, the Motoko source code from $FILE is first translated into the Viper intermediate verification language (currently emitted into stdout) and then compiled. The generated Viper program can be submitted to the Viper tool. If the generated Viper program verifies, this implies that the Motoko source code respects the formal code specification, e.g., canister invariants, and that Viper established the corresponding formal proof of correctness.

Formal code specification

Formal code specifications are written as part of the Motoko source code. These specifications are static, i.e., they do not affect the canister's runtime behavior. If a Motoko canister is compiled with moc --viper, it may contain static code specifications defined via the following keywords (exp : Type below denotes an expression of type Type):

  • assert:invariant (exp : Bool); — actor-level invariant; must be ensured right after canister initialization and after every atomic block execution. May appear only at the level of actor members.
  • assert:1:async (exp : Bool); — an await async { ... } block may include this as the first statement; the intention is two-fold:
    • at most one instance of this code block can be pending execution.
    • specify that the property exp is intended to hold when this block execution begins.
    • require that the tool actually checks whether this assumption holds (given this actor's entire source code)
  • assert:system (exp : Bool); — a static assertion that asks the verifier to prove that the property exp holds. Useful while designing code-level canister specifications.

Note: the above syntax is provisional. It has been used so far to avoid introducing breaking changes to the Motoko grammar. In the future, Motoko-san may switch to bespoke syntax for code specifications.

Static vs. dynamic assertions

The expression assert <exp> (which is already available in Motoko proper) means a dynamic assertion, i.e., a runtime check of the Boolean condition <exp>. Note, however, that adding an assert <exp> expression (for some Boolean expression <exp>) affects the static verification of the canister. Concretely, the verifier will take for granted that <exp> holds after this statement (since any execution violating this assumption would trap).

Testing vs. formal verification

Dynamic assertions can also be used for testing. Of course, the downside of testing is that if is typically not feasible to test against all possible scenarios; the untested scenarios can be exploited by an attacker. In contrast, formal verification relies on statically known information to prove the absence of attacks.

Precondition of public functions

In particular, dynamic assertions are very useful for specifying preconditions of an actor's public functions (i.e., functions exposed in the Candid API configuration). Since such functions can be invoked by anyone; the identity of the caller is statically unknown. It is thus necessary to check all of the assumptions at runtime, by writing assert <exp>(here, <exp> denotes some Bool expression representing a function's precondition). Conversely, writing assert:system <exp> at the top of a public function will never verify because Motoko-san has zero knowledge about the caller.

Examples

To get a better idea about how code-level specifications help formalize what a Motoko canister is intended to do, please refer to the examples in moc/test/viper.

Contributing to Motoko-san

Building the Motoko compiler

  1. Clone https://github.com/dfinity/motoko 
    cd motoko
  2. Install Nix: 
    curl -L https://nixos.org/nix/install | sh
  3. Obtain Nix cache (this speeds up the following steps): 
    nix-env -iA cachix -f https://cachix.org/api/v1/install
cachix use ic-hs-test
  4. Enter Nix shell (the first run of this command may take a while): 
    nix-shell
  5. Finally, build the Motoko compiler runtime and the compiler itself: 
    [nix-shell:motoko]$ make -C rts
[nix-shell:motoko]$ make -C src

Running Motoko-san 

[nix-shell:motoko] moc -viper input.mo > output.vpr

You may then verify the output.vpr file using Viper. Soon, there will be an interactive IDE integration for VS Code, s.t. the outputs do not need to be verified by manually invoking Viper.

Testing Motoko-san

After modifying the code and recompiling moc, don't forget to test the changes by running

[nix-shell:motoko]$ make -C test/viper

Each test case consists of a (formally specified) Motoko source file, say, $TEST (e.g., invariant.mo) and the expected test results, represented via a triplet of files:

  • test/viper/ok/$TEST.vpr.ok — what the Motoko compiler is expected to generate; this should be a Viper program.
  • test/viper/ok/$TEST.silicon.ok — verification errors reported by the Viper tool. For example: 
    [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. ([email protected])
    Note: Silicon is the name of one of the backends supported by Viper.
  • test/viper/ok/$TEST.silicon.ret.ok — the return code from running Viper on this input. For example: 
    Return code 1

File structure

The implementation of Motoko-san consists of the following source files:

  • src/viper/syntax.ml — the Viper AST implementation.
  • src/viper/pretty.ml — the Viper pretty printer. Used for serializing Viper AST into text.
  • src/viper/trans.ml — the Motoko-to-Viper translation. Implements the logic of Motoko-san.

Currently supported language features

Motoko-san is an early prototype. The tool supports only a modest subset of Motoko proper, which is not sufficient for most real-world applications. However, we hope that Motoko-san will enable the community to build more sophisticated Motoko code-level verifiers, simply by extending this prototype. In particular, the tool enables verifying reentrancy safety in simple (asynchronous) smart contracts (e.g., test/viper/claim.mo).

Below, we summarize the language features that Motoko-san currently supports. For each feature, we try to estimate the complexity of its natural generalization. For that purpose, we use the terms trivial (e.g., extending code by analogy), simple (we already know how to do it), hard (more discussions would be needed to figure out the exact approach or feasible level of generality).

  • Literal actor declarations — The only supported top-level entity is an actor literal:

    actor ClaimReward { ... } and actor { ... }

    Extending to actor classes and modules is simple.

  • Primitive types — Only integer and Boolean types are supported (including literals of these types):

    • Bool: not, or, and, implies (short circuiting semantics)

    • Int: +, /, *, -, %

    • Relations: ==, !=, <, >, >=, <=

    Supporting Text, Nat, Int32, tuples, record, and variants is simple.

    Supporting Option<T> types is trivial.

    Supporting async types is hard.

    Supporting Float, function types, co-inductive, mutually recursive, and sub-typing is hard.

    Supporting container types and generic types, e.g., arrays ([var T]) and HashMap<K, V>, is hard.

  • Declarations

    • Actor fields

      • Mutable: var x = ...
      • Immutable: let y = ...
      • Fields may not be initialized via block expressions: let z = { ... };

    • Public functions — Only functions of async () type with no arguments are supported:

      public func claim() : async () = { ... };

      Supporting function arguments and return values is simple.

    • Private functions — Currently not supported (extension is simple).

    • Local declarations — Only local variable declarations with trivial left-hand side are supported:

      var x = ...; and let y = ...;

      Supporting pattern matching declarations (e.g., let (a, b) = ...;) is simple.

  • Statements

    • ()-typed block statements and sequential composition:

      { var x = 0 : Int; x := x + 1; }

      Supporting let y = do { let y = 1 : Int; y + y }; is simple.

    • Runtime assertions: assert i <= MAX;

    • Assignments (to local variables and actor fields): x := x + 1

    • if-[else] statements

      Supporting pattern-matching is conceptually simple.

    • while loops (loop invariants are not currently supported)

      Supporting for loops is simple.

      Supporting break and continue is simple.

    • await async { ... } — Asynchronous code blocks that are immediately awaited on.

      Supporting general awaits and asyncs is hard.

      Supporting async function calls is simple.

  • Static code specifications — Note that the syntax is provisional:

    • assert:invariant — Canister-level invariants

    • assert:1:async — Async constraints (at block entry)

      Extending to support, e.g., assert:N:async constraints (for N > 1) is simple.

      Extending to support async constraints at block exit is trivial.

    • assert:func — Function preconditions

    • assert:return — Function postconditions

    • assert:system — Compile-time assertions

    Loop invariants — Extension is simple.

    Pure functions — The tool could be easily extended with a keyword, e.g., @pure, to specify functions that are verifier to be side-effect free; such functions could be used inside other code specifications, e.g., assert:invariant is_okay() for some @pure func is_okay() : Bool. This feature requires private functions.

Further information

If you have questions, please contact the Motoko compiler developers. You may do that, e.g., by filing a ticket via https://github.com/dfinity/motoko/issues/new (please add viper into the labels).