Loading...

Frequently Asked Questions

Technology

Proving smart contracts correct:

Automatic programmer helps build correct DAPPs

Play video


Finding flaws (e.g., re-entrancy) by proving no double-spend occurs:

Proving no double-spend

Play video

We secure smart contracts by synthesizing their adversaries.

For background, imagine your task is to write the "inverse" of a program, e.g., the decompressor `D` for an input toy compressor `K`. The LZ77 algorithm is an example `K`. The verification specification is simple: The "K+D program" should together be the identity operation over every input bitstream. You can symbolically execute K+D to generate SMT constraints and then prove using the SMT solver Z3. Now here's the kicker: What if D is not known, but instead is a template with holes. One of my previous papers shows how you may "solve for D" [1].

What we built at Synthetic Minds is pretty much this. Except K = the input smart contract. D = an arbitrary user contract.

The specifications it handles are:

  • S1: Global assertions over K+D, e.g., `K.balance at start >= K.balance at end`
  • S2: Any `assert(predicate)` already in K.
If our prover finds a D that violates S1, means it caused K to double spend. It "discovers" novel ways to trigger re-entry or suicide, without encoding any anti-patterns. That makes a more robust way to secure against future attacks.

  1. "Path-based Inductive Synthesis for Program Inversion" PLDI 2011: pdf,
  2. "From Program Verification to Program Synthesis" POPL 2010 pdf

The system is composed of about 15000 LoC (mostly C++):

The following components have been implemented:

  • Compiler front-end for smart contracts: Solidity → BIR
  • Symbolic executor: BIR → SMT
  • Verifier (uses symbolic executor): Solidity → Proof
  • Synthesizer (uses verifier): Input contract → User contracts

Here, BIR is our Blockchain-aware Intermediate Representation, the Proof is a satisfying SMT model. BIR makes blockchain constructs such as `now` and `balance` explicit, compiles away objects, and converts message passing into shared memory.

Currently, there is no handling of inline assembly, overflow bugs (doable), and many other things. :)

A gource animation (non-informational, but pretty!):

Synthetic Minds, verifier and synthesizer development: Spring 2018

Play video
On Ethereum, "users" are executable agents. When your attackers can be executable agents, comprehensive security needs their synthesis. Without that, you are verifying under an old world model.
Our synthesizer builds on peer-reviewed work with over 900+ citations. Multiple research papers and PhD describe research on program synthesis we leverage.
  • Unit tester
  • Fuzzer
  • Simulator
  • EVM bytecode concolic or symbolic executor
  • Script kiddie
  • Explicit state model checker
With gas limits, blockchain smart contracts are only pseudo-Turing complete. The same feature that makes them tractable on the blockchain, makes them provable.
Depends on the complexity of the contract, and its public ABI. Small-sized medium-complexity contracts take hundreds to thousands of core hours. We distribute compute across our high-core server fleet, and we aim to get you results back within minutes.

It helps. As a prioritization scheme. Eventually, I expect the system to be 10% deep learning and 90% formal methods.

You still need a verifier; unless you are fine with 99% OK contracts, that loose all their entire balance 1% of the time. You also need a symbolic synthesizer; the space of user programs goes to the number of atoms very fast. The primary issue for nets for program synthesis is generalization and abstraction. Recent work by others has shown promise in interactive theorem proving.

We have experimented with using a convolutional net on top of a symbolic synthesizer. Email us if you'd like to hear more that.

Some amazing recent projects are DeepMind's Differentiable neural computer, Google Brain's AutoML, and MSR's DeepCoder. It will be a while before they can generate provably correct code.

Ecosystem

Everything except the front-end for our synthesizer remains the same. Developing a front-end compiler from other languages to BIR should take a couple of person-months each. Supporting all major languages is on the Roadmap for Fall 2018.

Only about 1% of deployed contracts have sources on Etherscan. Our objective is to improve security of the contracts, not attack them. By needing Solidity sources, we limit nefarious uses.

If there is customer demand, we will develop a decompilation tool (or use existing ones, e.g., Porosity) to re-generate Solidity sources from EVM bytecode.

Ethereum has existing static-analyzers over EVM bytecode. Oyente, MAIAN, Mythril, Slither, Rattle, Manticore, and Securify, are great examples. Almost all are pattern-based control- or data-flow analyzers. We are building an expensive, but more comprehensive and generalizable synthesis-based system:

  • Synthesizer enables readable "explanations": Our goal is to build a program synthesizer for smart contracts. As our demo-videos show, synthesis provides actionable repro code for bugs. As opposed to an error line number, you get readable code. Reading code is the most natural way for developers to inspect their contracts, and also gives them a view of what their contract's future users might look like.
  • Functional verification instead of pattern-matching: Most of the tools look for specific anti-patterns that have previously led to contract failures. These are hardcoded as data-flow or control-flow anti-patterns over EVM bytecode. We instead attempt to verify a functional assertion (e.g., "don't leak balance"). Our approach might be 100x or more compute expensive. But compute is cheap compared to human insights. By not hard-coding, we get to be more comprehensive, and future-proof.
  • Generalizes to other blockchains: Instead of analyzing EVM bytecode, we compile Solidity to a blockchain-aware intermediate representation (BIR). Think of BIR as LLVM IR for the blockchain. Means we are not as close to the wire for Ethereum, but it means we'll have a significantly easier time supporting other systems, e.g., Tezo's Liquidity.

Generation 1 on the roadmap will be powerful enough to explore the space of multiple interacting contracts.
Those are blockchain-specific. Our system proves smart contracts correct, not the platform. Historically, smart contract bugs have caused more damage than any other type of attack. We believe that will remain the case unless formal verification/synthesis are widely adopted.

Availability and roadmap

We will be rolling out invites in Summer 2018. Register below.
Most likely Fall 2018, rollout based on demand. See development Roadmap.

Eventually, yes. The current version is centralized.

Decentralizing an automatic programmer is non-trivial but that is our ultimate objective. There are a few constraints the underlying infrastructure needs to respect for a automatic programmer to be feasible (see paper). Hence the need to develop fresh versions of the compiler front end, symbolic executor, verifier, and synthesizer. Generation 0 release is the first step towards the goal.

More questions? Contact us here.