Solidity Audit Methodology
Solidity audit methodology is a review in passes that checks what a contract promises before it checks how the code works. The auditor reads the promise first, then the code, then fixes each finding and proves the fix.
The spec states what the contract promises
SpecVault promises two things. Deposits increase the balance, and withdrawals never exceed deposits.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;
contract SpecVault {
mapping(address => uint256) public balances;
function deposit() public payable {
balances[msg.sender] += msg.value;
}
function withdraw(uint256 amount) public {
require(balances[msg.sender] >= amount, "too much");
balances[msg.sender] -= amount;
(bool success, ) = payable(msg.sender).call{value: amount}("");
require(success, "send failed");
}
}
Each entry point is checked for its caller
EntryVault has three entry points. The proof checks the owner call, the stranger call, and the withdrawal of another person's funds.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;
contract EntryVault {
address public owner;
mapping(address => uint256) public balances;
constructor() {
owner = msg.sender;
}
function deposit() public payable {
balances[msg.sender] += msg.value;
}
function withdraw(uint256 amount) public {
require(balances[msg.sender] >= amount, "too much");
balances[msg.sender] -= amount;
(bool success, ) = payable(msg.sender).call{value: amount}("");
require(success, "send failed");
}
function setOwner(address newOwner) public {
require(msg.sender == owner, "not owner");
owner = newOwner;
}
}
One finding is fixed and re-proved
BuggyClaim marks the claim after it sends ether, so a reentrant call pays twice. FixedClaim marks the claim first, so the second call reverts.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;
interface IClaim {
function claim() external;
}
contract BuggyClaim {
mapping(address => bool) public claimed;
function claim() public {
require(!claimed[msg.sender], "claimed");
(bool success, ) = payable(msg.sender).call{value: 1 ether}("");
require(success, "send failed");
claimed[msg.sender] = true;
}
}
contract FixedClaim {
mapping(address => bool) public claimed;
function claim() public {
require(!claimed[msg.sender], "claimed");
claimed[msg.sender] = true;
(bool success, ) = payable(msg.sender).call{value: 1 ether}("");
require(success, "send failed");
}
}
contract Attacker {
IClaim public victim;
bool public tried;
constructor(address victimAddress) {
victim = IClaim(victimAddress);
}
function claimThrough() public {
victim.claim();
}
receive() external payable {
if (!tried) {
tried = true;
try victim.claim() {} catch {}
}
}
}
Example
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;
contract AuditedVault {
address public owner;
uint256 public feePercent;
mapping(address => uint256) public balances;
address constant FEE_TO = address(0xA11CE);
constructor() {
owner = msg.sender;
feePercent = 1;
}
function deposit() public payable {
balances[msg.sender] += msg.value;
}
function withdraw(uint256 amount) public {
require(balances[msg.sender] >= amount, "too much");
balances[msg.sender] -= amount;
uint256 fee = (amount * feePercent) / 100;
uint256 net = amount - fee;
(bool okNet, ) = payable(msg.sender).call{value: net}("");
require(okNet, "net send failed");
(bool okFee, ) = payable(FEE_TO).call{value: fee}("");
require(okFee, "fee send failed");
}
function setFee(uint256 newFee) public {
require(msg.sender == owner, "not owner");
require(newFee <= 10, "fee too high");
feePercent = newFee;
}
}
Key points
- Spec first: The spec is the plain promise of what the contract must do.
- Invariants: An invariant is a rule that must stay true after every action.
- Entry points: An entry point is a public function an outsider can call.
- Arithmetic: Every calculation is checked for overflow, underflow, and rounding.
- Access control: Every powerful function is checked for who may call it.
In this example, AuditedVault holds a fee percent, a balance mapping, and an owner. deposit adds to the caller's balance. withdraw checks the balance, subtracts the full amount, then sends the net amount to the caller and the fee to the fee address. setFee is owner only and rejects any fee above ten percent.
Note
A checklist guides the review, but only tests and fixes prove a finding is gone.
Try it Yourself
Edit the code, then press Run.
Running is simulated · Remix IDE
Exercise
An audit finds that a claim function marks a claim after sending ether, so a reentrant call pays twice. What is the correct fix?