This is the second in a series of posts introducing Solarkraft, a TLA+-based runtime monitoring solution for Soroban smart contracts. The first post, Why Smart Contract Bugs Matter and How Runtime Monitoring Saves the Day, gives an overview of smart contracts, the traditional security model, and runtime monitoring as a solution.

Solarkraft was developed in collaboration by Igor Konnov, Jure Kukovec, Andrey Kuprianov, and Thomas Pani.

Running example: the Soroban timelock contract

In this post, we explore how to write small and modular runtime monitors in Solarkraft for Soroban contracts. Soroban is the Rust-based smart-contract platform of the Stellar blockchain. We use a 127-line Soroban smart contract and specify part of its behavior in 11 lines of Solarkraft and TLA+.

The example is the timelock contract from soroban-examples. The contract has two functions: deposit() and claim(). With deposit(), a user transfers tokens into the contract and specifies allowed claimants plus a time bound. One permitted claimant may later claim the deposit with claim(), as long as the time bound is upheld.

Depositing tokens

pub fn deposit(env: Env, from: Address, token: Address, amount: i128, claimants: Vec<Address>, time_bound: TimeBound) {
    // ...

    // Transfer token from `from` to this contract address.
    token::Client::new(&env, &token).transfer(
        &from,
        &env.current_contract_address(),
        &amount);

    // Store necessary info to allow one of the claimants to claim it.
    env.storage().instance().set(&DataKey::Balance,
        &ClaimableBalance {token, amount, time_bound, claimants}
    );

    // ...
}

deposit() takes a source account from, an SEP-41 token contract token, an amount, a list of claimants, and a TimeBound specifying before or after what timestamp the amount becomes available.

pub enum TimeBoundKind { Before, After }

pub struct TimeBound { pub kind: TimeBoundKind, pub timestamp: u64 }

Assume Alice invokes deposit() to place test tokens into the contract for Bob:

deposit(addrAlice, addrTestToken, 100,
        [ addrBob ], {"kind": "After", "timestamp": 1718000000})

The token transfer moves the specified amount from Alice into the contract. The storage update records that only Bob may claim the money, and only after the specified Unix timestamp.

Claiming the deposit

// check that the timestamp is before/after the current ledger timestamp
fn check_time_bound(env: &Env, time_bound: &TimeBound) -> bool {
  let ledger_timestamp = env.ledger().timestamp();

  match time_bound.kind {
    TimeBoundKind::Before => ledger_timestamp <= time_bound.timestamp,
    TimeBoundKind::After => ledger_timestamp >= time_bound.timestamp,
  }
}

pub fn claim(env: Env, claimant: Address) {
  // Make sure claimant has authorized this call
  claimant.require_auth();

  // Just get the balance - if it's been claimed, this will simply panic
  let claimable_balance: ClaimableBalance =
       env.storage().instance().get(&DataKey::Balance).unwrap();

  if !check_time_bound(&env, &claimable_balance.time_bound) {
    panic!("time predicate is not fulfilled");
  }

  let claimants = &claimable_balance.claimants;
  if !claimants.contains(&claimant) {
    panic!("claimant is not allowed to claim this balance");
  }

  // Transfer the stored amount of token to claimant
  token::Client::new(&env, &claimable_balance.token).transfer(
    &env.current_contract_address(),
    &claimant,
    &claimable_balance.amount,
  );
  // Remove the balance entry to prevent any further claims.
  env.storage().instance().remove(&DataKey::Balance);
}

claim() checks that the claimant authorized the call, that a claimable balance exists, that the time predicate holds, and that the claimant is allowed to claim the balance. If one check fails, the contract panics and the transaction reverts. If all checks pass, the deposited amount is transferred to the claimant and the balance record is deleted.

Modular runtime monitors in TLA+

A runtime monitor is a list of properties that should hold about each invocation of the smart contract. In Solarkraft, we use TLA+ to write these properties. TLA+ is a formal specification language developed by Leslie Lamport for reasoning about distributed systems.

A first property: when to revert

One of the checks in claim() is that some claimable balance has been set. Here is how to specify this behavior in Solarkraft / TLA+:

MustRevert_claim_NoBalanceRecord(env) ≜ ¬instance_has("Balance", env)

MustRevert_ means that we expect the contract to revert if this condition holds. _claim_ identifies the smart-contract function the property applies to. NoBalanceRecord is the property name. The expression checks whether the storage key Balance exists in contract instance storage.

Another property: verifying the time bound

We expect claim() to revert if the time bound supplied by the depositor is violated:

MustRevert_claim_BeforeTimeBound(env) ≜
    ∧ Balance.time_bound.kind = Variant("Before", UNIT)
    ∧ env.timestamp > Balance.time_bound.timestamp

The two conditions are connected with conjunction. If the time bound is a Before bound and the block timestamp is after the specified timestamp, the call to claim() should revert.

Monitors in TLA+ are small and modular

The Soroban source code necessary to check the time bound is several lines of Rust with a helper function and pattern match. The behavioral Solarkraft specification is just three lines:

MustRevert_claim_BeforeTimeBound(env) ≜
    ∧ Balance.time_bound.kind = Variant("Before", UNIT)
    ∧ env.timestamp > Balance.time_bound.timestamp

We also did not have to specify the entirety of the time-bound functionality. We did not cover the After case. Specifications are modular in this sense: you can specify as little or as much behavior as needed, extend the specification later, and combine properties in different ways.

Specifying expected behavior

So far, we specified when a contract invocation should revert. We can also specify expected behavior on successful transactions. deposit() stores the supplied list of claimants and the time bound in ledger state. In Solarkraft and TLA+:

MustHold_deposit_BalanceRecordCorrect(args) ≜
    ∧ Balance'.token = args.token
    ∧ Balance'.amount = args.amount
    ∧ Balance'.time_bound = args.time_bound
    ∧ Balance'.claimants = args.claimants

The Soroban instance storage key Balance is mapped to a TLA+ variable. Balance and Balance' refer to ledger state before and after the transaction. The property checks that deposit() stores the function arguments correctly in the ledger state after successful execution.

What is next?

This post explored how to specify runtime monitors in Solarkraft / TLA+. We looked at the Soroban timelock contract and created a small modular Solarkraft specification of part of its behavior.

Further posts in the series, written by collaborators, appeared on protocols-made-fun.com: How to Run Solarkraft, The Force Awakens: Hybrid Blockchain Runtime Monitors, and The Rise of Model Checker: Verifying Blockchain Monitors In and Near Realtime.

Development of Solarkraft was supported by the Stellar Development Foundation with an Activation Award from the Stellar Community Fund of 50,000 USD in XLM.