Runtime Verification January 2024 Updates

Welcome to the first newsletter of the year. This time around, we bring a combination of updates from last December and the month of January. If you want to be up to date with what we are up to, follow us on X or join our Discord to get in touch with our team and ask them all your questions about our work and tooling.

AUDITS

Our team has been working on some long-term engagements with clients during the past two months, including our latest report and blog post on MultiversX’s Multi Asynchronous Calls audit. In the upcoming weeks, we will announce newly completed audits and engagements on our X account, and they will be added to the next newsletter issue.

KONTROL

These are the monthly updates from our team working on Kontrol:

• Implemented `kontrol summary` — a new feature that allows to generate a summary for a Solidity function based on the list of account accesses that is generated by Foundry. This feature is particularly useful in projects with complicated and lengthy deployment — in this case, the execution of `setUp()` can be summarized via `kontrol summary`; then, the generated JSON file containing the summary of a deployment process can be used to initialize the initial node of the KCFG, i.e., the state of the contract at the start of verification, possibly saving tens of minutes of execution time (PRs: https://github.com/runtimeverification/kontrol/pull/271, https://github.com/runtimeverification/kontrol/pull/221).
• Added `no-gas` execution mode in `kontrol prove`, which is now the default behavior. With this change, Kontrol does not compute or reason about gas costs, which speeds up the execution. Gas computation can be turned on via the ` — use-gas` option now available in `kontrol prove` (PR: https://github.com/runtimeverification/kontrol/pull/252).
• Enabled Foundry test-like verification for tests starting with `check`,` prove`, `checkFail`, and `checkProve` prefixes, in addition to previously supported `test` and `testFail`. Such tests are being checked for failures caused, e.g., by failed `assert` and `require` statements, compiler-inserted overflow checks, and so on. This update allows specification of Kontrol-specific tests that would not be picked up for fuzzing during a `forge test` run, and provides compatibility with other symbolic testing tools such as halmos and hevm. Functions that do not start with one of these prefixes will be symbolically executed by `kontrol prove`, but any such failures will not be reported (PR: https://github.com/runtimeverification/kontrol/pull/249).
• Turned on ` — no-break-on-calls`, ` — fail-fast`, and ` — counterexample-generation` options in `kontrol prove` to improve the default performance and UX of the tool. As a result of this change, by default, Kontrol will not save a new node in KCFG every time an EVM call is performed, it will stop the execution on other branches if a failure has been identified in one of them, and will output the counterexample(s) for the failing test. These options can be turned off via ` — break-on-calls`, ` — no-fail-fast`, and ` — no-counterexample-generation`, respectively. (PR: https://github.com/runtimeverification/evm-semantics/pull/2258)
• Added ` — break-on-basic-blocks`, ` — break-on-storage`, and ` — break-on-cheatcodes` options to `kontrol prove`, instructing it to add a new node for every basic block, `SSTORE/SLOAD` operation, and Foundry rules and KEVM, thereby generating a more detailed KCFG and making it is easier to explore and investigate (PRs: https://github.com/runtimeverification/kontrol/pull/261, https://github.com/runtimeverification/evm-semantics/pull/2246, https://github.com/runtimeverification/evm-semantics/pull/2242).
• Enabled generation of KEVM claims from Kontrol-produced KCFG to facilitate debugging and profiling of proofs and claims. Option ` — to-kevm-claims` to “kontrol show …` now produces a module containing KEVM claims for each basic block. Option ` — kevm-claim-dir` … allows specifying a directory to generate these claims in. (PR: https://github.com/runtimeverification/kontrol/pull/262).
• Added support for `struct` variables in analyzed test function parameters to make it even easier to verify tests from an existing Foundry test suite (PR: https://github.com/runtimeverification/kontrol/pull/78)
• Modified internal K representation of analyzed contracts in include an absolute path in the name of the contract, making it possible to disambiguate (and, therefore, execute correctly) same-name contracts within one project (PR: https://github.com/runtimeverification/kontrol/pull/219).
• Included useful lemmas on boolean reasoning, set reasoning and map lookup to KEVM, facilitating and streamlining the analysis of EVM smart contracts (PRs: https://github.com/runtimeverification/evm-semantics/pull/2037, https://github.com/runtimeverification/evm-semantics/pull/2251).

RESEARCH

This month, we also bring an exciting update from our research team:

• Our paper, “A Logical Treatment of Finite Automata”, was accepted for the TACAS 2024 conference. In this paper, we show that by capturing finite automata as matching logic formulae, we may also capture algorithms that manipulate them. In fact, we are able to produce complete Hilbert-style proofs for equivalence between regular expressions using this technique. This is a first step towards formally proving similar manipulations over a program control flow graph, and other transition systems.

ERCx

And, before wrapping up this month’s newsletter, here are the ERCx updates:

• Added support for some Layer 2 networks such as Optimism (Mainnet and Sepolia), Arbitrum (Mainnet, Nova and Sepolia), Polygon (Mainnet and Mumbai), Binance Chain (Mainnet and Testnet), Linea (Mainnet), and Base (Mainnet and Sepolia).
• We released the first version of our test suite for ERC-721 tokens, aka NFTs.
• Cranked out the final version of our ICST 2024 paper on Leveraging Mutation Testing to Improve and Minimize Test Suites for Smart Contracts. This is a collaborative work with Certora Inc.
• Following the kind feedback from the auditors we met, we merged test levels Minimal and Recommended into Conformance. Conformance tests comprise all properties extracted from the standard.
• We brought several improvements to our backend.

That’s all for this month’s updates. Join us on X and Discord to never miss any updates from us.