Translation Certification for Smart Contracts
Jacco O.G. Krijnen, Manuel M.T. Chakravarty, Gabriele Keller, Wouter, Swierstra

TL;DR
This paper introduces a formal translation certification framework for smart contracts, ensuring trust in compiled code by verifying source code possession and faithful compilation, implemented in Coq for a functional language.
Contribution
It presents a novel, modular translation certification framework for smart contracts, addressing both compiler correctness and source code possession verification.
Findings
Successfully modeled compilation as translation relations in Coq.
Framework is modular and adaptable to evolving compiler implementations.
Enhances trustworthiness of smart contract deployment on blockchains.
Abstract
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high financial value, in an adversarial environment and, once committed to the blockchain, they cannot be changed anymore. Smart contracts are typically developed in a high-level contract language and compiled to low-level virtual machine code before being committed to the blockchain. For a smart contract user to trust a given piece of low-level code on the blockchain, they must convince themselves that (a) they are in possession of the matching source code and (b) that the compiler faithfully translated the source code's semantics. Classic approaches to compiler correctness tackle the second point. We argue that translation certification also addresses…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Blockchain Technology Applications and Security · Cryptography and Data Security
