What is an example of a runtime verification tool being used to audit a smart contract?

Quoted from Forex.com.bd-Editorial External answer — Ethereum Stack Exchange Author: Chadi Sebbar Source score (net votes, not local likes): 0 Original post: https://ethereum.stackexchange.com/a/172433 License: CC BY-SA 4.0 — https://creativecommons.org/licenses/by-sa/4.0/ Adaptation: HTML converted to plain text; contact email addresses removed. "Runtime verification" here means: state a property the system must always satisfy, then check it against the running system as it executes, rather than against the source code beforehand. (Not to be confused with Runtime Verification Inc., the firm behind the K framework. The question uses the general sense.) For a smart contract there are two places to put that check. Here is a minimal example of each, on the same property. The property A minimal vault that holds one ERC-20 and records what it owes: contract Vault { IERC20 public immutable token; mapping(address => uint256) public balanceOf; uint256 public totalDeposits; // deposit(), withdraw() ... } The property: the vault always holds at least what it owes. token.balanceOf(address(vault)) >= vault.totalDeposits() Option 1: check it inside the contract, on every call modifier checksSolvency() { _; require(token.balanceOf(address(this)) >= totalDeposits, "invariant: insolvent"); } function withdraw(uint256 amount) external checksSolvency { balanceOf[msg.sender] -= amount; totalDeposits -= amount; token.transfer(msg.sender, amount); } This is runtime verification in the strict sense: the property is evaluated on every execution, and a violating transaction reverts, so the bad state never lands on-chain. The costs are gas on every call, and coverage only of the functions you remembered to decorate. Option 2: check it outside the contract, on every block // monitor.mjs (Node 18+, npm i viem) import { createPublicClient, http, parseAbi } from "viem"; import { mainnet } from "viem/chains"; const client = createPublicClient({ chain: mainnet, transport: http(process.env.RPC_URL) }); const VAULT = "0x..."; const TOKEN = "0x..."; const vaultAbi = parseAbi(["function totalDeposits() view returns (uint256)"]); const erc20Abi = parseAbi(["function balanceOf(address) view returns (uint256)"]); client.watchBlockNumber({ onBlockNumber: async (blockNumber) => { const [held, owed] = await Promise.all([ client.readContract({ address: TOKEN, abi: erc20Abi, functionName: "balanceOf", args: [VAULT], blockNumber }), client.readContract({ address: VAULT, abi: vaultAbi, functionName: "totalDeposits", blockNumber }), ]); if (held < owed) console.error(`block ${blockNumber}: insolvent, holds ${held}, owes ${owed}`); }, }); This costs nothing on-chain, and it can see things the contract cannot: the token starting to charge a transfer fee, the price your oracle returns, an admin upgrading the implementation or granting a role. What it cannot do is stop the transaction; it tells you one block later. In practice you pair it with something that can act, such as a pause role the team holds. Why this is different from an audit, and where it earns its keep An audit (and static analysis, and formal verification of the source) reasons about one version of the code, under the assumptions that were true when it was reviewed. A runtime check reasons about what is actually deployed, today, with today's dependencies. That difference matters because many losses come from something that did not exist at review time. A concrete case: the read-only reentrancy in Curve's get_virtual_price was disclosed privately in April 2022 and published with full detail on 11 October 2022 ( ChainSecurity post-mortem ). In February 2023 dForce listed a new market on Arbitrum priced from that function, and it was drained less than three days after it was created ( the exploit transaction ). No audit could have covered a contract that did not exist yet. A watch on the protocol's own admin and deployer addresses would have flagged "a new market, priced by a view function on a contract you do not control" on the day it went live, and the fix ChainSecurity describes (trigger the pool's reentrancy lock before reading the price) is itself a runtime check inside the contract. One practical tip Write the property once and use it in both places: as a Foundry invariant test before deployment, and as the monitor's check after. Then what you verified before launch and what you watch after launch are literally the same statement, and a code change that breaks it fails in CI before it reaches the chain. Disclosure: I work at Fidesium, which does smart contract audits and post-deployment monitoring. We wrote up the dForce timeline block by block, with which kind of watch would have fired at which moment: How continuous monitoring catches what a point-in-time audit misses

Cancel quote