Name
Abstract | ||
|---|---|---|
Smart contracts are programs that run on a distributed ledger platform. They usually manage resources representing valuable\r\n assets. Moreover, their source code is visible to potential\r\n attackers, they are distributed, and bugs are hard to\r\n fix. Thus, they are susceptible to attacks exploiting programming errors.\r\n Their vulnerability makes a rigorous formal analysis of the functional\r\n correctness of smart contracts highly desirable.\r\n In this short paper, we show that the architecture of smart\r\n contract platforms offers a computation model for smart\r\n contracts that yields itself naturally to deductive program\r\n verification. We discuss different classes of correctness\r\n properties of distributed ledger applications, and show that\r\n design-by-contract verification tools are suitable to prove\r\n these properties. We present experiments where we apply the\r\n KeY verification tool to smart contracts in the Hyperledger\r\n Fabric framework which are implemented in Java and specified using the Java Modeling Language. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1007/978-3-030-54994-7_21 | FM Workshops (1) |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernhard Beckert | 1 | 862 | 86.50 |
| Jonas Schiffl | 2 | 0 | 1.35 |
| Mattias Ulbrich | 3 | 183 | 17.83 |