Formal Verification of Smart Contracts: Short Paper
| Autor: | Karthikeyan Bhargavan, Georges Gonthier, Nadim Kobeissi, Cédric Fournet, Antoine Delignat-Lavaud, Thomas Sibut-Pinote, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Anitha Gollamudi, Natalia Kulatova |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Microsoft Research, Harvard University, Symbolic Special Functions : Fast and Certified (SPECFUN), Inria Saclay - Ile de France, Inria de Paris, Harvard University [Cambridge], Programming securely with cryptography (PROSECCO ) |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Functional programming
Cryptocurrency Cryptocurrencies Correctness Semantics (computer science) Computer science 020207 software engineering 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] computer.software_genre Computer security Stack machine Bytecode Formal verification [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Virtual machine Formal methods Computer science 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing computer |
| Zdroj: | Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security ACM Workshop on Programming Languages and Analysis for Security ACM Workshop on Programming Languages and Analysis for Security, Oct 2016, Vienna, Austria. ⟨10.1145/2993600.2993611⟩ PLAS@CCS |
| DOI: | 10.1145/2993600.2993611⟩ |
| Popis: | International audience; Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM code; instead, they can program in a JavaScript-like language, called Solidity, that compiles to bytecode. Since the main purpose of EVM is to execute smart contracts that manage and transfer digital assets (called Ether), security is of paramount importance. However, writing secure smart contracts can be extremely difficult: due to the openness of Ethereum, both programs and pseudonymous users can call into the public methods of other programs, leading to potentially dangerous compositions of trusted and untrusted code. This risk was recently illustrated by an attack on TheDAO contract that exploited subtle details of the EVM semantics to transfer roughly $50M worth of Ether into the control of an attacker.In this paper, we outline a framework to analyze and verify both the runtime safety and the functional correctness of Ethereum contracts by translation to F*, a functional programming language aimed at program verification. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|