Reference. Obsidian: Typestate and Assets for Safer Blockchain Programming
Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts , which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. We integrated a permissions system that encodes a notion of ownership to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian’s applicability to the domains of parametric insurance and supply chain management, finding that Obsidian’s type system facilitates reasoning about high-level states and ownership of resources. We compared our 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.
Cite
Cited by (1)
PLIERS: A Process that Integrates User-Centered Methods into Programming Language Design coblenz-2021-pliers
Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: languages have high iteration costs, programmers require significant learning time, and user performance has high variance. To address these problems, we adapted both formative and summative HCI methods to make them more suitable for programming language design. We integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. We assessed 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. Empirical studies showed that the PLIERS process resulted in languages that could be used effectively by many programmers and revealed additional opportunities for language improvement.
Cites 70 works (2 here)
With notes (2)
PLIERS: A Process that Integrates User-Centered Methods into Programming Language Design coblenz-2021-pliers
Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: languages have high iteration costs, programmers require significant learning time, and user performance has high variance. To address these problems, we adapted both formative and summative HCI methods to make them more suitable for programming language design. We integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. We assessed 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. Empirical studies showed that the PLIERS process resulted in languages that could be used effectively by many programmers and revealed additional opportunities for language improvement.
Session Types as Intuitionistic Linear Propositions caires-2010-session
External (68)
- Can advanced type systems be usable? An empirical study of ownership, assets, and typestate in Obsidian (2020)
- MadMax: analyzing the out-of-gas world of smart contracts (2020)
- Obsidian (Encyclopaedia Britannica) (2020)
- Common Patterns (Solidity documentation) (2020)
- Smarter Smart Contract Development Tools (2019)
- IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain (2019)
- Safer smart contract programming with Scilla (2019)
- Flint for Safer Smart Contracts (2019)
- Slither: A Static Analysis Framework for Smart Contracts (2019)
- An Introduction to DAML (2019)
- Blockchain for supply chain (IBM) (2019)
- Introduce the Asset trait (Flint proposal) (2019)
- Empowering Business-Level Blockchain Users with a Rules Framework for Smart Contracts (2018)
- Interdisciplinary programming language design (2018)
- Making Sense of Blockchain Applications (2018)
- ZEUS: Analyzing Safety of Smart Contracts (2018)
- Towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity (2018)
- SMT-Based Verification of Solidity Smart Contracts (2018)
- Towards Safer Smart Contracts: A Survey of Languages and Verification Methods (2018)
- A Survey of Attacks on Ethereum Smart Contracts (SoK) (2017)
- Design and Implementation of Concurrent C0 (2017)
- A Taxonomy of Blockchain-Based Systems for Architecture Design (2017)
- A user study to inform the design of the Obsidian blockchain DSL (2017)
- Application of Blockchain Technology in the Manufacturing Industry (Dieterich et al., Medium) (2017)
- $32 million worth of digital currency ether stolen by hackers (2017)
- The Potential for Blockchain to Transform Electronic Health Records (2017)
- Formal Verification of Smart Contracts (2016)
- Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab (2016)
- Making Smart Contracts Smarter (2016)
- Programmers Are Users Too: Human-Centered Methods for Improving Programming Tools (2016)
- Analysis of the DAO exploit (2016)
- Towards a shared ledger business collaboration language based on data-aware processes (2016)
- Thoughts on The DAO Hack (2016)
- The Rust Programming Language (website) (2015)
- EIP 20: ERC-20 Token Standard (2015)
- Considering Productivity Effects of Explicit Type Declarations (2014)
- Foundations of Typestate-Oriented Programming (2014)
- The Programming Language Wars (2014)
- Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming (2014)
- Aliasing in Object-Oriented Programming. Types, Analysis and Verification (2013)
- An Empirical Investigation into Programming Language Syntax (2013)
- Uniqueness and reference immutability for safe parallelism (2012)
- A type system for borrowing permissions (2012)
- Checking Concurrent Typestate with Access Permissions in Plural: A Retrospective (2011)
- First-class state change in plaid (2011)
- Practical affine types (2011)
- An overview of the K semantic framework (2010)
- Typestate-oriented programming (2009)
- Practical API Protocol Checking with Access Permissions (2009)
- PLURAL: checking protocol compliance under aliasing (2008)
- Usability Implications of Requiring Parameters in Objects' Constructors (2007)
- Typestates for Objects (2004)
- Checking interference with fractional permissions (2003)
- Using HCI techniques to design a more usable programming system (2003)
- Agile Software Development: Principles, Patterns, and Practices (2003)
- More dynamic object reclassification (2002)
- Adoption and focus: practical linear types for imperative programming (2002)
- Capabilities for Sharing (2001)
- Featherweight Java (2001)
- Local type inference (2000)
- Ownership types for flexible alias protection (1998)
- A study of the fragile base class problem (1998)
- Formalizing and Securing Relationships on Public Networks (1997)
- Reasoning about programs in continuation-passing style (1992)
- Heuristic evaluation of user interfaces (1990)
- Linear types can change the world (1990)
- Typestate: A programming language concept for enhancing software reliability (1986)
- On optimistic methods for concurrency control (1981)