Current use of web-app-like development practices for smart contracts is not working. People have lost over 4.1M ETH due to code bugs in these contracts, aka decentralized applications (Dapps). That equals $1.8B at current exchange rates, or $500M at the time of loss. The execution environment is "deploy once, change never", which resembles hardware and space applications. NASA/Airbus use formal methods to check this kind of software. Dapps need similar tools.
I have worked on formal methods since 2006. In my PhD on program synthesis, I reduced checking code properties to theorems that could be proven mechanically. Incidentally, a full program was not required. The program could have "holes" and the prover would “fill” the holes by synthesizing code. I took those ideas to synthetic biology in my postdoc and previous company.
In 2016 when I started to look at smart contracts, I realized those ideas could help build robust Dapps, and maybe prevent them from losing $100M+/year. In June 2016, a Solidity vulnerability was discussed (June 10), but the DAO was deemed immune (June 12), right before it was exploited (June 17), losing ~$150M. In 2017, another ~$300M was lost to the Parity multisig bug. This year, I built a system to help mitigate future failures.
The core insight requires some background: Imagine you wrote a lossless compression algorithm `K` (e.g., LZ77 or LZW). Would it not be amazing to synthesize the decompressor `D` automatically? The invariant for `K+D` is the identity function. So if we had a `D` with holes, we could use a prover to verify the identity invariant and “solve for D” simultaneously. Now, what if your `K` was a blockchain smart contract, and `D` an arbitrary user contract? If we want K to be immune to double spends, we could ask for `K+D` that violates the invariant “K’s balance at start >= K’s balance at end”. Not only would we formally verify properties, we would synthesize a specific `D` that helps explain any violations.
Here's how it works: Our tool has `prove` and `autocode` modes. For a smart contract, `prove` validates its properties while `autocode` will generate user contracts that break it—if any exist. Our servers will aim for turnaround times of minutes allowing use in CI, instead of weeks-long human audits. Two demo screencasts are online: http://synthetic-minds.com/pages/faq.html.
There are 3 steps under the hood. The 1st step is a source-to-source compiler from Solidity to a shared-memory, non-object, explicit Blockchain-state Intermediate Representation (BIR). BIR is not Solidity specific, so we could compile Ethereum’s Vyper or Tezo’s Liquidity to it, but Solidity’s traction makes it a natural place to start. The 2nd step is a symbolic executor that converts BIR to an “equation”. Think of symbolic execution as execution that traverses every path and without explicit values. E.g., `func a(int x) { y = x + 1; z = y * y; return z; }` would translate to `a(x) = (x + 1).(x + 1)`. Symbolic execution allows us to convert entire programs into an SMT equation. SMT is a theorem proving language used by many automated solvers, e.g., Z3, CVC4. The most novel, 3rd step, augments a user contract with holes for function bodies. That encodes any arbitrary future user contract. The solver can fill holes that (dis)prove combined properties. This simultaneously validates global invariants, and provides readable code if problematic user contracts exist.
Formal methods are sometimes hard to use, but it turns out that for smart contracts we can bypass the major issues (false positives, esoteric bugs found, and difficult-to-explain findings). First, most false positives come from inevitable approximations that formal analyses have to make, so they can terminate while analyzing code that itself might not terminate, i.e., Undecidability of analyzing Turing-complete languages. Gas limits truncate executions, which means we get to skip those approximations. Second, when esoteric (weird and obscure) bugs cause failures in normal web services you have to weigh the time and cost of fixing it against the potential loss, which might be negligible. But because smart contracts are immutable, any esoteric code path can be fatal to the entire Dapp, so there is no such tradeoff. Lastly, in contrast with the infinite variability of interfaces for normal web services, the uniformity of blockchain actors provides a template, enabling us to synthesize code as developer-friendly explanations of behavior.
Over 12+ years of work, there is one question I have repeatedly asked: Can we trade off human insight at the expense of compute power? Current alternatives for securing contracts look for 10-20 anti-patterns, built from human insights observing past failures. In contrast, our approach asks for a functional invariant (e.g., no double spend), which might be 100x or more expensive to solve. Compute is cheap though, and our ability to find future failures is only limited by the amount we expend on `autocode`.
The first prototype is operational now, and I am sending out beta invites next week: http://synthetic-minds.com. Excited to hear thoughts from the community!
by Andrey
Azimov