Nothing Special   »   [go: up one dir, main page]

skip to main content
research-article
Open access

Can advanced type systems be usable? An empirical study of ownership, assets, and typestate in Obsidian

Published: 13 November 2020 Publication History

Abstract

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.

Supplementary Material

Auxiliary Presentation Video (oopsla20main-p23-p-video.mp4)
This is a presentation video for our OOPSLA 2020 paper, "Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian." Some blockchain programs (smart contracts) have included serious security vulnerabilities. Obsidian is a new programming language that uses a strong type system to rule out some of these vulnerabilities. Ownership, typestate, and assets, which Obsidian uses to provide safety guarantees at compile time, have not seen broad adoption together in popular languages and may result in signifcant usability challenges. We performed an empirical study with 20 participants comparing Obsidian to Solidity, the language most commonly used for writing smart contracts today. Obsidian participants were able to successfully complete more of the programming tasks than the Solidity participants. We also found that asset-related bugs, which Obsidian detects at compile time, were commonly accidentally inserted by the Solidity participants.

References

[1]
Yasemin Acar, Christian Stransky, Dominik Wermke, Michelle L Mazurek, and Sascha Fahl. 2017. Security developer studies with GitHub users: Exploring a convenience sample. In Proceedings of the Thirteenth USENIX Conference on Usable Privacy and Security. 81-95.
[2]
Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. 2009. Typestate-oriented Programming. In Companion of Object Oriented Programming Systems, Languages, and Applications (OOPSLA '09). 1015-1022. https://doi.org/10.1145/ 1639950.1640073
[3]
Brett A. Becker, Paul Denny, Raymond Pettit, Durell Bouchard, Dennis J. Bouvier, Brian Harrington, Amir Kamil, Amey Karkare, Chris McDonald, Peter-Michael Osera, Janice L. Pearce, and James Prather. 2019. Compiler Error Messages Considered Unhelpful: The Landscape of Text-Based Programming Error Message Research. In Working Group Reports on Innovation and Technology in Computer Science Education (Aberdeen, Scotland Uk) (ITiCSE-WGR '19). 177-210. https://doi.org/10.1145/3344429.3372508
[4]
Kevin Bierhof and Jonathan Aldrich. 2007. Modular Typestate Checking of Aliased Objects. In Object-oriented programming systems, languages, and applications ( OOPSLA '07). 301-320. https://doi.org/10.1145/1297027.1297050
[5]
Luís Caires and Frank Pfenning. 2010. Session types as intuitionistic linear propositions. In International Conference on Concurrency Theory (CONCUR '10). https://doi.org/10.1007/978-3-642-15375-4_16
[6]
Michael Coblenz, Jonathan Aldrich, Brad Myers, and Joshua Sunshine. 2020a. Obsidian vs. Solidity RCT Replication Package. (8 2020 ). https://doi.org/10.1184/R1/12771074.v1
[7]
Michael Coblenz, Jonathan Aldrich, Brad A. Myers, and Joshua Sunshine. 2018. Interdisciplinary Programming Language Design. In Symposium on New Ideas, New Paradigms, and Refections on Programming and Software (Onward! '18). 133-146. https://doi.org/10.1145/3276954.3276965
[8]
Michael Coblenz, Gauri Kambhatla, Paulette Koronkevich, Jenna L. Wise, Celeste Barnaby, Joshua Sunshine, Jonathan Aldrich, and Brad A. Myers. 2019a. PLIERS: A Process that Integrates User-Centered Methods into Programming Language Design. arXiv: 1912.04719
[9]
Michael Coblenz, Whitney Nelson, Jonathan Aldrich, Brad Myers, and Joshua Sunshine. 2017. Glacier: Transitive Class Immutability for Java. In International Conference on Software Engineering (ICSE '17). IEEE Press, 496-506. https: //doi.org/10.1109/ICSE. 2017.52
[10]
Michael Coblenz, Reed Oei, Tyler Etzel, Paulette Koronkevich, Miles Baker, Yannick Bloem, Brad A. Myers, Joshua Sunshine, and Jonathan Aldrich. 2020b. Obsidian: Typestate and Assets for Safer Blockchain Programming. ACM Transactions on Programming Languages 42 ( 2020 ). Issue 3. https://doi.org/10.1145/3417516 To appear.
[11]
Michael Coblenz, Joshua Sunshine, Jonathan Aldrich, and Brad A. Myers. 2019b. Smarter Smart Contract Development Tools. 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain. https://doi.org/10.1109/ WETSEB. 2019.00013
[12]
J. Czerwonka, M. Greiler, and J. Tilford. 2015. Code Reviews Do Not Find Bugs. How the Current Code Review Best Practice Slows Us Down. In International Conference on Software Engineering (ICSE '15, Vol. 2 ). 27-28.
[13]
Ankush Das, Stephanie Balzer, Jan Hofmann, Frank Pfenning, and Ishani Santurkar. 2019. Resource-Aware Session Types for Digital Contracts. arXiv: 1902. 06056 [cs.PL]
[14]
Robert DeLine and Manuel Fähndrich. 2004. Typestates for Objects. In European Conference on Object-Oriented Programming (ECOOP '04). https://doi.org/10.1007/978-3-540-24851-4_21
[15]
Kevin Delmolino, Mitchell Arnett, Ahmed Kosba, Andrew Miller, and Elaine Shi. 2016. Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab. In International conference on fnancial cryptography and data security. https://doi.org/10.1007/978-3-662-53357-4_6
[16]
The Rust Project Developers. 2017. What is Ownership? ( 2017 ). Retrieved November 15, 2017 from https://doc.rustlang.org/book/second-edition/ch04-01-what-is-ownership.html
[17]
Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2002. More Dynamic Object Reclassifcation: Fickle II. ACM Trans. on Programming Languages and Systems 24, 2 (March 2002 ), 153-191. https://doi.org/10.1145/514952.514955
[18]
Ethereum Foundation. 2020a. Ethereum Project. Retrieved February 18, 2020 from http://www.ethereum.org
[19]
Ethereum Foundation. 2020b. Solidity. Retrieved February 18, 2020 from https://solidity.readthedocs.io/en/develop/
[20]
Ethereum Foundation. 2020c. State Machine. Retrieved February 18, 2020 from https://solidity.readthedocs. io/en/v0.4.24/ common-patterns.html#state-machine
[21]
Ethereum Foundation. 2020d. Withdrawal from Contracts. Retrieved February 25, 2020 from https://solidity.readthedocs. io/ en/v0.6. 3/common-patterns.html#withdrawal-from-contracts
[22]
Ethereum Foundation. 2020. Simple Open Auction. https://solidity.readthedocs. io/en/v0.6. 3/solidity-by-example.html#simpleopen-auction
[23]
Ronald Garcia, Éric Tanter, Roger Wolf, and Jonathan Aldrich. 2014. Foundations of Typestate-Oriented Programming. ACM Trans. on Programming Languages and Systems 36, 4, Article 12 (Oct 2014 ), 44 pages. https://doi.org/10.1145/2629609
[24]
Luke Graham. 2017. $32 million worth of digital currency ether stolen by hackers. CNBC. Retrieved November 2, 2017 from https://www.cnbc.com/ 2017 /07/20/32-million-worth-of-digital-currency-ether-stolen-by-hackers.html
[25]
Stefan Hanenberg, Sebastian Kleinschmager, Romain Robbes, Éric Tanter, and Andreas Stefk. 2014. An empirical study on the impact of static typing on software maintainability. Empirical Software Engineering 19, 5 (oct 2014 ), 1335-1382. https://doi.org/10.1007/s10664-013-9289-1
[26]
David J. Houston and Lilliard E. Richardson. 2007. Risk Compensation or Risk Reduction? Seatbelts, State Laws, and Trafc Fatalities. Social Science Quarterly 88, 4 ( 2007 ), 913-936. https://doi.org/10.1111/j.1540-6237. 2007. 00510.x
[27]
Kadena. 2019. PACT. https://pact.kadena.io
[28]
Erik Meijer and Peter Drayton. 2004. Static typing where possible, dynamic typing when needed: The end of the cold war between programming languages. In OOPSLA '04 Workshop on Revival of Dynamic Languages.
[29]
The University of Glasgow. 2001. System.IO.Unsafe. https://hackage.haskell. org/package/base-4.12.0.0/docs/System-IOUnsafe.html
[30]
John F. Pane, Brad A. Myers, and Leah B. Miller. 2002. Using HCI techniques to design a more usable programming system. In Human Centric Computing Languages and Environments (HCC '02). 198-206. https://doi.org/10.1109/HCC. 2002.1046372
[31]
Victor Pankratius and Ali-Reza Adl-Tabatabai. 2014. Software engineering with transactional memory versus locks in practice. Theory of Computing Systems 55, 3 ( 2014 ), 555-590. https://doi.org/10.1007/s00224-013-9452-5
[32]
Andrea Pinna, Simona Ibba, Gavina Baralla, Roberto Toonelli, and Michele Marchesi. 2019. A Massive Analysis of Ethereum Smart Contracts Empirical Study and Code Metrics. IEEE Access 7 ( 2019 ). https://doi.org/10.1109/ACCESS. 2019.2921936
[33]
Mozilla Research. 2015. The Rust Programming Language. Retrieved February 18, 2020 from https://www.rust-lang.org
[34]
Oracle Corp. 2019. Secure Coding Guidelines for the Java SE, version 4.0. Retrieved February 18, 2020 from https://www. oracle.com/technetwork/java/seccodeguide-139067.html
[35]
Chris Sadler and Barbara Ann Kitchenham. 1996. Evaluating Software Engineering Methods and Tool-Part 4: The Infuence of Human Factors. SIGSOFT Softw. Eng. Notes 21, 5 (Sept. 1996 ), 11-13. https://doi.org/10.1145/235969.235972
[36]
Franklin Schrans, Daniel Hails, Alexander Harkness, Sophia Drossopoulou, and Susan Eisenbach. 2019. Flint for Safer Smart Contracts. ( 2019 ). arXiv: 1904.06534
[37]
Robert C Seacord. 2013. Secure Coding in C and C++. Addison-Wesley Professional.
[38]
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao. 2019. Safer smart contract programming with Scilla. In Object-oriented Programming, Systems, Languages, and Applications (OOPSLA '19). https://doi.org/10.1145/3360611
[39]
Emin Gün Sirer. 2016. Thoughts on The DAO Hack. Hacking, Distributed. Retrieved February 18, 2020 from http://hackingdistributed.com/ 2016 /06/17/thoughts-on-the-dao-hack/
[40]
Stack Overfow. 2019. Developer Survey Results 2019. Retrieved February 18, 2020 from https://insights.stackoverfow.com/ survey/2019
[41]
Andreas Stefk and Stefan Hanenberg. 2014. The Programming Language Wars: Questions and Responsibilities for the Programming Language Community. In Symposium on New Ideas, New Paradigms, and Refections on Programming and Software (Portland, Oregon, USA) (Onward! 2014 ). 283-299. https://doi.org/10.1145/2661136.2661156
[42]
Andreas Stefk and Susanna Siebert. 2013. An empirical investigation into programming language syntax. ACM Transactions on Computing Education (TOCE) 13, 4 ( 2013 ), 19. https://doi.org/10.1145/2534973
[43]
Robert E. Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Engineering SE-12, 1 ( 1986 ), 157-171. https://doi.org/10.1109/TSE. 1986.6312929
[44]
Joshua Sunshine, James D. Herbsleb, and Jonathan Aldrich. 2014. Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming. In European Conference on Object-Oriented Programming (ECOOP '14). https://doi.org/10.1007/978-3-662-44202-9_7
[45]
Nick Szabo. 1997. Formalizing and Securing Relationships on Public Networks. First Monday 2, 9 ( 1997 ). https://doi.org/10. 5210/fm.v2i9. 548
[46]
The Linux Foundation. 2020a. Hyperledger. ( 2020 ). Retrieved February 18, 2020 from https://www.hyperledger.org
[47]
The Linux Foundation. 2020b. Hyperledger Fabric. Retrieved February 18, 2020 from https://www.hyperledger.org/projects/ fabric
[48]
Phillip Merlin Uesbeck, Andreas Stefk, Stefan Hanenberg, Jan Pedersen, and Patrick Daleiden. 2016. An Empirical Study on the Impact of C++ Lambdas and Programmer Experience. In International Conference on Software Engineering (Austin, Texas) ( ICSE '16). ACM, 760-771. https://doi.org/10.1145/2884781.2884849
[49]
Philip Wadler. 1990. Linear types can change the world. In Programming concepts and methods, Vol. 2. 347-359.
[50]
Serdar Yegulalp. 2018. Rust language is too hard to learn and use, says user survey. https://www.infoworld.com/article/ 3324488/rust-language-is-too-hard-to-learn-and-use-says-user-survey.html

Cited By

View all
  • (2023)How to Evaluate Blame for Gradual Types, Part 2Proceedings of the ACM on Programming Languages10.1145/36078367:ICFP(159-186)Online publication date: 31-Aug-2023
  • (2023)Usability-Oriented Design of Liquid Types for Java2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)10.1109/ICSE48619.2023.00132(1520-1532)Online publication date: May-2023
  • (2023)Pacta sunt servanda: Legal contracts inScience of Computer Programming10.1016/j.scico.2022.102911225(102911)Online publication date: Jan-2023
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 4, Issue OOPSLA
November 2020
3108 pages
EISSN:2475-1421
DOI:10.1145/3436718
Issue’s Table of Contents
This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 November 2020
Published in PACMPL Volume 4, Issue OOPSLA

Permissions

Request permissions for this article.

Check for updates

Badges

Author Tags

  1. assets
  2. blockchain
  3. empirical studies of programming languages
  4. linear types
  5. ownership
  6. permissions
  7. smart contracts
  8. typestate

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)239
  • Downloads (Last 6 weeks)39
Reflects downloads up to 01 Oct 2024

Other Metrics

Citations

Cited By

View all
  • (2023)How to Evaluate Blame for Gradual Types, Part 2Proceedings of the ACM on Programming Languages10.1145/36078367:ICFP(159-186)Online publication date: 31-Aug-2023
  • (2023)Usability-Oriented Design of Liquid Types for Java2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)10.1109/ICSE48619.2023.00132(1520-1532)Online publication date: May-2023
  • (2023)Pacta sunt servanda: Legal contracts inScience of Computer Programming10.1016/j.scico.2022.102911225(102911)Online publication date: Jan-2023
  • (2023)Liquidity analysis in resource-aware programmingJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100889135(100889)Online publication date: Oct-2023
  • (2022)From Legal Contracts to Legal Calculi: the code-driven normativityElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.368.2368(23-42)Online publication date: 6-Sep-2022
  • (2022)Liquidity Analysis in Resource-Aware ProgrammingFormal Aspects of Component Software10.1007/978-3-031-20872-0_12(205-221)Online publication date: 2-Nov-2022
  • (2022)Programming Legal ContractsThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_7(129-146)Online publication date: 4-Jul-2022
  • (2021)PLIERSACM Transactions on Computer-Human Interaction10.1145/345237928:4(1-53)Online publication date: Jul-2021
  • (2021)An Empirical Study of Solidity Language Features2021 IEEE 21st International Conference on Software Quality, Reliability and Security Companion (QRS-C)10.1109/QRS-C55045.2021.00105(698-707)Online publication date: Dec-2021
  • (2020)ObsidianACM Transactions on Programming Languages and Systems10.1145/341751642:3(1-82)Online publication date: 24-Nov-2020

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media