Formal Verification of the Gnosis Safe Contracts
An Update to the Mainnet Release
This week, we released the Mainnet version of the Gnosis Safe for Android, and we received quite a lot of feedback and questions. One of the most important questions that we’d like to address here relates to security:
How does Gnosis ensure that there are no bugs in the deployed contracts, considering the issues with the Parity multi-sig wallet earlier in 2018?
At Gnosis, we only consider a version production-ready if we have done an external audit or a formal verification of the smart contract code. For this Safe Mainnet release, we have taken the following security measures:
An external audit was performed on version 0.0.1 of the Safe contracts and the formal verification for the current version (0.1.0) is in progress. The biggest changes that have been made between versions 0.0.1 and 0.1.0 are the following:
- Used EIP-712 to generate the signatures for signed messages
- Added support for EIP-1271 signatures
- Upgrade to Solidity 0.5.0
Unfortunately, the upgrade to Solidity 0.5.0 delayed the formal verification of the Safe’s current version (0.1.0), but the first results can already be seen. You can follow progress at: https://github.com/runtimeverification/verified-smart-contracts/tree/master/gnosis.
Due to the ongoing formal verification, we decided to not mark the contracts as a 1.x version, but as a 0.1.x version. This is not properly reflected in the store entries of the mobile app and browser extension. For this reason, we decided to make this more explicit in the title of the Play Store entries by changing the app’s name to “Gnosis Safe — Mainnet Beta.” We have also added more details on the formal verification progress to the Play Store app description.
We want to gather early feedback from everyone and encourage the usage of the Safe. Going forward, we will provide detailed documentation on the release process and share it with everyone. Part of this process will include that the smart contracts will be published and verified on Mainnet before they will be available through mobile app stores. Additionally, an audit or formal verification will be performed for every update to the contracts.
