Spotlight on Lablet Research #22 - Obsidian: A Language for Secure-by-Construction Blockchain Programs

Spotlight on Lablet Research #22 -

Obsidian: A Language for Secure-by-Construction Blockchain Programs

Lablet: Carnegie Mellon University

Blockchains have been proposed to support transactions on distributed, shared state, but hackers have exploited security vulnerabilities in existing programs. The CMU research team, which is led by Principal Investigator (PI) Jonathan Aldrich and Co-PI Brad Myers and includes participating Sub-Lablet George Mason University, applied user-centered design in the creation of Obsidian, a new language that uses typestate and linearity to support stronger safety guarantees than current approaches for programming blockchain systems.

Programming language designers commonly guess what language designs would be best for their users and create languages accordingly. The outcome of this is languages that are difficult to use and error-prone. In particular, blockchain programs have been plagued by serious bugs. Although techniques from the theory of programming languages can detect many of these kinds of bugs, languages that use these techniques have been too difficult for programmers to use effectively. Obsidian, which integrates a strong, static type system that detects many of these bugs, uses a new user-centered design approach. The team developed formative and summative methods for the user-centered design of programming languages and applied them to create Obsidian. This included a usability study, which demonstrated the effectiveness of the design methods to obtain a usable language. Obsidian addresses the opportunity of directly incorporating models that address the kinds of errors that can occur in distributed systems with shared state and transferable resources. Obsidian uses the technical approaches of typestate (expressing both the types of objects and their state in a way that supports static reasoning) and linearity (to avoid loss or duplication of tracked assets).

This project considers models for secure collaboration and contracts in a decentralized environment among parties that have not established trust. A significant example is blockchain programming, which requires high security but also, in implementations, demonstrates the often-dramatic consequences of defects.

The project research included both technical and usability assessments of these two ideas. The technical assessment addressed the feasibility of sound and composable static analyses to support these two semantic innovations. The usability assessment focused on the ability of programmers to use Obsidian effectively to write secure programs with little training. A combined assessment would focus on whether programmers are more likely to write correct, safe code with Obsidian than with Solidity, and with comparable or improved productivity.

Researchers performed an empirical study with 20 participants comparing Obsidian to Solidity, which is the language most commonly used for writing smart contracts today, and observed that most of the Obsidian participants were able to successfully complete most of the programming tasks given to them. The research team also found that asset-related bugs, which Obsidian detects at compile time, were commonly accidentally inserted by the Solidity participants. The team identified potential opportunities to improve the usability of typestate as well as to apply the usability benefits of Obsidian's ownership system to other languages.

Most distributed payment schemes (cryptocurrencies) suffer from a lack of privacy and anonymity for their users due to the public nature of their ledger. The research team developed MiniLedger, a permissioned, distributed payment system that not only guarantees the privacy of transactions but also offers built-in functionalities for various types of audits by any external authority (i.e., audits on transaction values or of total assets of participants). As a starting point, they used the recently proposed zkLedger architecture, defined system functionalities and security properties, and addressed vulnerabilities and shortcomings identified in zkLedger. Most importantly, MiniLedger is the first private and accountable payment system with nearly constant storage costs. To achieve such a storage improvement, researchers implemented pruning functionalities for the transaction history without hurting security or auditing, while they extended MiniLedger to perform fine-grained audits at a client level. Evaluation of the results showed that MiniLedger is not only practical in terms of storage, but also has minimal computational overhead compared to zkLedger, as the pruning-related functionalities can be tailored for maximum efficiency on each deployment use-case.

The team also developed a new approach for detecting injection vulnerabilities in applications by harnessing the combined power of both human developers' test suites and automated dynamic analysis. Their new approach, RIVULET, monitors the execution of developer-written functional tests in order to detect information flows that may be vulnerable to attack. Then, RIVULET uses a white-box test generation technique to repurpose those functional tests to check if any vulnerable flow could be exploited. When applied to the version of Apache Struts exploited in the 2017 Equifax attack, RIVULET quickly identified the vulnerability, leveraging only the tests that existed in Struts at that time. The researchers compared RIVULET to the state-of-the-art static vulnerability detector Julia on benchmarks, finding that RIVULET outperformed Julia in both false positives and false negatives. They also used RIVULET to detect previously unknown vulnerabilities.

The team adapted HCI methods to make them more suitable for programming language design and integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. They evaluated PLIERS by using it to design two new programming languages. Glacier extends Java to enable programmers to express immutability properties effectively and easily. Obsidian is a language for blockchains that includes verification of critical safety properties. Summative usability studies showed that programmers were able to program effectively in both languages after short training periods.

In describing two case studies that evaluate Obsidian's applicability to the domains of parametric insurance and supply chain management, they found that Obsidian's type system facilitates reasoning about high-level states and ownership of resources. They compared their Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.

Background on this project can be found here.