Introducing Elle: A formally-verified EVM compiler to write more secure Ethereum code.

Elle-Core captures structured programming abstractions and enables their translation to Ethereum EVM bytecode through a verified compiler. Learn more.

Elle is a project to build a formally-verified compiler that ensures a secure link between higher-level smart contract 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.

The Problem

Ethereum — and, more generally, blockchains with Turing-complete scripting languages — are exciting technologies because they have 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 and the Parity wallet, resulting in substantial monetary losses. In Ethereum, the fact that smart contracts cannot be upgraded in general after deployment can make this especially destructive.

Additionally, it’s possible for the code to be bug-free, but the generated bytecode is still incorrect — namely if the compiler (the program that translates the program source code into bytecode for the EVM) has a bug and mistranslates 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. 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 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:

“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 used an automated “fuzzing” technique to produce test cases that revealed dozens of bugs in each platform.

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 vital part of these foundations.

The Elle Compiler

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, which is built in the proof assistant Coq 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, or just “Elle” for short when clear from context) that compiles down to the 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 builds on Eth-Isabelle, a formal specification of the EVM (both its syntax, the bytecodes of the EVM; and its semantics, a formal description of its behavior) inside of the Isabelle proof assistant (Isabelle is another widely-used system for machine-checked proofs in pure mathematics and program-correctness). On top of this EVM implementation, Elle contains a syntactic definition of the Elle-Core language along with a formal semantics for it. It contains an implementation of a translation from Elle-Core to EVM (described in detail here), as well as a correctness proof linking the semantics of Elle-Core programs to their compiled EVM counterparts (described in detail here).

Elle-Core provides users with a structured programming abstraction, freeing them from having to reason directly about addresses of program locations when describing control-flow (e.g. the jumps and conditional jumps used to implement if-statements and for-loops). With Elle’s structural abstraction, it becomes straightforward to implement conventional control structures such as if, for, unless, etcetera.

Elle Users

Elle is targeted at two main groups of users. The first group is users that are building smart contracts and are looking for a trustworthy compiler. This set of users have two options –they could write 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. Currently, this takes the form of a frontend to Elle called FourL, responsible for taking existing LLL programs and translating them into Elle-Core. After this pre-processing step, the programs can be translated to EVM with the assurance that the translation for Elle-Core to EVM is correct.

The second group that Elle is targeted for are the 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 (writing proofs in a proof assistant).

The ability to formally verify smart contracts helps protect users 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.” As with laws in the legal system, smart contracts written incorrectly can lead to unintended consequences. Since the compiler has such an integral role in “writing” these “laws,” trust in them is of great importance.

Elle and Auditors

Vast amounts of time, effort, and money are 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 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.

Elle and Contract Verification

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 (mathematical theorems stating that their code will work as expected), they will want to know that the compiler cannot compromise these guarantees. Elle can help provide them with the assurance they desire.

Currently, as a result of the untrusted nature of compilers used in the Ethereum ecosystem, most formal analysis happens at the level of EVM bytecode (tools such as Mythril and KEVM support formal analysis at this level). This approach has the advantage that analysis is being performed directly on the code that will live on the blockchain, meaning that the properties proven and bugs found apply directly to the smart contract as deployed on Ethereum. However, these analyses are unable to take advantage of higher-level abstractions that may be present in the source code that the bytecode programs were originally compiled from. Furthermore, changes to the compiler may cause different bytecode to be generated, meaning the analyses must be rerun.

Another approach to verifying Ethereum smart contracts works at the level of source code rather than bytecode. Some of the work being done on semantics for higher-level smart contract languages (such as KVyper) support this kind of reasoning. Verifying programs at this level allows for the use of all the high-level abstractions and information (such as datatypes) that are present in the source language but become obscured or lost during the translation to bytecode. However, these tools require the compiler to be trustworthy, or the facts they prove might not hold on the bytecode actually generated by the compiler (which is, of course, what will get run at the end of the day).

Elle can be seen as bridging these two approaches: enabling the convenience of source-level reasoning with the iron-clad guarantees that come with having proofs about the actual bytecode that will be stored and run on-chain.

Future Work on Elle

Work on the Elle system is ongoing. Much of the new work is on a successor to Elle called Gazelle (still at a very early stage) that aims to build a more flexible system, taking advantage of the lessons learned from building Elle.

Goals of Gazelle include the following (in approximate order of priority, although this is subject to change):

1. Adding new support for higher-level languages with larger user bases as compared with LLL, such as Vyper.
2. More thorough proofs of correctness of the frontends supporting these high-level languages.
3. Integration with the K Semantics Framework and its definition of EVM.
4. Supporting alternate instruction sets/virtual machines, such as eWASM.

In addition to these goals for the compiler itself, we want to build program logics on top of it. These are tools that leverage Elle/Gazelle’s formal semantics to enable (more) convenient reasoning for doing proofs at the source-code level. These tools would be similar to 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.

Words of Caution

Although the core of Elle has been formally verified to produce correct code, the Elle system should not (yet) be considered production-ready for the following two reasons:

1. Parts of the compiler–including the implementation of the FourL frontend that translates LLL programs into Elle’s intermediate representation–have not yet been verified.
2. The compiler has not been subjected to traditional software-auditing techniques, and only a limited number of people have dug through the compiler’s implementation in detail.

Therefore, we don’t advise using Elle to compile contracts to be deployed to mainnet, or that will manage nontrivial amounts of valuable assets. Future versions of Elle will aim to be appropriate for mission-critical, mainnet usage, but at this stage, Elle should be considered a prototype.

Call to Action

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 Elle’s documentation. You might also want to look at Mario (the author)’s research blog, as well as this academic paper (preprint) describing the Elle system in detail.

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 README here for information on how to build the FourL executable (you don’t need Isabelle to do this.) This way you can take advantage of Elle’s trustworthy compilation, without needing a detailed understanding of verification. Keep in mind the caveats listed above though — Elle isn’t yet ready for production use.

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. (Auditors): Audit (Future Versions of) Elle.

Though the Elle project does not have any resources committed to it to help pay for a commercial code audit, we believe strongly that getting more eyes on the code will help build the assurance that the compiler is appropriate for mission-critical use; in particular, that the verified parts of the compiler are correctly specified, and that the unverified parts of the compiler are free of bugs.

The current version of Elle is likely to be substantially rewritten in the future to make it more maintainable, but many of the core specifications and theorems about the correctness of the compilation are unlikely to change much. Therefore, even at this early stage, auditors or careful programmers willing to take a closer look at Elle’s implementation should get in touch! (See below). The Elle compiler will remain an open-source project, ensuring that the efforts put in by people helping to review the code will benefit the entire Ethereum community.

5. 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, Concrete Semantics is available for free as an ebook. 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.

6. 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 that use Elle to do practical verification, the easier it will be to identify pain points in its usage and ways to improve the platform.

7. 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 the Vyper language), and building higher-level reasoning tools to make it easier to do verification of smart contracts built on top of Elle.

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.

Conclusion

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 compiled smart contracts to the next level because Elle comes with a proof that the output EVM 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.

If you’re looking for Elle itself, you can find that on GitHub here.

Finally, you might want to check my research blog, where I plan to post updates about the status of the project from time to time.

This project is generously funded by ConsenSys Hub R&D, a division of ConsenSys AG.

Thanks for reading!
-Mario Alvarez

Disclaimer: The views expressed by the author above do not necessarily represent the views of Consensys AG. ConsenSys is a decentralized community with ConsenSys Media being a platform for members to freely express their diverse ideas and perspectives. To learn more about ConsenSys and Ethereum, please visit our website.