Automated Smart Contract Synthesis and Verification for Distributed Ledger Blockchain Technology

点击翻译按钮获取中文摘要

Bitcoin! Ethereum! Blockchain! Crypto-economics! In the past year, these words made headline news*globally. The promise of Distributed Ledger-based Technologies (DLT) - also known as the "internet of value"- has electrified*the world and created an excitement for technology that was last seen in the 1990s*when the internet was entering mainstream. The possible widespread adoption and*underlying technological philosophy of fully decentralized governance promises*to shake up the worlds of commerce, finance, and privacy/security, among others. Judging from the investment inflows since 2016 (larger than any other technology sector), it promises redefine the*socioeconomic fabric of society at a global and drastic scale. The*development of these technologies occurred almost entirely occurred outside of the mainstream*tech sector advanced by individuals, self-declared “cypherpunks.”*Universities and their researchers have been largely at the sidelines. And*that's a concern. As such, it is critical that these innovations are based on sound technological principles that enable good governance and*societal progress. One major advantage of DLT is the distributed deployment of software called smart contracts which present a whole new set of opportunities. For example, it allows decentralized commerce, decentralized trading of securities, decentralized financial derivative securities, fully automated supply-chain management, or automatic enforcement and transfers of artists' property rights. As multi-million dollar assets or real estate deeds registered on a*blockchain are handled by this software, attacking or manipulating it becomes lucrative, as the recent DAO and Parity wallet attacks already demonstrated in the past two years with more than $250 million dollars lost due to errors (bugs) in smart contract software. This projects aims to bridge this gap by: (a) developing a novel programming language that comprises the most common operations needed to code smart contracts efficiently; (b) building a comprehensive verification environment for this language to assist checking correctness even at the level of a novice software engineer; (c) developing a template-based automated synthesis tool for smart contracts generating software that is "correct by design" and (d) using the proposed ecosystem to sandbox a decentralized oracle (whose purpose is to input real life information onto the blockchain) so as to demonstrate the efficacy and practicality of the research on a large scale.