Formal Verification— A Journey Deep into the Gnosis Safe Smart Contracts
Don’t worry we’ll get you there Safe and sound
At Gnosis, we take security seriously. While we ensure our code is always audited, with our Gnosis Safe wallet, we’ve gone one step further and formally verified our smart contracts.
A Brief History
Back in 2016, we developed a multisig-contract in preparation for Gnosis’ token sale that fulfilled our need to securely manage large amounts of tokens and ether. This multisignature wallet emerged as the de-facto standard for teams managing shared funds.
A year after that, we released a fully refactored version of the wallet contract with a host of improvements including higher gas efficiency, upgradability, token-gas payment options, and meta transactions. After careful internal review of the contract, we commissioned Ethereum researcher Alexy Akhunov to perform a full audit.
However, at this time the Gnosis Multisig contract held well over $3 billion in ether and tokens — with stakes this high, we did not want to “release” the contract until we were sure that it provided the highest level of security.
One Step Further
Shortly after the audit was performed, we decided that we would take our commitment to security one step further and formally verify the Gnosis Safe smart contracts. Our team worked closely with Runtime Verification (RV) — a company that specializes in using runtime verification techniques to ensure that software systems are secure — to release a formal verification report. While testing and auditing are essential steps in the development process, formal verification is a mathematical proof-based methodology used to significantly decrease the likelihood that a smart contract is buggy.
Despite its utility, formal verification is often overlooked in the smart contract development process, for reasons of prohibitive cost and time delays. But, by the end of this post you’ll understand why formal verification is important for critical ecosystem infrastructure.
If the term formal verification seems a little confusing, don’t fear! Let’s take a journey deep into the world of formal verification and your confusion will be transformed into clarity.
Why Formal Verification and How Does it Work?
First, the basics. A smart contract must be compiled into bytecodes before it can be deployed on the blockchain. Then the Ethereum Virtual Machine (EVM) validates the transaction and instructs the contract to execute.
But what happens if there is a mistake in the codebase or an opportunity for an attacker to create a malicious contract? There have been quite a few notable smart contract hacks which serve as prime examples of what happens when smart contract security is overlooked.
The rise of decentralized technology has taught us that with great potential comes great responsibility. Smart contracts allow devs to do a lot of cool things on the blockchain (e.g. the DAO), but implementing the code is difficult and even a tiny vulnerability can have devastating consequences (e.g. the DAO).
To us, there is a way to decrease the probability of bugs in your code and build confidence in your decentralized applications. Check, double-check and formally verify your code!
Here’s what this process looks like.
The first step to formally verifying a smart contract is to devise a set of conditions or specifications that must be met for the smart contract to be successfully executed. These conditions encompass what are otherwise known as formal specifications.
Once these formal specifications are identified, they are converted into a programming language called K. This framework analyzes the functions of your program and verifies that each function works as intended.
This process is iterative and continues until all possible behaviors of the function in any execution environment meet the formal specification. Any issues discovered are reported back to the development team, resolved in the contract, and then verified again.
Why Formal Verification Matters
Even though blockchain is still in its nascence, smart contract security has improved dramatically; nonetheless, it is vital that we as a community go the extra mile (or kilometer) to ensure that our code is secure.
Of course, auditing and extensive testing are essential steps to take before a dapp is deployed. But, smart contracts are notoriously complex, and these methods miss critical vulnerabilities because they often don’t account for all of the possible behaviors of a program. Formal verification is the added step that every smart contract developer should consider before deploying an application onto the blockchain because it is a wicked accurate way to mathematically prove that a contract works the way it was intended to.
Although it isn’t cheap, formal verification is an investment in blockchain technology because building confidence in our platforms and protocols is key to adoption and critical to protecting the assets of our users.
The Gnosis Safe’s Formally Verified Contracts
The goal of our work with RV was to audit the code of the Gnosis Safe smart contract and to formally verify security-critical properties. The properties were identified by the Gnosis team and formalized by RV using the K-Framework discussed above.
The formal verification process led to several findings in the Safe’s smart contracts, including reentrancy and transaction reordering vulnerabilities, as well as usability issues that clients of the contract should be aware of. However, the vulnerabilities identified were exploitable in rather limited circumstances, and we have since released a new version of our smart contracts (v1.0.0) that addresses each critical issue identified by the RV team. For a full list of findings, please read the full report.
In short, we believe that the Gnosis Safe smart contracts will be the basis of wallet infrastructure in the future. Our team and others in the space will continue building on these contracts because they provide a best in class security experience for users.
Please make sure to update to the newest version of the multisig if you haven’t already, and stay tuned for news on our soon to be released Team Safe!
Please note: Smart contract development is a new technology. There is always the possibility of human error when writing, auditing and formally verifying smart contracts. Gnosis has gone the extra mile to ensure that there are no bugs in the Gnosis Safe smart contracts with formal verification. However, there remains a risk of vulnerabilities in code, which we cannot fully rule out. Use of the Gnosis Safe is at your own risk.
Thanks to: Eric Gorski, Kei Kreutler, Martin Köppelmann, Tobi Schubotz, Lukas Schor, Daejun Park, Grigore Rosu, and Patrick MacKay
