Skip to main content

1. The Actor-Boundary Invariant Model

1. Introduction: The Async Interference Problem​

In the context of the Internet Computer (ICP), smart contracts are built around the Actor Model. Each canister (actor) processes a single message at a time, providing isolated state and sequential execution within a message's boundaries. However, interactions between canisters require asynchronous messaging (await). When a canister awaits a response from another, its execution is suspended, and the canister is free to process other incoming messages before the original execution resumes.

This creates a critical vulnerability known as Async Interference or Reentrancy. While suspended, the internal state of the actor may be mutated by interleaving messages. If the suspended function resumes under the assumption that the state remains unchanged since before the await, it may make incorrect, potentially catastrophic decisions (e.g., double-spending, flawed authorization, or corrupted internal accounting).

Sector9 addresses this class of bugs with formal checks for local handler correctness and explicit protocol-level modeling. Instead of relying purely on dynamic locks or runtime reentrancy guards, Sector9 employs a deductive Actor-Boundary Invariant Model. This article explains that model through src/viper/mvir_await.ml, src/viper/mvir_actor_invariants.ml, and src/viper/lower_stmt_async.ml.

2. The "Atomicity-Until-Await" Paradigm​

Sector9 operates on the "Atomicity-Until-Await" paradigm. The core rule enforced by the verifier is: A message handler executes atomically between await points.

Consequently, all actor invariants and contract-visible state consistency must hold at three critical junctures:

  1. Method Entry (Precondition phase)
  2. Method Exit (Postcondition phase)
  3. Immediately before each await (Suspension phase)

To prove local correctness, Viper (the deductive backend) must model what happens to actor state during suspension. Since the verifier cannot predict which messages will interleave, Viper takes a conservative, effect-driven approach: it invalidates shared actor locations that public methods may write, plus deep mutable or escaping actor-rooted locations that cannot be treated as stable. Fields outside the inferred interference set can keep stronger frame facts.

3. Actor Invariants: The $Inv($Self) Predicate​

The implementation of actor invariants is handled heavily in src/viper/mvir_actor_invariants.ml. When a developer writes an invariant block in their actor, the system translates this into a Viper predicate, typically named $Inv.

Injection of Preconditions and Postconditions​

The mvir_actor_invariants.ml pass detects if a program has explicit actor invariants (e.g., declarations matching the pattern invariant_<line>). If so, it augments every public/actor method.

For a method to execute, it requires the $Inv($Self) predicate as a precondition (meaning the state is valid when the method begins). It also must ensure $Inv($Self) as a postcondition (meaning the method leaves the actor in a valid state).

let patch_method (id, ins, outs, pres, posts, body_opt) =
  let self_e = self_exp_from_params ins in
  (* ... *)
  let inv_pred = Mvir_helpers.(!!!) self_e.Source.at (InvPredicateE { self = self_e }) in
  (* Add InvPredicateE to pres and posts *)

Self-Framing and Unfolding​

A major challenge in verification is that contracts (requires, ensures) often need to read actor fields to evaluate logical properties. However, if the fields are bundled inside the opaque $Inv($Self) predicate, the verifier cannot read them without "unfolding" the predicate.

The pass actively rewrites expressions to maintain self-framing. Non-resource contracts (pure boolean expressions) that touch the actor's heap (uses_self_heap) are wrapped in an UnfoldingE node:

