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" .
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:
The following components have been implemented:
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!):
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.
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:
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.