Sökning: id:"swepub:oai:research.chalmers.se:c14ae2f8-6a9c-4552-8fb1-9ac712a4d656" >
Short Paper: Blockc...
Short Paper: Blockcheck the Typechain
-
- Benitez, Sergio (författare)
- Stanford University
-
- Cogan, Jonathan (författare)
- Stanford University
-
- Russo, Alejandro, 1978 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- 2020-11-09
- 2020
- Engelska.
-
Ingår i: PLAS 2020 - Proceedings of the 15th Workshop on Programming Languages and Analysis for Security. - New York, NY, USA : ACM. ; 13 November 2020, s. 35-39
- Relaterad länk:
-
https://research.cha... (primary) (free)
-
visa fler...
-
https://research.cha...
-
https://research.cha...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- Recent efforts have sought to design new smart contract programming languages that make writing blockchain programs safer. But programs on the blockchain are beholden only to the safety properties enforced by the blockchain itself: even the strictest language-only properties can be rendered moot on a language-oblivious blockchain due to inter-contract interactions. Consequently, while safer languages are a necessity, fully realizing their benefits necessitates a language-aware redesign of the blockchain itself. To this end, we propose that the blockchain be viewed as a typechain: a chain of typed programs-not arbitrary blocks-that are included iff they typecheck against the existing chain. Reaching consensus, or blockchecking, validates typechecking in a byzantine fault-tolerant manner. Safety properties traditionally enforced by a runtime are instead enforced by a type system with the aim of statically capturing smart contract correctness. To provide a robust level of safety, we contend that a typechain must minimally guarantee (1) asset linearity and liveness, (2) physical resource availability, including CPU and memory, (3) exceptionless execution, or no early termination, (4) protocol conformance, or adherence to some state machine, and (5) inter-contract safety, including reentrancy safety. Despite their exacting nature, typechains are extensible, allowing for rich libraries that extend the set of verified properties. We expand on typechain properties and present examples of real-world bugs they prevent.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Språkteknologi (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Language Technology (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Nyckelord
- digital currency
- compiler
- smart contract
- programming language
- type system
- blockchain
- typechain
- safety
- security
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)