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.
7 Likes

Weldon job, @hxc, this paper presents DeCon, a Declarative programming language for executing smart contract and indicating contract-level properties, I see that DeCon, as a declarative programming language for smart contract was introduced to make smart contracts easier to analyze and verify. It is clear that DeCon complies declarative specifications into executable Solidity programs that run on blockchains, e.g., Ethereum, and monitor the specified properties at run-time.

Elements of A DeCon contract;
• Relations
• rules, and
• relation annotations.

I think for better understanding of this paper, it is required to present the main objective of this paper;

• The author design DeCon, a declarative language that unifies smart contract implementation and specification and demonstrated its expressiveness via case studies on representative smart contracts and their high-level correctness properties.

• They design an algorithm to compile these high-level specifications into executable Solidity programs, with instrumentation for run-time verification.

• Finally, implemented and experimentally evaluate DeCon. The evaluation shows that the generated executable code has comparable efficiency with the equivalent open source implementation of the same contract (14% median gas over-head), and the overhead of run-time verification is moderate (16% median gas overhead

As a result of the above, in DeCon, smart contracts are specified in a high-level and executable manner, and which offers opportunities for efficient analysis and verification and bringing clarity to transaction execution via data provenance. Honestly, Contracts implemented in DeCon demonstrate comparable efficiency to open-source reference implementation. I hope and believe that DeCon compiler needs further optimization to generate more efficient executable code.

3 Likes

The type of collaboration efforts by the business sme and the sc dev teams is quite remarkable, it is sometimes unbearable to be in technical subject matter expertise teams, maneuvering. I would like to know what are the specifications or even the data element requirements for accomplishing the SC logic and algorithm.

Great summary @hxc :clap: :clap:

It is always fascinating to find new information about smart contracts and their development.

Is DeCon a different programming language from Solidity or a form of it? Do they share any similarities?

Additionally, does DeCon help developers avoid creating attack vectors for exploits/hacks? I’m asking because the majority of contract attacks are enabled by a flaw in the design/architecture of the code which the attacker exploited.

Finally, you mentioned certain overheads that emanate from using the prototype compiler. What are they, and can they be avoided, or eliminated?

2 Likes

Hi @Havesto,

Glad that you are interested in DeCon.

Is DeCon a different programming language from Solidity or a form of it? Do they share any similarities?

DeCon is a different language from Solidity.
In fact, it is a declarative language, which means it only specifies what are the correct transaction conditions,
and view definitions, but not how to compute them. On the contrary, Solidity is an imperative language,
where it contains all the instructions to compute the results. The analogy here is SQL (declarative) v.s. C (imperative).

The connection between the two is that DeCon is compiled to Solidity in order to be executed.

does DeCon help developers avoid creating attack vectors for exploits/hacks?

DeCon avoids a lot of attack vectors found in Solidity, like re-entrancy or mishandled exceptions, etc.

Because, as mentioned above, DeCon is a declarative language, so programmers do not implement
the instructions themselves. Instead, these instructions are generated by the DeCon compiler,
and thus a lot of common attack vectors can automatically be avoided.

On the other hand, DeCon compiler could also have its unique attack vectors,
which indeed is an interesting research question to be answered.

Finally, you mentioned certain overheads that emanate from using the prototype compiler. What are they, and can they be avoided, or eliminated?

There are two sources of overhead: DeCon compiler, and run-time verification.

Optimizing the DeCon compiler to generate more gas-efficient code is an ongoing work in our group.

Mitigating run-time verification is another thread of ongoing work, where we use static verification techniques
to prove some of the properties before execution, thus avoiding the run-time monitoring altogether.

Thanks!

2 Likes

@hxc Thank you very much for this fantastic work.

DeCon models each smart contract as a set of relational tables that store transaction records. This relational representation of smart contracts enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to contract debugging via data provenance. Specifically, a DeCon program consists of a set of declarative rules and violation query rules over the relational representation, describing the smart contract implementation and contract-level properties, respectively.
A tool was develop to compile DeCon programs into executable Solidity programs, with instrumentation for run-time property monitoring.