I always do a mental audit at the end of the week to make sure I’m balancing time between my career and my personal life.
One of the core services we offer at Extropy.io is contract auditing. That is, we will take your smart contract application code and conduct a full security audit to ensure that it is free from security vulnerabilities.
In this post we will describe the process that we go through in our audits, including a checklist of some of the vulnerabilities that we look for. We’ll also offer some recommended advice for preparing your codebase for an audit.
We audit your code according to the following criteria.
There’s a lot that can be said of each of the above, but in the following we’ll just focus on security and code correctness. In particular, we’ll outline the contract security vulnerabilities we look for and the approach we take for verifying code correctness.
Of the above goals, one of the most important will likely be security. The SWC (Smart Contract Weakness Classification) registry is a very handy resource of known vulnerabilities
The Smart Contract Weakness Classification Registry is an implementation of the weakness classification scheme proposed in EIP-1470. It is loosely aligned to the terminologies and structure used in the Common Weakness Enumeration (CWE) while overlaying a wide range of weakness variants that are specific to smart contracts.
The following is a checklist of contract weaknesses / vulnerabilities that we look for in audits:
|SWC-132||Unexpected Ether balance||CWE-667 Improper Locking|
|SWC-131||Presence of unused variables||CWE-1164 Irrelevant Code|
|SWC-128||DoS With Block Gas Limit||CWE-400 Uncontrolled Resource Consumption|
|SWC-122||Lack of Proper Signature Verification||CWE-345 Insufficient Verification of Data Authenticity|
|SWC-120||Weak Sources of Randomness from Chain Attributes||CWE-330 Use of Insufficiently Random Values|
|SWC-119||Shadowing State Variables||CWE-710 Improper Adherence to Coding Standards|
|SWC-118||Incorrect Constructor Name||CWE-665 Improper Initialization|
|SWC-116||Timestamp Dependence||CWE-829 Inclusion of Functionality from Untrusted Control Sphere|
|SWC-115||Authorization through tx.origin||CWE-477 Use of Obsolete Function|
|SWC-114||Transaction Order Dependence||CWE-362 Concurrent Execution using Shared Resource with Improper Synchronization (‘Race Condition’)|
|SWC-113||DoS with Failed Call||CWE-703 Improper Check or Handling of Exceptional Conditions|
|SWC-112||Delegatecall to Untrusted Callee||CWE-829 Inclusion of Functionality from Untrusted Control Sphere|
|SWC-111||Use of Deprecated Solidity Functions||CWE-477 Use of Obsolete Function|
|SWC-108||State Variable Default Visibility||CWE-710 Improper Adherence to Coding Standards|
|SWC-107||Reentrancy||CWE-841 Improper Enforcement of Behavioral Workflow|
|SWC-106||Unprotected SELFDESTRUCT Instruction||CWE-284 Improper Access Control|
|SWC-104||Unchecked Call Return Value||CWE-252 Unchecked Return Value|
|SWC-103||Floating Pragma||CWE-664 Improper Control of a Resource Through its Lifetime|
|SWC-102||Outdated Compiler Version||CWE-937 Using Components with Known Vulnerabilities|
|SWC-101||Integer Overflow and Underflow||CWE-682 Incorrect Calculation|
Another vital goal of an audit is to determine correctness of the code i.e. does it do what it’s intended to do? Clearly this has a lot to do with another of our audit goals above: testing. Indeed, we encourage the inclusion of a test suite as part of the application code to be audited! It gives us a good sense of (at least) the following:
Recently we started using formal verification tools to help with our audits. With these tools, we can construct proofs of formal program specifications - a level of assurance that goes well beyond conventional means of testing. One particular formal verification tool we have been using is KLab. This provides very useful tooling for verifying correctness and debugging of contracts.
KLab builds upon KEVM (also called Jello Paper) - a formal specification of the Ethereum Virtual Machine expressed in the language of the K Framework. KLab includes a specification language
act for expressing contract properties without the need for a deep knowledge of KEVM nor K.
To help with verifying token contracts, we have been implementing
act specifications of the ERC20-K standard (the same ERC20 of EIP-20 but formally specified in K). See our ERC20-act GitLab repo for more details.
For auditing ERC20 tokens, we have developed a specification ERC20-act for formally verifying contracts against the ERC20 standard (see the box above). This allows us to check the most basic properties of a standard token contract.
Of course, to properly verify a contract in its entirety (whether a token or not) will depend on the particular nuances of the contract. As such, this will vary on a case by case basis. If you are interested in adding formal verification to your codebase, we can assist with that as an additional service to the audit.
If you decide to audit your contract with Extropy, we recommend some steps to ensure the audit goes smoothly. This checklist is a great read, and our advice is generally similar: