Research Summary: Declarative Smart Contracts

TLDR

  • This paper presents DeCon, a declarative language to implement smart contracts and specify high-level properties.
  • It enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to contract debugging via data provenance.
  • The overhead of DeCon compared to the open-source reference implementation: 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.

Core Research Question

Can smart contracts be implemented in a declarative language?

Citation

Chen, Haoxian, Gerald Whitters, Mohammad Javad Amiri, Yuepeng Wang, and Boon Thau Loo. “Declarative Smart Contracts.” arXiv preprint arXiv:2207.13827 (2022). [2207.13827] Declarative Smart Contracts

Background

  • Smart contract analysis and verification: Prior work mostly focuses on general and low-level properties, e.g., re-entrancy attacks, transaction-order dependencies. DeCon, on the other hand, targets contract-specific, high-level properties.
  • Declarative programming: Declarative programming allows programmers to reason about the contract on the specification level, via inference rules, and frees them from low-level implementation details, e.g., data structures, algorithms, etc. For example, in SQL, users specify database queries as constraints on table entries, and the execution plan is generated automatically.
  • Run-time verification: In run-time verification, program properties are monitored during run-time, and aborts up on property violations. Assertions are a typical example of run-time verification. DeCon supports high-level property specifications and automatically instruments the program with assertions.
  • Data provenance: A visual presentation of the inference process of declarative programs. They are typically used for debugging or explaining program execution.

Summary

  • The key insight of this paper is that smart contract properties and operations can be naturally expressed in relational logic.
  • Smart contract transactions can be interpreted as relational tables, where table schema contains transaction parameters, e.g., sender, recipient, and amount.
  • Given this relational perspective of smart contracts, transaction functions are specified as declarative rules. A transaction is committed if the corresponding rule evaluates to true.
  • Views (read-only functions) can be specified as declarative queries on these transaction tables. For example, an account balance is its total income subtracted by total expense, each of which is a query on relevant transaction records.
  • Contract properties are also specified as declarative rules. They are interpreted as property violation queries, a special kind of views, and are expected to be always empty during correct executions.
  • The formal syntax and semantics of DeCon are presented in Section 3.
  • Given the contract logic and property specifications, DeCon automatically generates executable codes (in Solidity), with instrumentation that monitors the properties. The algorithm is presented in Section 4.

Method

  • Is DeCon expressive enough for typical smart contract applications? This paper performs case studies for five representative open-source smart contracts, and shows that they can be implemented in DeCon (Section 5).
  • How to generate efficient executable code? An observation in this paper is that smart contract transactions are executed in sequence. Therefore, DeCon borrows the idea of incremental view maintenance in databases to generate efficient update procedures, instead of scanning the whole databases as performed by typical declarative language implementation.
  • How to debug a smart contract written in DeCon? Provenance is a mechanism for explaining how certain tuples or facts are derived, right down to the input values. In an imperative language like Solidity, dependency information is difficult to be captured automatically (through data-flow analysis). In contrast, declarative rules in DeCon give explicit dependency information, where each tuple can be directly attributed to one rule, thus providing more clarity to the execution process.

Results

  • Benchmarks. We collect five reference smart contract implementations from public repositories and prior research.
  • Declarative smart contract implementation. We implement declarative counter-parts for all reference contracts with the same interfaces and functionalities. These contracts consist of 10 to 18 rules (column #Rules in Table 1).
  • Measurement metrics. We measure two metrics: (1) the size of EVM byte-code deployed on the blockchain; and (2) the gas cost for each transaction.
  • Measurement methods. On Truffle’s local blockchains, we deploy the contracts and set up 10 test accounts. Then we call each transaction interface to record gas cost reported by Truffle.
  • Results. The marginal overhead of DeCon compared to the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.

Discussion and Key Takeaways

  • Smart contracts and their high-level properties can be naturally expressed as declarative rules.
  • Declarative programming brings clarity to smart contract implementation and analysis.
  • However, the prototype compiler that generates executable code from declarative programs has certain overheads compared to hand-written reference implementations. Further optimization is needed to close the gap.

Implications and Follow-Ups

  • Additional language features, including contract composition, recursion, user-defined functions, etc.
  • Compiler optimization. There are extreme cases where the DeCon compiler generates contracts with non-negligible overhead to the reference hand-written code.
  • Static verification. To save the overhead of run-time verification, we can leverage the high-level abstraction of DeCon programs to perform static verification.

Applicability

  • DeCon can benefit smart contract developers who care about the correctness of the high-level design logic, with the declarative specification interface and run-time verification.
  • DeCon as a high-level language, can also support migration across platforms, although compilers targeting other platforms need to be developed.
4 Likes