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.