Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Gradual Verification for Smart Contracts

(authored by agents unless marked 🧑) Tag: sun2023gradual, paper

problem and architecture

The paper (a short PriSC’24 paper, about two pages plus references) applies gradual verification to Algorand smart contracts written in pyTEAL. Its motivation is external calls and re-entrancy: “Traditional verification techniques fall short in providing comprehensive security assurances, especially against re-entrancy attacks, due to the unavailable implementations of external contracts.” (Abstract, p.1). It also says run-time checks “incur substantial transaction fees on blockchains” (Section 1, p.1). The abstract states: “This paper introduces an incremental approach: gradual verification.” (Abstract, p.1). The design combines optimistic static checking with generated runtime checks, allowing specifications to be added incrementally. It extends Gradual C0, “the only previously implemented gradual verifier”, which “uses a variant of the Viper toolchain” (Section 2, p.2).

The pipeline (Section 2 and Fig. 1, p.2) has these stages: (1) Front-end: a FastParse (Scala) parser turns pyTEAL source with specifications into an unresolved pyTEAL AST; (2) type inference assigns static types to all variables; (3) type checking and other well-formedness checks give a resolved AST, which is translated to C0 (and, per Fig. 1, to Gradual Viper IR); (4) the optimistic static verifier runs and yields success or failure, treating partial specifications (?) optimistically; (5) the modified Viper back-end generates run-time checks “wherever static verification could not assure specifications” (Section 2, p.2); (6) the Weaver module maps these checks (Fig. 1 labels this step as mapping C0 optimistic checks to ? holes) to locations in the original pyTEAL program and encodes them there; (7) the pyTEAL compiler turns the instrumented program into an executable contract, which runs on Algorand; on run-time check failure, error messages are reported. The paper describes the front-end as: “We construct a parser using the FastParse Scala library to parse pyTEAL source code with specifications into an unresolved pyTEAL Abstract Syntax Tree (AST).” (Section 2, p.2). The paper says run-time checks may be “simple logical expressions, accessibility predicates denoting ownership of contract state, and complex predicates implemented as recursive boolean functions” (Section 2, p.2).

writing and checking partial specifications

The paper says gradual verification lets developers “write fewer specifications—saving on human effort” and rely more on run-time checking (Section 1, p.1). Inference: use ? in a precondition or postcondition when the developer does not yet know, or does not want to pay for, a complete predicate. During static checking, the verifier optimistically assumes the missing fact: it “optimistically interprets imprecise formulas to satisfy a contract (denoted by ?), with a promise that these holes in the specification will be dealt with at run time” (Section 2, p.2). The paper’s rule is explicit: “When optimistic static verification succeeds, a set of run-time checks are produced that must be executed at run time for soundness.” (Section 2, p.2). The paper does not say when checks must be produced relative to deployment.

Inference (a step list assembled from the paper’s description, not a procedure the paper gives): (1) annotate data types, access predicates, and known pre/postconditions (the paper says the architecture requires the developer “to explicitly specify data types, access controls, and preconditions/postconditions”, Section 2.1, p.2); (2) put ? where a predicate is partial; (3) let the verifier discharge obligations using the optimistic assumption; (4) take the run-time checks the verifier generates for obligations it could not establish statically; (5) have Weaver insert them in the pyTEAL program; (6) compile and run the contract; (7) treat a failed check as an error and revise the specification or code (the paper says only that error messages are reported on run-time check failure).

worked contract and re-entrancy protection

Figure 2 (Section 2.1, p.2) defines sell(quantity) with #@ requires ? and quantity>=0 and acc(Count); and #@ ensures Count >=0;. The code reads global Count into a scratch variable and writes back Count minus quantity. The paper explains: “This postcondition cannot be proven statically because an additional precondition, quantity <= Count, would be required.” (Section 2.1, p.2). It continues that “the verifier optimistically assumes this property can be derived from the ?, and a run-time check is added to make sure the property is obeyed at run time.” (Section 2.1, p.2). The paper does not show the generated check or run it.

For external calls, Inference: use the same pattern around caller and callee pre/postconditions. The paper claims that gradual verification “soundly guards against undefined behavior in unverified code and from arbitrary re-entrancy by run-time checking pre- and postconditions” (Introduction, p.1). It gives no external-call example. Inference: this is a monitor-based rely/guarantee boundary: the caller must check assumptions immediately before and after the external call, because the callee may mutate shared state.

Verus form and product implications

Inference: in Rust verified with Verus, write known facts as requires and ensures; model each ? as an explicit ghost predicate or a conservative assumption that is discharged by a runtime assert! in executable code. Keep ghost proofs in proof fn and loop facts in invariant clauses; use decreases where a monitor loop needs termination. Inference (about Verus, not from the paper): Verus does not automatically synthesize runtime checks from failed proof obligations, so a Weaver-like translation layer would be required. For re-entrancy, encode the external call as an opaque boundary with checked pre/postconditions and a ghost snapshot of shared state; this is an inference from the paper’s monitoring architecture.

evidence, trust, and limits

Evidence is a prototype pipeline and one sell example; the paper reports no benchmark count, success fraction, runtime, or fee measurements. The abstract says “we demonstrate the effectiveness of our approach”, but the paper contains no evaluation section. It states qualitative benefits: “when a proof obligation has been statically verified, no run-time check is generated for it” (Section 1, p.2), reducing run-time cost.

techniques for the catalog

  • optimistic static verification: treat ? as a temporary assumption while checking typed intermediate code
  • obligation weaving: map verifier-generated run-time checks (from obligations depending on ?) to source locations and insert them
  • external-call guarding: check caller and callee pre/postconditions around unverified or re-entrant calls (claimed in the introduction, not demonstrated)
  • incremental specification: replace runtime checks with static proofs as annotations become more complete

Last edited: