Research Summary: Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications

[David]

TLDR

• In Ethereum dApps, contracts and clients are implemented as separate programs – in different programming languages – communicating via send and receive operations. Such a design makes it hard to express and understand the distributed program flow of dApps, and therefore increases the risk of mismatches in the client-contract interface, which can lead to large financial losses.
• In this paper, we introduce a tierless programming language for Ethereum dApps, called Prisma. The main idea is to implement the contract and its clients in one unit and express communication in direct-style, similar to the async/await pattern known from other languages. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible.
• Prisma captures the internal semantics of dApps more naturally than previous approaches to dApp programming by reversing the role of the smart contract. Instead of interpreting the smart contract as a passive entity waiting for input of the clients, in Prisma, the smart contract becomes the active entity managing the program flow and passing it to the clients in case input is required.

Core Research Question

How to address today’s shortcomings in the development of Ethereum dApps, most importantly the separation of contract and client on two independently implemented tiers and the finite state machine-style encoding of the communication protocol?

Citation

• Conference version: David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, Mira Mezini.
  “Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Abstract)”. ECOOP (2022).
• Extended version: David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini. “Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Version)”. arXiv preprint arXiv:2205.07780 (2022).

Background

• DApp development with Solidity: The code snippet below depicts the smart contract part of a fundable TicTacToe game. The players first deposit their stakes in the contract (Fund) before actually playing the game via alternating moves (Move). Once the game terminates, parties can withdraw their winnings (Payout).
  
  
  
  In order to prevent unexpected behavior due to functions being called in the wrong order or by the wrong party, developers check before every function call if the function may be called by the callee in the current phase. This way, programmers implicitly define a finite state machine (FSM) for the intended client contract interaction protocol. The FSM for the given smart contract is given below. Insufficient program flow control can lead to unintended behavior and financial losses. In the example, if the developer forgot line 12, a malicious client could trigger a premature payout potentially preventing an honest winner from withdrawing its reward.

  

Summary

• Typically, Solidity contracts and the corresponding clients are written as separate programs – in different programming languages – communicating via send and receive operations encoding the client contract communication protocol in a finite state machine-style.
• This has the following two major problems.
  • Developers have to master two technology stacks, the one of the contract and the one of the client.
  • The distributed send and received operations make distributed program flow awkward to express and reason about.
• To address these shortcomings, we design a new programming language, Prisma. From a design point-of-view Prisma solves several problems present in the typical approach of dApp development based on Solidity.
  • First, Prisma allows the implementation of contract and client in one unit, in one programming language. Prisma code constitutes a subset of Scala which is compiled to Solidity contract code and Scala client code.
  • Second, Prisma enables developers to explicitly define the client contract execution protocol of the dApp and automatically enforces correct execution of said protocol.
  • Third, Prisma forces developers to explicitly define access control for every contract invocation, hence, reducing the risk of human failure.
• The figure below depicts the same TicTacToe game as above but implemented in Prisma.
  
  • Both contract and client functionality is implemented in the same code unit.
  • The contract client interaction protocol is explicitly defined via the init function. This function corresponds to the main function known from other programming languages. The contract initiates the dApp by executing the init function. Once, the execution reaches an awaitCl expression, the contract passes the control flow to the clients and waits for a response. Clients execute the code block initiated by the awaitCl expression and delimetered by the curly brackets. The response is sent to the contract which continues the execution after the awaitCl expression.
  • Developers specify which client the contract is waiting for via the lambda expression provided to the awaitCl expression as the only parameter. The lambda expression takes a client address as input and outputs a boolean value. Clients evaluate the lambda expression with their own address as input and only execute the subsequent code block if the lambda expression evaluates to true.
• We present a core calculus, formalizing both Prisma and its compiler, as well as a formal proof showing that our compiler preserves the behavior of the dApp in presence of an attacker controlling the client code.
• We provide an extensive evaluation based on twelve case studies implemented in Prisma and in Solidity showing (1) that Prisma supports the most common dApp scenarios and (2) the additional layer of abstraction introduced by Prisma comes with reasonable overhead in terms of gas consumption.
• We provide a detailed comparison of Prisma with related work. The comparison highlights the benefits of Prisma from a design point of view, i.e., the benefits of implementing a dApp in a single program, where protocols are expressed by control flow and enforced by the compiler.

Method

