Runtime Verification: In Solidity Specification, Property Testing, and Verification

Runtime Verification

Runtime Verification (https://runtimeverification.com) is a software quality assurance firm focused on providing tools and processes which improve client software and software development practices.

Introduction

Compound has suffered from numerous low-level functional correctness errors in the past, some which have made it past several reputable oversight and quality assurance firms. At least some of these issues could have been caught with simple property tests. For example:

  • An upgrade to price feeds for cETH led to cETH markets being frozen (cETH Price Feed Incident: Post-Mortem) when the new contracts did not expose the expected functionality for retrieving price data.
  • In another incident, a prior coding error led to an old bug suddenly becoming a problem on migration: https://twitter.com/Mudit__Gupta/status/1443454935639609345. This is the perfect scenario for property tests that can be run on CI, as the test may have passed before the upgrade, but at upgrade time but before deployment the developers would have been notified that the test had started to fail.

Our proposal is to introduce property testing (using Foundry: GitHub - foundry-rs/foundry: Foundry is a blazing fast, portable and modular toolkit for Ethereum application development written in Rust.) to Compound’s quality-assurance toolbox. We’ll focus on delivering immediate value by doing a system architecture review, followed by developing targeted property tests that can be run on Compound’s CI now and into the future to guard against upgrade failures. Once a quality property test suite is developed, it continues to deliver value by safeguarding against breaking changes without expensive maintenance or heavy compute costs.

Longer-term value is also offered, via symbolic execution of these property tests, which effectively turns the properties into formal specifications and their symbolic testing into formal verification (see Hoare Triples as Property Tests below for details). There are now several open source tools which support formal verification of Foundry-style property tests, including:

This gives Compound the flexibility to choose how to pursue formal verification of their property tests, should that higher level of assurance be voted for.

Runtime Verification is uniquely positioned to deliver on these goals, with our extensive experience in both auditing (GitHub - runtimeverification/publications: Publications of Runtime Verification, Inc.) and our involvement in writing Foundry property test suites for clients, for example:

Runtime Verification has a long history of promoting the “shift-left” mindset to security. We work closely with our clients to teach them our methods so they can improve their contract quality and security independent of contracting external firms.

The proposal is broken into four phases, each to be individually approved by DAO vote. Only upon completion of prior phases will later phases go to DAO votes (approved in execution order, with option to terminate). All payments accepted in whatever mix of COMP and USDC the DAO prefers.

Any and all feedback on scope, timeline, cost, and collaboration welcome!

Scope:

Compound Comet: GitHub - compound-finance/comet: An efficient money market protocol for Ethereum and compatible chains (aka Compound III, Compound v3).

We are open to other scopes as proposed by the Compound community. If there is a better target, please inform!

Looking at this repository, estimates below are based on this output from cloc tool:

Language files blank comment code
Solidity 84 1209 2749 4115
JSON 3 0 0 740
Markdown 1 6 0 12
SUM: 88 1215 2749 4867

Phase 1: Design Modeling and Property Tests

Design modeling is the first phase of any audit engagement that Runtime Verification pursues (see the anatomy of an RV audit in this 10 minute talk: Secureum TrustX — Layer-2 Room, 21 April - YouTube). In this phase, we review the business logic and system architecture of the financial application. We cross reference the existing documentation on the protocol during the process, to identify any inconsistencies between the intended behavior and the documented behavior, augmenting it where needed with updated or new documentation. In our experience, many of the major errors and issues are found in this stage.

Following design modeling, we will develop an extensive and complete (as possible) property test-suite using the Foundry property testing tool for all external behavior of Compound Core. This test-suite will be informed by the design model, with the intention of catching deviations in the source-code from the intended system design. We will provide documentation to the Compound team on how to run the test-suite, and assist in setting up CI if requested.

  • Timeframe: 13 weeks, 2 engineers
  • Cost: USD 325000.
  • Deliverables:
    • Design modeling report, with our system description and any issues we find in the overall system documented. See the “Contract Description and Invariants” section of this document for an example: https://raw.githubusercontent.com/runtimeverification/publications/main/reports/smart-contracts/Blockswap_Stakehouse.pdf.
    • Foundry property test-suite which covers the scope of the design model produced in Phase 1. Documentation on how to run this test-suite, and assistance integrating into Compound CI process upon request. The test suite will be focused on both (i) functional correctness of individual operations, and (ii) high-level invariant statements.

Phase 2: Property Verification

Runtime Verification offers Foundry property test verification, which increases the level of assurance that you get from Foundry property test suites dramatically. Instead of randomly testing individual inputs (default Foundry behavior), we use symbolic execution to explore all possible paths of execution. With a well-tuned test-suite, and the correct lemmas in place, you can claim full formal verification here! Runtime Verification will develop the lemmas needed, and integrate them into the Compound repository, as well as the documentation needed for the Compound community to use and extend those verification conditions. As preferred by Compound team, we can also try other open-source verification tools on the property test-suite (eg. HEVM and Halmos), but most other tools don’t have complete support for the set of cheat-codes that KEVM supports yet. This phase will be timeboxed.

  • Timeframe: 8 weeks, 2 engineers
  • Cost: USD 200000.
  • Deliverables: K lemmas committed to Compound repository which enables automatically verifying the relevant property tests in the time allotted. Documentation for the Compound team which they can use to expand on this work, adding their own lemmas, and integrating into their CI if desired.

Phase 3: Education

Runtime Verification will work with the Compound team to educate them on how to extend the property test-suite, and how to maintain the proofs developed in Phase 2. This will include training in how to use the open source K Framework, how to effectively write new property tests, and how to write lemmas for the property test-suite when proofs are failing.

  • Timeframe: 8 weeks, 1 engineer
  • Cost: USD 100000
  • Deliverables:
    • 4 workshops (4 hours each) targeted at the Compound devs, focusing on teaching how the verification infrastructure works and how to extend the properties/verification goals.
    • 8 weeks of full-time support from one of our verification engineers.

Phase 4: KaaS Integration

Runtime Verification offers KaaS (K as a Service), which exposes a faster more powerful symbolic execution engine and better proof search tactics. Runtime Verification will make KaaS available to the Compound team for 12 months, following the completion of Phase 3. This will ease the CI burden on the Compound team (running K proofs on CI is quite intensive), as well as giving access to the better user interfaces and proof search tactics available via KaaS.

  • Timeframe: 12 months
  • Cost: USD 200000.
  • Deliverables:
    • Access for Compound team to KaaS system (fixed-size compute).
    • 8 engineer-weeks of support in using the KaaS system and maintaining the proofs.

Appendix

Hoare Triples as Property Tests

It is folklore in the software engineering and programming language community that Hoare logic triples:

forall vars . {precondition} code {postcondition}

where vars are the free variables of the Hoare triple (the core of most software verification) can be expressed as parametric property tests of the form:

function prop(vars) {
  assume precondition;
  code;
  assert postcondition
}

Passing the property test prop(vars) by executing it symbolically with vars as symbolic inputs is equivalent to formal verification of the Hoare triple.

2 Likes