ChainSecurity Ltd performed a security audit of the Polkadot Claims smart contract. To ensure that the Claims contract is secure and functionally correct, ChainSecurity Ltd formally verified the contract’s code with respect to 12 important functional requirements. To find out more about the scope of the audit and the verified requirements, read our detailed audit report.
Summary
The Web3 Foundation engaged ChainSecurity Ltd to perform a security audit of Polkadot Claims, an Ethereum-based smart contract that will allow holders of the DOT allocation indicator token to claim their balances of DOTs to a Polkadot public key ahead of Polkadot’s genesis.
The state of the Claims contract will be used to initialize the genesis of Polkadot, including the Polkadot public key to associate to a specific allocation, the index of the public key, and the vesting status of the allocation. Due to the importance of this data, the security of the Claims contract was considered of utmost importance. To address this, ChainSecurity Ltd was tasked to formally verify the correctness of the contract’s code, especially with respect to critical requirements, such as ensuring immutability of the state of the contract after claims have taken place.
To guarantee that the Claims contract is secure and functionally correct, ChainSecurity Ltd formally verified the contract’s code. In more detail, the security audit consisted of:
1) Formalizing 12 critical functional requirements pertaining to the immutability of the state after the initialization, access-control requirements, and the safety of the contract set-up period;
2) Formally verifying the correctness of the Claims contract with respect to the formalized properties. Verification was carried out using VerX, ChainSecurity Ltd’s state-of-the-art verifier for smart contracts;
3) Analyzing the Claims contract for generic security vulnerabilities using Securify, ChainSecurity Ltd’s state-of-the-art security scanner;
4) A thorough manual audit of the Claims contract for compliance with best security practices.
During the audit, ChainSecurity Ltd found 0 critical, 0 high, 2 medium and 9 low severity issues. All reported issues have been addressed or acknowledged by the Web3 Foundation. In particular, all security and design issues have been resolved with appropriate code fixes. The audit report describes the fixes that were applied to each issue and the reasoning of the Web3 Foundation behind them.