Source.annotate note (UnfoldingE (Vpr_names.inv, [self_e], e')) at

This temporarily unfolds the invariant predicate just enough to evaluate the contract, then folds it back, keeping the permission accounting clean.

Snapshotting with old(...)​

In Sector9, old(e) refers to the state of e at the entry of the method, not the state before the most recent await. To ensure old(...) evaluations remain sound, the AST pass also wraps old expressions that touch the heap inside the $Inv unfolding. This guarantees that the entry state evaluated in postconditions is mathematically rooted in the invariant-guarded snapshot captured at method initiation.

4. Modeling the await Boundary​

The actual suspension logic is materialized in src/viper/mvir_await.ml. This pass (Phase 6 of the MVIR pipeline) treats the await keyword as a hard semantic boundary.

Havoc and State Invalidation​

When an await occurs, the local variables of the method remain stable, but aliases to actor state or escaping heap references are invalidated. Sector9 implements this by emitting a HavocS marker.

let rewrite_stmt ~(self_allowed : bool) ~(has_perm : bool) (s : stmt) : stmt list =
  match s.Source.it with
  | AwaitBarrier { havoc } when self_allowed && has_perm && should_havoc havoc ->
      (* ... *)
      [ Source.annotate note (HavocS havoc_locs) at;
        Source.annotate note (AwaitBarrier { havoc = None }) at;
        require_inv_unfold note at
      ]

The sequence of events around an await in MVIR is:

  1. Require Invariant: The system implicitly asserts that the actor invariant holds (meaning the developer must have restored the state to validity).
  2. Havoc (HavocS): The verifier assumes the environment may mutate the shared actor locations in the computed interference set. The Viper backend encodes this by releasing and restoring the relevant permissions, assigning fresh nondeterministic values to those locations while preserving facts that are outside the await havoc set.
  3. AwaitBarrier: Marks the expiration of borrows.
Actor-Boundary FlowAwait turns actor state into a verifier boundary
01Atomic handler

Code runs against known actor state until it reaches a suspending call.

02Require invariant

$Inv($Self) must hold before the actor exposes state to interleaving messages.

03Havoc shared writes

Publicly writable or otherwise nonstable actor locations are refreshed as nondeterministic values.

04Resume with proof debt

Locals survive, stale heap assumptions do not. Proofs must use snapshots or invariant facts.

SurvivesLocal snapshots
ResetInterference set
RequiredCatch-all recovery

By releasing and restoring permissions around the await boundary, Viper mathematically severs the connection between pre-await and post-await facts for locations that may be touched by interleaving messages. If a developer needs such a value to persist across an await, they must copy it into a local variable or make the needed fact part of a stable invariant.

Explicit State Exclusions​

Because HavocS invalidates trust in the computed interference set, Sector9 forces developers into a safer design pattern. If code says:

let old_balance = this.balance;
try { await some_call(); } catch (_) {};
assert this.balance == old_balance; // FAILS VERIFICATION

This will fail verification because Viper cannot prove this.balance wasn't modified during suspension. The developer is forced to explicitly track state indices, utilize async channels, or structure the protocol so that interleaving cannot violate business logic.

5. Async Call Lowering and Channels​

In src/viper/lower_stmt_async.ml, Sector9 translates high-level async calls into lower-level MVIR constructs that can be reasoned about.

Remote Stubs​

Instead of trying to statically inline or analyze external canister code, Sector9 generates "Remote Stubs".

let declare_remote_stub (ctxt : ctxt) (at : Source.region) (base : M.id) (arg_exprs : M.exp list) (ret_typ : T.typ) : id =

A remote stub encapsulates the type signature and expected effects of an external call. At the call site, Viper learns only the exported contract surface the imported method makes available.

  • Remote-safe result facts become assume obligations after the stub call.
  • Hidden remote state is heavily guarded; it does not become locally readable state.

Channel Predicates and Pending Counters​

To model the mechanics of message passing, Sector9 injects channel bookkeeping. When an async call is made, it increments a pending counter on a specific "site field":

( [Syntax_helpers.inc_field_stmt at site_fld; Syntax_helpers.inc_field_stmt at chan_fld],
  [Syntax_helpers.dec_field_stmt at site_fld; Syntax_helpers.dec_field_stmt at chan_fld] )

This is a powerful formalization: it allows the verifier to maintain invariants about the number of outstanding requests (e.g., invariant pending_withdrawals == 0). This is crucial for DeFi protocols that need to lock funds while an external transfer is pending.

The try/catch Requirement​

A notable enforcement in Sector9 is that every await that may suspend must appear inside a try { ... } catch (_) { ... } block with a catch-all. Because remote calls can fail (due to canister traps, network timeouts, or upgrade wipes), the verifier refuses to verify code that blindly assumes an await will return successfully. This forces the developer to explicitly handle the rollback or failure state, ensuring the actor invariant is restored even on the error path.

6. Comparison with Other Models​

vs. Solidity Reentrancy Guards​

In Ethereum/Solidity, the standard defense against Reentrancy is a dynamic nonReentrant mutex.

  • Solidity: Throws a runtime error if a reentrant call occurs. It protects the specific function but does not protect against cross-function reentrancy unless applied globally, which limits composability. It also costs gas on every invocation.
  • Sector9: Models reentrancy statically. By havocing actor state at the await point, the verifier rejects code that relies on stale state unless the needed fact follows from an invariant or local snapshot. Enforcing invariant checks before the await also ensures the actor exposes a state that satisfies its declared invariant while suspended.

vs. Move Linear Types​

Move (Aptos/Sui) eliminates many reentrancy issues by eschewing dynamic dispatch and utilizing linear types (resources).

  • Move: You cannot have a shared reference to a resource while it is being mutated, and global storage access is strictly gated.
  • Sector9: Retains the familiar asynchronous actor model of ICP but overlays strict permission accounting. While Sector9 doesn't use linear types natively for everything, the Viper translation enforces linear permissions in the background. You cannot access a field without an acc(field) permission, and those permissions are yielded to the environment during an await.

vs. Pony's Causal Messaging​

Pony uses reference capabilities to ensure data-race freedom at compile time, eliminating the need for locks.

  • Pony: Highly focused on local memory safety and thread concurrency without blocking.
  • Sector9: Geared specifically toward the distributed, asynchronous reality of ICP where "threads" are entirely different consensus subnets. Sector9's model is heavier (using SMT solvers) because it proves business logic (e.g., balances summing correctly) alongside memory safety.

7. Conclusion​

Sector9's Actor-Boundary Invariant Model is a rigorous, pessimistic approach to asynchronous programming. By treating await points as total memory barriers (HavocS), it rejects local proofs that depend on unstated async state assumptions.

Strengths:

  1. Stale-State Discipline: Verified code cannot use pre-await actor state after suspension unless it is preserved by a local snapshot or an invariant.
  2. Invariants as Boundaries: By forcing invariants to hold before suspension, the actor presents an invariant-satisfying state to other messages.
  3. Forced Error Handling: The strict try/catch rule around await prevents proofs from silently assuming remote calls always succeed.

Limitations:

  1. Developer Friction: Developers must aggressively cache state in local variables before an await and manually reconstruct their worldview upon resumption. This can make code verbose.
  2. Pessimism: The model assumes any mutation in the await interference set can occur. If invariants or public footprints are too loose, the developer might not be able to prove post-await logic, even if the deployed protocol would not take that path. The TLA+ lane can model narrower protocol schedules, but the local Viper lane remains conservative unless the source contracts and footprints justify stronger facts.

Ultimately, mvir_await.ml and mvir_actor_invariants.ml form the bedrock of Sector9's security model, transforming the chaotic reality of distributed asynchronous messaging into a strict, verifiable Hoare-logic framework.