| Creators: |
Cumming, Daniel and Utting, Mark and Cassez, Franck and Dong, Naipeng and Tork, Sadra B. and Risius, Marten |
| Title: |
EVM-Vale: Formal Verification of EVM Bytecode using Vale |
| Item Type: |
Conference or Workshop Item |
| Event Title: |
(Proceedings of the) 7th Symposium on Distributed Ledger Technology (SDLT) |
| Event Location: |
Goldcoast, Australia |
| Event Dates: |
November 30 - December 1, 2023 |
| Projects: |
IDI |
| Page Range: |
pp. 39-54 |
| Additional Information: |
Distributed Ledger Technology / ed. by Dong, N. (u.a.) (Communications in Computer and Information Science ; 1975).- p.39-54 |
| Date: |
2023 |
| Divisions: |
Informationsmanagement |
| Abstract (ENG): |
We evaluate the use of the existing Microsoft Vale framework to guarantee correctness of low level Ethereum Virtual Machine (EVM) bytecode, while affording smart contract developers higher-level language and reasoning features. We encode EVM-R (a subset of EVM semantics and instruction set) into F*, and raise the EVM-R into Vale design-by-contract components in an intermediate language supporting conditional logic. The specifications of Vale procedures constructed from these verified EVM bytecodes carry integrity to the bytecode level, unlike current EVM compilers. Furthermore, raising the instruction set to Vale allows opportunity for refinement of the instructions, which we did ensuring safety properties of overflow protection, invalid memory access protection, and functional correctness. We demonstrate our contributions through two case study smart contracts, a simple casino, and a subcurrency coin. |
| Forthcoming: |
No |
| Language: |
English |
| Citation: |
Cumming, Daniel and Utting, Mark and Cassez, Franck and Dong, Naipeng and Tork, Sadra B. and Risius, Marten
(2023)
EVM-Vale: Formal Verification of EVM Bytecode using Vale.
In: (Proceedings of the) 7th Symposium on Distributed Ledger Technology (SDLT), November 30 - December 1, 2023, Goldcoast, Australia, pp. 39-54.
(Communications in Computer and Information Science; 1975).
ISBN 9789819700066
|