• We refer the reader to our paper for more details on language design, formalization, proofs or comparison to related work. Here, we focus on the empirical evaluation showcasing applicability and efficiency of Prisma.
• To show applicability, we have implemented twelve case studies representing the most common classes of dApps: Financial, Wallet, Notary, Game, and Library.
• To show efficiency, we have compared the gas consumption of the case studies implemented with Prisma to the gas consumption of the same case studies implemented with Solidity.

Results

• The figures below illustrate the absolute gas usage (a,c) and relative overhead (b,d) of contract deployment (a,b) and contract interactions (c,d) of contracts written in Prisma compared to those written in Ethereum.
  

• The deployment overhead is below 6 %. The execution overhead is below 10 % which amounts for at most 3.55 K gas (0.6$ at April, 2021). Both overheads are mainly caused by the code and variables required to manage the program flow on the contract side, i.e., to automatically enforce the correct execution of the contract client interaction protocol.
• It is not possible that Prisma smart contracts achieve a better gas consumption than Solidity smart contracts. Prisma code is compiled to Solidity code, hence, every contract compiled from Prisma can be implemented in Solidity directly. The current version of our compiler constitutes a research prototype. We are confident that additional engineering effort can reduce the observed overhead further.

Discussion and Key Takeaways

• From a design point-of-view, Solidity comes with several shortcomings that aggravate the dApp development and increases the potential of errors.
• We propose a new programming language, Prisma, that overcomes many of the disadvantages of Solidity. Most importantly, it allows the implementation of contract and client in one unit, in one programming language, and enables developers to explicitly define the client contract execution protocol of the dApp.
• While significantly improving the dApp development from a design point-of-view, Prisma comes with acceptable efficiency overhead that is most likely to become negligible with further engineering efforts.

Applicability

• The implementation, we have published together with our paper, constitutes a research prototype. It can be used by other developers to get to know our programming language, its compiler and the case studies used for evaluation. Further, it can be used to implement additional case studies. However, we do not claim completeness of our implementation, i.e., there might be single Solidity features that cannot be reproduced in Prisma, yet, and, in individual cases, inefficiencies that still need to be eliminated.
• Once, the prototype has been advanced to an off-the-shelf product it can be used by anyone to implement dApps in a more natural way.

[Henry]

Hello @David , I found this paper interesting, Weldon job, I said so because I noticed that the key feature of dApps is that they can directly link application logic with transfer of monetary assets. This enables a wide range of correctness/security-sensitive business applications, e.g., for cryptocurrencies, crowdfunding, and public offerings, and make them, at the same time, an attractive target for attackers. I believe that these problem demand programming models that can ensure the correctness and security of dApps by-design, especially given the fact that contract code cannot be updated after deployment. I think before contract and clients are implemented in different languages, firstly, developers have to master the two technology stacks. The dominating approach in industry uses Solidity for the contract and JavaScript for clients.

I see that the reason the author proposed Prisma as the first language that features a global programming model for Ethereum dApps is because the global model has not been explored for dApp programming and it is quite unfortunate. One good thing about Prisma is that it enables interleaving contract and client logic within the same program and then adopts a direct style (DS) notation for encoding send-and-receive operations which is akin to languages with baked-in support for asynchronous interactions.

Honestly, I see Prisma as a God sent that came to relieve the developer from the responsibility of correctly managing distributed, asynchronous program flows and the heterogeneous technology stack. Instead, the burden is put on the compiler, which distributes the program flow by means of selective. I believe that One important part of our compiler is CPS translation. Another one good feature of Prisma is that it is embedded into Scala as a host language. Prisma’s features are implemented as a source-to-source macro that transforms Scala code to Scala code. But in Solidity, developers manually check whether flow control is needed and, if so, may derive the state from existing contract variables to avoid a state variable if possible.

I think client developers need to encode byte arrays using hexadecimal string representations starting with “0x”, otherwise they cannot be interpreted by the contract. So using one language for both the contract and the clients naturally enables static type safety of values that cross the contract–client boundary, to be honest, non-compromised client cannot provide inconsistent input, e.g., with wrong number of parameters or falsely encoded types.

It is important to note that in a setting with different language stacks, it is not possible to statically detect type mismatches in the client–contract interaction; e.g.„ Solidity has a type byte for byte arrays, which does not exist in JavaScript (commonly used to implement clients of a Solidity contract). My thoughts at the moment.