PaperlayerView exact revision on arXiv

Source-linked AI summary

Scilla: a Smart Contract Intermediate-Level LAnguage

Ilya Sergey, Amrit Kumar, Aquinas Hobor

arXiv:1801.00687v1cs.PL

TL;DR

Smart contracts can exhibit subtle behavior that threatens reliability, while formal methods offer a way to reason about behavior before deployment. Scilla uses communicating automata and separates contract computation from communication to support verification; the paper reports a Coq embedding and proved contract properties, while noting that its preliminary model omits several features.

  • Problem

    Smart-contract semantics can diverge from developers’ expectations, and formal guarantees are valuable because deployed contracts are nearly impossible to patch.

    Source: §1 · p. 1

  • Method

    Scilla is an intermediate language based on communicating automata that separates contract computation from communication and supports formal reasoning about transitions.

    Source: §1 · p. 2

  • Results

    The paper presents a Coq embedding of Scilla and reports proved safety and liveness properties of a contract.

    Source: §3.4 · p. 9, §6 · p. 12

  • Takeaways & Limitations

    The automata model provides a basis for mechanised reasoning about contract executions and their safety properties.

    Source: §3.2 · p. 6, §6 · p. 12

    The preliminary verification model omits resource semantics such as gas, full blockchain reflection, continuations, and exceptions.

    Source: §3 · p. 5

Abstract

from arXiv · show

This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspect of smart contracts on a blockchain, allowing for the rich interaction patterns, and a programming component, which enjoys principled semantics and is amenable to formal verification. Scilla is not meant to be a high-level programming language, and we are going to use it as a translation target for high-level languages, such as Solidity, for performing program analysis and verification, before further compilation to an executable bytecode. We describe the automata-based model of Scilla, present its programming component and show how contract definitions in terms of automata streamline the process of mechanised verification of their safety and temporal properties.

1 Introduction

Scilla is an intermediate-level language for smart contracts, designed to make contract behavior amenable to formal reasoning while separating computation from blockchain communication. Its introduction motivates this design through the difficulty of reliably understanding and verifying smart contracts before deployment.

1 Introduction

  • Smart contracts are difficult to secure because subtle operational behavior can diverge from developers’ expectations, and deployed contracts are nearly impossible to patch.The paper cites the DAO and Parity wallet attacks as examples of such divergences.Source: §1 · p. 1
  • Formal methods can specify operational behavior and check safety and liveness before contracts are irrevocably committed, while language design must balance expressivity, state, communication, and principled execution semantics.The introduction also weighs support for machine-checked reasoning against the complexity of expressive, stateful, communicating contracts.Source: §1 · pp. 1–2
  • Scilla targets compilation from higher-level languages to executable bytecode, with analysis and verification at the intermediate-language level.The paper outlines the automata model, verification support, and the manuscript's later discussion of contract languages.Source: §1 · p. 2, Paper outline · p. 2
  • Communicating automata separate atomic in-contract computations from message exchanges, supporting reasoning about contract effects and blockchain-wide interactions.Transitions end with explicit communication when control must pass to another party.Source: §1 · p. 2
  • Separating pure expressions, local state manipulation, and blockchain reflection is intended to give transitions predictable effects and support progress, type preservation, and verification.The paper draws on functional programming with effects; in-contract transition computations must terminate.Source: §1 · p. 2
  • Explicit continuations restore expressivity to an automata-based model by letting the execution environment invoke continuations after external calls.External calls can remain the last instruction while supporting translation from languages such as Solidity.Source: §1 · p. 2

2 Contracts as Communicating Automata

Scilla presents contracts as communicating automata, separating contract computation from communication with other parties. Its crowdfunding example illustrates transitions, state effects, and continuations for handling returned values while preserving a structured model for verification.

2 Contracts as Communicating Automata

  • Scilla’s crowdfunding example models a campaign with immutable owner, deadline, and minimum-goal parameters, plus mutable backer records, a funded flag, and contract balance.The goal is a minimum target, not a hard cap.Source: §2 · p. 2

2.1 Transitions and messages

  • Transitions act like methods but execute atomically: external interaction occurs when a transition receives a message and when it ends by sending messages or returning.Messages identify transitions with tags; filters can check message fields and state, while complex checks and state writes belong in the transition body.Source: §2.1 · pp. 2–3

2.2 Basics of program flow

  • Transition bodies use let-in bindings and branching for pure computation, and each execution branch ends by sending messages or returning.A send may carry a continuation; the crowdfunding example uses the empty continuation because it needs no further execution after a callee returns.Source: §2.2 · pp. 3–4

2.3 State and effects

  • Scilla distinguishes pure expressions from commands that read or write mutable fields, making transition effects easier to reason about separately from expression evaluation.Read-only blockchain introspection, such as reading the current block number, is syntactically marked and supports reasoning about liveness; exceptions are not explicit in the current model and are handled at runtime.Source: §2.3 · p. 4

2.4 Advanced control flow and continuations

  • Scilla’s core transitions use tail calls, so control passes to another contract only through an explicit message; explicit continuations support work that must resume with a callee’s returned value.Continuations are invoked passively from an execution stack, unlike active transitions, which require a message. A continuation may schedule another continuation, so cross-contract cycles can potentially fail to terminate, while standalone transitions terminate.Source: §2.4 · pp. 4–5
  • The paper adopts CPS transformation and defunctionalisation as the design basis for representing continuations, and describes a future translator from a subset of Solidity into Scilla.The translator is intended to produce transitions for direct control flow and continuations for return-flow.Source: §2.4 · pp. 4–5

3 Mechanised Verification of Scilla Contracts

This section presents mechanised verification of Scilla contracts using a preliminary Coq model, including proofs that a non-funded crowdfunding contract preserves donated funds and records and allows backers to reclaim donations after a failed campaign. It also notes omitted model features and further correctness and liveness properties that remain unproved.

3 Mechanised Verification of Scilla Contracts

  • The preliminary model leaves out resource semantics such as gas, full blockchain reflection, continuations, and exceptions, which the authors consider orthogonal to the automata-based approach.The section frames Scilla’s automata model as supporting formal semantics for executions and properties across a contract’s life-cycle.Source: §3 · p. 5

3.1 Contracts in Coq: basic definitions and properties

  • The Coq embedding shallowly represents Scilla’s pure component with Gallina functions and its message-passing transitions as a relation, with unique transition tags enforced by the contract type.Other correctness guarantees must be proved for each user-defined contract.Source: §3.1 · pp. 5–6

3.2 Semantics, safety, and consistency properties

  • Contract traces encode executions as steps over schedules, supporting generic safety properties and temporal properties relating states across traces.Safety can be proved by showing a property holds initially and is preserved by each transition; the since_as_long connective expresses preservation under conditions on schedule elements.Source: §3.2 · pp. 6–7

3.3 Embedding Scilla into Coq

  • The Crowdfunding contract is translated into Coq by hand, using Gallina state-passing functions and sequences to encode mappings.The current encoding omits explicit reentrancy; a transition returning no output leaves contract state unchanged and represents an exception.Source: §3.3 · pp. 7–9, Figure 4 · p. 8

3.4 Reasoning about contract behaviour

  • Quantifying safety and temporal properties over all schedules lets the model verify contract behavior modularly against any interaction allowed by its transitions.Schedules act as an external oracle for the nondeterminism of on-chain interaction, including potential adversaries.Source: §3.4 · p. 9
  • The Crowdfunding contract’s balance always covers recorded donations while the campaign remains unfunded, a property proved as safety.The property states that the contract can reimburse all recorded backers unless the campaign has been funded.Source: §3.4 · p. 9
  • A machine-checked proof under 50 lines of Coq shows that a non-funded campaign does not lose or spend its backers’ money.The proof uses the safe_ind induction principle and establishes that balance_backed holds in the initial state.Source: §3.4 · p. 9
  • A donation record persists as long as its backer does not try to withdraw, as proved by induction over reachable execution traces.The proof shows the contract does not alter the record during execution while schedules contain no message from that backer.Source: §3.4 · p. 9
  • With a recorded donation, an unfunded campaign below its goal, and an expired deadline, a backer can claim the donation back.The 10-line Coq proof states this as a one-step safety property: the backer can send a message that elicits a return message containing the donation.Source: §3.4 · pp. 9–10
  • These three properties do not establish that the contract is bug-free; owner withdrawals after success are unverified, while the formalisation can support unshown liveness proofs against funds remaining locked forever.The paper notes that the finite-time ability of either backers or the owner to relieve contract funds is a liveness property, but does not prove it here; it cites the Parity multi-signature wallet as a motivating example.Source: §3.4 · p. 10

4 Discussion

Scilla’s communicating-automata model opens opportunities for logic-based contract verification while raising questions about language expressivity. The discussion frames verification around contract-specific correctness properties and examines what the Coq encoding guarantees and leaves open.

4 Discussion

  • Communicating automata create opportunities for logic-based verification while raising challenges for the design and expressivity of high-level contract languages.Source: §4 · p. 10

4.1 Towards logic-based reasoning about contracts

  • Correctness conditions vary by contract; the paper combines universal safety and temporal properties, while precise specification of desired properties remains outside its scope.Source: §4.1 · p. 10
  • Scilla’s semantic foundations and logical vocabulary are intended to let programmers formulate and mechanically prove reasonable contract properties of interest.Source: §4.1 · p. 10
  • Encoding programs and semantics in a dependently typed proof assistant offers a principled way to verify implementations in terms of programs rather than models.Source: §4.1 · p. 10

4.2 On Turing-completeness and contract language design

  • Coq’s total functions make Scilla transitions terminate and support symbolic execution, with third-party tools proposed for future proof automation.Source: §4.2 · p. 10
  • Finite transitions can still take arbitrarily long, and circular message-passing calls can enable potentially non-terminating executions; parameterized cost bounds are planned.Source: §4.2 · p. 10

5 Related Proposals

The proposals differ in their treatment of state, contract communication, and verification. Scilla’s automata-based model supports shared state and external interactions while restricting how those interactions interleave with local computation.

Typecoin and Simplicity

  • Typecoin’s linear UTXO logic and Simplicity’s self-contained transactions lack Scilla’s shared-state, communicating-contract model.Simplicity does not support communicating contracts, while Typecoin’s logic handles splitting and merging UTXOs rather than complex states.Source: §5 · p. 11

Solidity

  • Scilla restricts Solidity’s reentrancy exposure by requiring external calls at transition end and passing return values explicitly; the paper also demonstrates safety and liveness proofs.The comparison links arbitrary interleaving of local state changes and external calls to a class of re-entrancy attacks.Source: §5 · p. 11

Bamboo

  • Bamboo changes contracts when state changes, whereas Scilla keeps the transition function fixed and represents such morphing with a state component.The passage also distinguishes Bamboo for not focusing on contract verification.Source: §5 · p. 11

Babbage and F⋆ embedding

  • Babbage is hard to compare because it lacks formal design semantics; the F⋆ embedding verifies Solidity but does not propose a new programming model.Babbage is described as a conceptual design using a mechanical rather than textual model.Source: §5 · p. 11

Viper

  • Viper plans to restrict state changes after non-static calls; Scilla requires every external call to be the transition’s final instruction.Source: §5 · p. 11

Rholang

  • Unlike Rholang, Scilla bounds recursion and makes external calls tail calls, avoiding complex interleaving and making safety properties easier to prove.Rholang admits unbounded recursion.Source: §5 · p. 11

Plutus and OWL

  • Plutus is simpler and lacks Scilla’s global-state manipulation and external calls, while OWL favors pure functions over Scilla’s separated interactions.The paper also describes Scilla contracts as easily composable through their automata-based design.Source: §5 · p. 11

Zen, Michelson, and Liquidity

  • Zen and Michelson are stateless or purely functional, unlike Scilla’s transitions that affect external state; Liquidity shares Michelson’s restrictions.The paper notes that Zen’s purity removes side effects and interaction with other contracts, limiting the contracts it can build.Source: §5 · p. 11

6 Conclusion & Future Work

The paper outlines Scilla as an intermediate-level smart-contract language that separates communication from programming and uses communicating automata. It reports a Coq embedding with safety and liveness proofs, and identifies formalization and implementation as future work.

Conclusion

  • Scilla is an intermediate-level smart-contract language that separates communication from the programming component and uses communicating automata.Source: §6 · p. 12
  • The authors embedded a Scilla contract in Coq and proved safety and liveness properties of that contract.Source: §6 · p. 12

Future Work

  • Future work includes defining Scilla’s formal grammar and semantics, implementing the language, and developing and verifying contracts on a real-world blockchain platform.Source: §6 · p. 12
Loading 1801.00687v1…