soroban-decidable-verification

Experiments with verifying Soroban smart contracts using decidable logic. These are research prototypes. Use them at your own risk; no warranty is provided!

We offer a framework for reasoning about Soroban smart contracts using Ivy, a research tool for automation-assisted interactive development and verification of protocols.

You can create a model of your Soroban smart contract, state the desired safety properties, and then with the help of Ivy, interactively discover an inductive invariant that establishes the desired properties:

• translating your contract to Ivy is relatively straightforward, especially if the contract does not use complex data structures;
• discovering the inductive invariant can be a laborious process, requiring some expertise.

A tutorial for Ivy can be found in the doc/ folder in the Ivy repository.

Docker Image

We have a Docker image with a number of verification tools installed, including our custom versions of Ivy (hoping to be merged upstream) and mypyvy:

sudo service docker start
./docker/build
./docker/run

Examples

(1) To check all invariants on a given specification:

ivy_check token.ivy

(2) If an invariant fails to be maintained, you can obtain a concrete counter-example:

ivy_check trace=true token.ivy

This prints a counter-example to induction (CTI) in the form of a pre-state and step-by-step execution of the relevant transition.

(3) If you do not care about the step-by-step execution, you can greatly speed up the time it takes to generate the counter-example, you can run:

ivy_check model=true shrink=false token.ivy

This generates only the pre-state and tells Ivy to not minimize the generated model. Alternatively, if you want only the beginning of the step-by-step execution (e.g., to figure out which transition arguments we used), you can run:

ivy_check trace=true action_depth=0 token.ivy

action_depth can be any integer. Larger integers print more of the execution steps.

(4) To convert an Ivy specification to mypyvy, add attribute method=convert_to_mypyvy in the .ivy file and then run ivy_check.

If you want to use SMT queries to simplify the resulting mypyvy file, call ivy_check simplify=true. This might take minutes to hours on larger specifications, but should make queries on the mypyvy side much faster, especially for invariant inference.

You can then call mypyvy on the resulting .pyv file, e.g.:

mypyvy verify token.ivy
mypyvy updr token.ivy

Specification walkthrough

This repository contains Ivy specifications for:

• an abstracted Soroban environment (soroban.ivy)
• abstracted versions of the integers (integers.ivy)
• a model of the Token contract (token_contract.ivy)
• a model of the Liquidity Pool contract (liquidity_contract.ivy)

Soroban environment

We have modeled a bare-bones version of the Soroban environment, which provides basic support for reasoning about (a) authorization properties and (b) whether transactions panic.

The environment includes a partial_map module to represent mappings (key-value dictionaries) and two modules that abstract the integers: simplified_integer (addition, substraction, comparison) and decidable_integer (multiplication, division, sqrt). It does NOT model expiration for temporary storage – all storage is modeled as permanent.

Integers

In integers.ivy, we have three "versions" of integers, two of which are decidable models of the integers (simplified_integer with only comparison and plus/minus and decidable_integer, with more complex operations), and one which is the actual interpreted integers.

All properties of the models of integers are automatically verified against the actual integers.

All three modules expose the same interface, and you can easily toggle between the version by uncommenting the relevant line at the beginning of soroban.ivy.

Token contract

token_contract.ivy is translated from the soroban-examples repository. We have proven some basic consistency properties (all_balances_positive, all_allowances_positive) and an authorization property (allowance_implies_authorization) that states that allowances can only exist if there was some authorization (i.e. signature) provided by an end-user in the past.

The associated token.ivy file includes a "two-state" property, i.e. a property that relates the pre- and post-states of all transitions, which shows that a user's balance can only decrease if authorized (either directly by the user, or indirectly through an allowance signed by the user).

This property is stated in the end_transaction_hook action, which is called at the end of every transaction and has access to both the pre- and post-state (pre-state is accessed through fields prefixed by _, e.g. balance._map).

Findings:

• It was possible to create "zero" allowances without any authorization from the account owner. This is not a security issue, but allowed the creation of "noise" in the state.

Liquidity pool contract

liquidity_contract.ivy is translated from the soroban-examples repository. There is also a simplfied version (see the section below) in simplified/pool.ivy. (Indeed, the simplified version is preferable for experimentation.)

We have not been able to prove any substantial correctness property (in particular, we have not proven the no_depositor_loss property), largely due to limitations about decidable integers. Driving this proof to completion is left as future work.

Nonetheless, we had some findings:

• There was a correctness-relevant typo in get_deposit_amounts;
• In certain scenarios, it was possible to "brick" the LP contract by ensuring all deposit transactions panic. The contract was written to assume that, upon the first deposit, it will always be the case that reserve_a > 0 && reserve_b > 0, but this was in fact not the case. States that violate this property were reachable both via deposit and via swap transitions, and all further deposits would panic. Existing shares would still be withdrawable, so no funds were at risk.
  • The root cause of the above issue is the "redistribution" mechanism that ensures that tokens transferred directly to the LP contract (without being deposited) are (morally) assigned to whoever next withdraws shares. (The implementation is here – note that the balances of tokens are used to compute the number of withdrawn tokens, not the reserves.) This ensures that these tokens are not "lost", but makes it more difficult to reason about the properties of the LP property.
• The formalisation explictly exposed this (perhaps obvious) requirement: the LP contract address must NOT have token authorizations for the tokens in the pool. (Otherwise, whoever was authorized to act on the pool's behalf can steal the pool's contents.)

Simplified contracts

We originally hoped we could discover invariants directly on the "naturally-translated" specifications described above. This works in principle, but SMT solver queries (invoked by ivy_check) are relatively time consuming for the full specifications, sometimes taking on the order of tens of minutes for a single query.

To ease the process of discovering invariants, we developed simplified versions of these specifications (found in models/simplified) and used those to discover the invariants (and, particularly, to apply invariant inference tools) and then back-ported the invariants to the main specifications.

We experimented with mypyvy's implementation of UPDR, with moderate success, but performance is currently too bad (especially for the non-simplified specifications) to offer good UX for developers hoping to use this framework to automatically reason about their contracts.

For now, the manual Ivy methodology of running ivy_check trace=true spec.ivy and repeatedly eliminating counter-examples to induction (CTIs) is the only feasible approach.

Tips

• Remove constants and relations that are not needed in your specification (e.g. minus_one or ghost state), as each extra constant/relation can exponentially increase solver times