-
Notifications
You must be signed in to change notification settings - Fork 6
Introducing Elle
Elle is a project to build a formally-verified compiler that ensures a secure link between higher-level smart contract code code and the Ethereum Virtual Machine bytecode that implements it. In this document, we'll explore what Elle can do to help us make the Ethereum code we write even more secure.
Ethereum - and, more generally, Blockchains with Turing-complete scripting languages - is an exciting technology because it has the potential to fundamentally rework how we trust each other. Many transactions (such as exchanging two assets with an untrusted party in an escrow swap) have traditionally required trust in a third party, such as a bank or escrow house, to faithfully execute the transaction (only release my asset if my counterparty has turned in their asset, and vice versa).
When swapping digital assets on Ethereum, rather than needing to trust a service provider, we now only need to trust a smart contract (a program for EVM, the Ethereum Virtual Machine) that exists on the blockchain to correctly encode the transaction logic of our trusted transactions (in addition to trusting Ethereum's decentralized protocol).
But what if that smart contract is wrong?
How could it be wrong? The code implementing it could have a bug - in other words, there is a mismatch between the programmer's intentions for program behavior and what actually was produced. This has happened to smart contracts in Ethereum several times, most notably in the case of TheDAO (http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/) and the Parity wallet (https://blog.zeppelin.solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7 and https://paritytech.io/a-postmortem-on-the-parity-multi-sig-library-self-destruct/). In Ethereum, the fact that smart contracts cannot be upgraded in general after deployment can make this especially destructive.
But it's possible for the code to not have a bug but the generated bytecode to still be wrong - namely, if the compiler (the program that translates the program source code into bytecode for the EVM) has a bug and mis-translates the code.
Such a bug can be intentionally inserted into a compiler (which doesn't appear to have been the case for the bug listed below), or can be an innocent mistake, but in either case the result can be that incorrect bytecode is generated, leading to a smart contract with unexpected behavior. For example, take this bug https://blog.ethereum.org/2017/05/03/solidity-optimizer-bug/ that was found (and fixed) in Solidity some time ago. It involved Solidity incorrectly compiling constant values. If triggered, the bug could, for instance, have resulted in a token contract with a very different initial distribution than intended, causing severe consequences for whatever cryptoeconomic system might have been built on top of that token.
In the words of a Redditor (https://www.reddit.com/r/ethereum/comments/6909mm/solidity_optimizer_bug_fixed_in_0411/), “Solidity [compiler] bugs are the most terrifying kind of bugs in Ethereum. If the EVM breaks then we could plausibly hard-fork to fix it, but if the compiler is producing something wrong then it may not even be possible to tell what would have been right.”
Indeed, even more mature compiler systems for other platforms, such as GCC and LLVM, can be subject to bugs causing miscompilation as well. The CSmith project (https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf) used an automated “fuzzing”-like technique to produce test cases revealing dozens of bugs in each.
If we want to build a better, decentralized Web, we need to be able to trust its foundations - otherwise we can't trust what's built on top of it. The compiler is a key part of these foundations.
Fortunately, there is a way to make compilers that are not subject to these sorts of bugs: build the compiler inside of a proof assistant, and prove its correctness using a formal proof that can be checked by a machine. This is exemplified by the CompCert project (http://compcert.inria.fr/), which is built in the proof assistant Coq (https://coq.inria.fr/) and has accompanying proofs of correctness. In the CSmith study, no bugs were found in the parts of CompCert that had been proven correct.
Elle is a project to do this same thing, for a structured programming language (Elle-Core) that compiles down to EVM. (CompCert itself is not suited for this task, both because it assumes the target is a register machine and because of its restrictive licensing terms). Elle represents an effort to build towards* a *trustworthy compiler for Ethereum.
Elle is targeted at two main groups of users. The first are users that are building smart contracts and just want a compiler they know they can trust. These users can use Elle - either by writing their code in Elle's core syntax or through one of its frontends - to build their code, and can rest easier knowing that the compiler has not mistranslated their code. Toward this end, the Elle project encompasses building front-ends that can compile contracts in existing languages for EVM, such as the LLL language (https://media.consensys.net/an-introduction-to-lll-for-ethereum-smart-contract-development-e26e38ea6c23).
The second is the group of users that want to go farther. They want to take advantage not just of Elle's trustworthy compilation, but also its formal semantics, a specification of the meaning of the source language Elle-Core, to prove properties about their smart contracts. This can help them build confidence in the smart contracts themselves in the same way as Elle gives for the process through which they are compiled - through writing proofs in a proof assistant. The ability to formally verify smart contracts helps protect us from bugs in the smart contracts' implementations, and is a very exciting direction for Ethereum smart contract development.
Smart contracts can be seen as exemplifying Lessig's notion of “code as law” (https://www.harvardmagazine.com/2000/01/code-is-law-html). As with laws in the legal system, smart contracts written incorrectly can lead to unintended consequences. As since the compiler has such an integral role in “writing” these “laws”, trust in them is of great importance.
A huge amount of time, effort, and money is being spent on auditing smart contracts to ensure that they will behave according to their creators' intentions after deployment. This type of work shares a lot in common with formal verification, most notably that much of the work goes into creating a clear specification of intended behavior, but there is typically less emphasis on proofs of correctness.
Manual auditing is indispensable to securing Ethereum smart contracts, and probably always will be. However, source-code-level auditing has the same blind spots as source-level formal analysis. Elle can help to solve this blind spot, giving auditors assurance that the compiler will not spoil their audit results. Currently, auditors use tools such as Mythril (https://github.com/ConsenSys/mythril) on contract bytecode, so they are able to examine the compiler's output in some ways, but the bulk of high-level reasoning still happens at the source level.
Additionally, an auditing-like segment of the market is emerging in which groups with expertise in formal verification work on a contract basis to create formal specifications and proofs of correctness tailored to smart contracts coming from other companies. Since users of these services value having the highest degree of assurance possible, they will want to know that the compiler cannot compromise these guarantees. Elle can help with this.
Now that you've read this article, you should have a better understanding of the problems at hand - smart contracts not matching their creators' intent, particularly errors introduced through a bug in compilation.
You should also have a better understanding of how formally verified compilers such as Elle can help solve this problem, and who might want to use them.
If you're interested in getting involved further, here are some actions you can take:
**1. Read the rest of the documentation.
**If you're interested in learning more about Elle, check out the remainder of the docs in Elle's GitHub Wiki (NB: currently they are in the Quip folder “Project CoVe”).
2. Use Elle to compile your smart contract.
If you're writing a smart contract in LLL, you can make use of Elle's “FourL” frontend to compile your own smart contracts. See the Makefile here for information on how to build the FourL executable (you don't need Isabelle to do this.) (https://github.com/mmalvarez/eth-isabelle/tree/master/elle/generated)**. **This way you can take advantage of Elle's trustworthy compilation, without needing a detail understanding of verification.
**3. (Tool Integrators): Integrate Elle with your tool
**Ethereum has a number of tool suites for developers, such as Truffle. Maintainers of development software suites that include compilers might consider whether it makes sense to add Elle as a compiler option to the kits of compilers they provide for their users, particularly if they already support LLL through Solidity's LLL compiler.
4. Learn more about verification.
To use the full power of Elle (i.e., using the formal semantics of its source language to reason about smart contracts), first learn more about how to use proof assistants to verify programs. For a good resource on learning to use the Isabelle proof system in which Elle is built, a great resource is Concrete Semantics, which is available for free as an ebook: (http://www.concrete-semantics.org/). Once you know your way around Isabelle, it will become much easier to contribute to Elle or to use Elle in your own formal verification work.
5. Use Elle as part of your own verified smart contract development
If/once you have familiarity with formal verification in Isabelle, you may be interested in using the formal semantics of Elle to prove properties about your own smart contracts written in the Elle-Core language. The more people are using Elle to do practical verification, the easier it will be to identify pain points in its usage and ways to improve the platform.
6. Contribute to Elle
A lot of work still remains to be done on Elle, including enhancements to the LLL frontend, building new frontends (one key goal is supporting a useful subset of the Solidity language), and building higher-level reasoning tools to make it easier to do verification of smart contracts built on top of Elle. For some inspiration on what these tools might look like, check out the Verified Software Toolchain (VST) project, which has built tools along these lines on top of CompCert that can be used to interactively verify C programs: http://vst.cs.princeton.edu/
One great way to contribute is to write new documentation, or improve on existing documentation. Trying to make Elle as understandable as possible for new users is an important priority of the project.
After reading this article, hopefully you have gained a better understanding of what Elle is, what problems it can solve, and how it might be useful to you. Elle helps take the security of EVM smart contracts to the next level, because Elle comes with a proof that the output program will have the same meaning as the source.
If you decide you want to get involved, please don't hesitate to contact me (Mario Alvarez). You can find me on Gitter here: https://gitter.im/mmalvarez
If you're looking for Elle itself, you can find that here: https://github.com/mmalvarez/eth-isabelle
Thanks for reading!