Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
Michael Coblenz Jonathan Aldrich Joshua Sunshine Brad A. Myers
cs.SE cs.PL D.3; D.2.3









An Empirical Study of Obsidian]Can Advanced Type Systems Be Usable? An Empirical Study of
Ownership, Assets, and Typestate in Obsidian








0000-0002-9369-4069             

  Doctoral Candidate
  Computer Science Department              
  Carnegie Mellon University            
  5000 Forbes Ave.
  Pittsburgh
  PA
  15213
  USA                    

mcoblenz@cs.cmu.edu          




                                        
0000-0003-0631-5591             

  Professor
  Institute for Software Research              
  Carnegie Mellon University            
  5000 Forbes Ave.
  Pittsburgh
  PA
  15213
  USA                    

jonathan.aldrich@cs.cmu.edu          



                                        
0000-0002-4769-0219             

  Professor
  Human-Computer Interaction Institute              
  Carnegie Mellon University            
  5000 Forbes Ave.
  Pittsburgh
  PA
  15213
  USA                    

bam@cs.cmu.edu          





                                        
0000-0002-9672-5297             

  Systems Scientist
  Institute for Software Research              
  Carnegie Mellon University            
  5000 Forbes Ave.
  Pittsburgh
  PA
  15213
  USA                    

joshua.sunshine@cs.cmu.edu          















Some blockchain programs (smart contracts) have included serious security vulnerabilities. Obsidian is a new typestate-oriented programming language that uses a strong type system to rule out some of these vulnerabilities. Although Obsidian was designed to promote usability to make it as easy as possible to write programs, strong type systems can cause a language to be difficult to use. In particular, ownership, typestate, and assets, which Obsidian uses to provide safety guarantees, have not seen broad adoption together in popular languages and result in significant usability challenges. We performed an empirical study with 20 participants comparing Obsidian to Solidity, which is the language most commonly used for writing smart contracts today. We observed that Obsidian participants were able to successfully complete more of the programming tasks than the Solidity participants. We also found that the Solidity participants commonly inserted asset-related bugs, which Obsidian detects at compile time.





<ccs2012>
<concept>
<concept_id>10011007.10011006.10011008.10011024</concept_id>
<concept_desc>Software and its engineering Language features</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011050.10011017</concept_id>
<concept_desc>Software and its engineering Domain specific languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10002978.10003022</concept_id>
<concept_desc>Security and privacy Software and application security</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10003120.10003121.10011748</concept_id>
<concept_desc>Human-centered computing Empirical studies in HCI</concept_desc>
<concept_significance>300</concept_significance>
</concept>
</ccs2012>


[500]Software and its engineering Language features
[500]Software and its engineering Domain specific languages
[300]Security and privacy Software and application security
[300]Human-centered computing Empirical studies in HCI










