Our Smart Contract Auditing Process

“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.” — Jill Wagner

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.

Audit goals

We audit your code according to the following criteria.

• Sound Architecture. That is, assessments of the overall architecture and design choices, based on our understanding of your code.
• Best Practices. We evaluate whether the codebase follows the current established best practices for smart contract development.
• Code Correctness. The audit includes an evaluation of whether the code does what it is intended to do according to the documentation supplied.
• Code Quality. We evaluate whether the code has been written in a way that optimises readability and maintainability.
• Security. We look for any exploitable security vulnerabilities, or other potential threats to the stakeholders of the application.
• Testing and Testability. We examine both how easily testable the code is, and how thoroughly tested it actually is.

Security checklist

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
• SWC-131: Presence of unused variables
• SWC-128: DoS With Block Gas Limit
• SWC-122: Lack of Proper Signature Verification
• SWC-120: Weak Sources of Randomness from Chain Attributes
• SWC-119: Shadowing State Variables
• SWC-118: Incorrect Constructor Name
• SWC-116: Timestamp Dependence
• SWC-115: Authorization through tx.origin
• SWC-114: Transaction Order Dependence
• SWC-113: DoS with Failed Call
• SWC-112: Delegatecall to Untrusted Callee
• SWC-111: Use of Deprecated Solidity Functions
• SWC-108: State Variable Default Visibility
• SWC-107: Reentrancy
• SWC-106: Unprotected SELFDESTRUCT Instruction
• SWC-104: Unchecked Call Return Value
• SWC-103: Floating Pragma
• SWC-102: Outdated Compiler Version
• SWC-101: Integer Overflow and Underflow

Checking correctness

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:

• The correctness of the code
• The testability of the code
• The developer’s intent

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.

Preparing for audit

If you decide to audit your contract with Extropy.io, we recommend some steps to ensure the audit goes smoothly. This checklist is a great read, and our advice is generally similar:

• Write clean code with a consistent code style
• Use standard libraries where possible
• Include a test suite (ideally 100% code coverage)
• Document the functions of your public API (at least)
• Document your protocol and release process
• If creating a token, document the creation and distribution process
• Include end-user documentation where relevant