[
    Joshua Sunshine
    December 30, 2023
=====================





§ INTRODUCTION




Obsidian <cit.> is a new programming language for writing smart contracts <cit.>, which are programs for blockchain platforms. Blockchains aim to provide a trusted computing medium among users who have not necessarily established trust. By decentralizing computation, system designers can obtain strong security properties. Unfortunately, these properties can only be obtained when the smart contracts themselves implement the intended behavior. Through bugs and security vulnerabilities in blockchains, attackers have stolen millions of dollars worth of cryptocurrencies <cit.>.


To improve safety and prevent vulnerabilities, researchers have developed new languages with stronger safety properties. In this work, we focus on Obsidian, which stands for Overhauling Blockchains with States to Improve Development of Interactive Application Notation. Obsidian was based on a requirements analysis for smart contract tools <cit.> to provide safety properties that would be relevant to many blockchain applications. In addition, Obsidian was designed to be usable through iterative user testing with 44 participants <cit.> so that programmers would be able to use it effectively. In prior work, we showed that most of the participants in a six-participant qualitative study were able to complete relevant programming tasks <cit.>. However, that small study did not compare Obsidian to any other languages. 

Ours is the first quantitative user study (of which we are aware) of a type system that supports linear types, ownership, or typestate, or any combination of these together. Earlier formative studies of Obsidian isolated particular language features, sometimes by adapting those features in the context of a language with which participants were already familiar. In contrast, in this summative study we studied the full Obsidian language, including the compiler and editor. Our study compares Obsidian to the most widely-used language for writing smart contracts,  Solidity <cit.>.

Although Solidity and Obsidian target different blockchain platforms (Ethereum <cit.> and Hyperledger Fabric <cit.>, respectively), we chose Solidity for comparison because it is the dominant programming language used in public smart contract development and because it is the language that was used to develop popular smart contracts that had serious security vulnerabilities <cit.>.





Considering Obsidian's design goal to improve safety with a novel type system, we identified three high-level research questions for our study:


    
  RQ1: Could we obtain actionable data about the usability of a novel programming language (that uses a type system that would be unfamiliar to our participants) in a short-duration user study (less than one day), which would be representative of real-world smart contract development?
    
  RQ2: Do programmers using Solidity insert more of the kinds of bugs that Obsidian is designed to catch?
    
  RQ3: Strong type systems can impose a usability burden on programmers because the compiler forces programmers to write code so that the compiler can verify various safety properties. Can programmers who were previously familiar with object-oriented programming (but not with Obsidian, typestate, ownership, or linear type systems in general) successfully use Obsidian to complete relevant smart contract programming tasks? If so, is there a significant impact on task completion times?


In RQ1, actionable data refers to data that inform programming language designers about their designs in ways that have implications on language design or language training. We used these three research questions to develop task criteria (<ref>). Then, we developed three tasks according to the criteria: Auction (<ref>), Prescription (<ref>), and Casino (<ref>). In each task, we refined these high-level research questions into task-relevant ones.

In summary, after the training period (about 90 minutes), seven of the ten Obsidian participants were able to successfully use Obsidian to finish implementing the required small program in our Auction task. In contrast, only two of the ten Solidity participants finished the task correctly. In the Prescription task, seven of the ten Obsidian participants were able to fix a security vulnerability in the program, whereas only two of the ten Solidity participants were able to do so. Six of the Obsidian participants used ownership to do the task, suggesting that ownership is teachable in a relatively short training period.

Five of the Obsidian participants had enough time remaining to do the Casino task (meaning that the other participants felt that their solutions were incomplete when their four-hour time expired). Although four of these wrote solutions that compiled, all four abused the disown operator, resulting in asset loss. Among the eight Solidity participants who had enough time for this task, half inserted bugs that resulted in improper asset fabrication or loss, showing that it is still important to pursue approaches to prevent asset abuse. Only one participant, who was in the Solidity condition, finished the task correctly.


After the tasks had ended, we gave participants a post-study survey asking for their opinions about the language they had used. We found that Obsidian participants felt that ownership was useful. They also observed that the tutorial and exercises were effective tools for learning the language.

We come to three conclusions in this paper. First, the methodology we used, in which we include practice-based training in a traditional quantitative study, is effective for evaluating a novel programming language. Second, despite the strong, unfamiliar restrictions it imposes, Obsidian's ownership and permissions system can be taught to some kinds of programmers in a short period of time in a way that results in many of them being able to use it effectively. That is, for some tasks, Obsidian enables people to be more successful at writing code that is free of the serious bugs that Obsidian detects. Third, without using techniques to detect or prevent asset-loss bugs, when doing some kinds of smart contract programming tasks, programmers will accidentally insert these kinds of bugs.




§ THE OBSIDIAN LANGUAGE

Obsidian uses ownership to express in the type system that each asset (an object that has value and therefore should not be lost) has exactly one owning reference. Ownership represents a form of linear types <cit.>. Ownership may be transferred between references, but if the owning reference goes out of scope, then the compiler reports an error. This ensures that owning references to assets cannot be lost unless they are explicitly disowned by the programmer. This design was motivated by <cit.>, who found in a user study that programmers of smart contracts inserted bugs that lost assets.

Obsidian extends ownership with typestate <cit.> because blockchain programs are typically stateful with objects supporting different operations depending on their state <cit.>. Thus, owning references can also specify what state the referenced object is in. For example, Auction@Open is the type of a reference to an Auction object that is in state Open. Because only owning references can specify typestate in Obsidian, ownership is implied by the presence of a typestate specification. Alternatively, Auction@Owned is the type of an owned reference to an Auction object, which may be in any state. Ownership is one example of linear types <cit.>: types that are consumed when used rather than being duplicated, and which must be consumed rather than merely dropped.

To improve flexibility, Obsidian also allows Shared references, which can refer to an object that has no owner, and Unowned references, which refer to an object that may have an owner. These additional options allow users to avoid establishing ownership structures when none are needed. Unlike Owned and Shared references, Unowned references cannot be used to change which of the various named states the object is in. This is required for soundness, since a change in state through an Unowned reference might violate a typestate specification on the owning reference. These annotations (Owned, Shared, and Unowned) are referred to as permissions because they denote what operations can be done via references with those annotations.

Obsidian is a class-based object-oriented language that uses a syntax similar to Java. Obsidian uses the keyword contract instead of class due to conventions of blockchain platforms, and calls methods transactions because invocations of blockchain code from outside the blockchain have transactional semantics: either the execution finishes successfully and new state is stored in the blockchain, or the transaction is reverted and any state changes are not preserved. Currently, Obsidian supports the Hyperledger Fabric blockchain platform <cit.>.

We provided a full description and formal treatment of Obsidian <cit.>; here, we explain Obsidian by example. The left column of <ref> shows part of an Auction contract. An Auction instance is always in one of three states: Open, BidsMade, or Closed. A field, seller, is always in scope, but when the object is in state BidsMade, fields maxBidder and maxBid are also in scope. Transactions specify types for their parameters, but in addition to the normal parameters, when this is specified as the first parameter, the program can specify a type for the this reference. The bid transaction, for example, can only be invoked via a Shared reference to the receiver. Formal parameters use >> to denote changes in permission or state. For example, the money parameter of bid is specified with permission Owned >> Unowned, meaning that the caller must pass an Owned reference, and when bid returns, from the perspective of the caller, the money is now Unowned. In other words, ownership was passed from the caller to the transaction.

