Automated Smart Contract Synthesis and Verification for Distributed Ledger Blockchain Technology

比特币!Ethereum !区块链!Crypto-economics !在过去的一年里，这些词成为了全球的头条新闻。基于分布式账本的技术（DLT）——也被称为“价值互联网”——的前景震惊了世界，并引发了人们对技术的兴奋，上一次出现这种兴奋是在上世纪90年代，当时互联网正进入主流。完全去中心化治理的广泛采用和潜在的技术理念有望撼动商业、金融和隐私/安全等领域。从2016年以来的投资流入（超过任何其他科技行业）来看，它有望在全球范围内重新定义社会的社会经济结构。这些技术的发展几乎完全发生在主流技术领域之外，由自称为“密码朋克”的个人推动。大学和他们的研究人员在很大程度上是旁观者。这是一个令人担忧的问题。因此，至关重要的是，这些创新必须基于能够实现善治和社会进步的可靠技术原则。DLT的一个主要优势是分布式部署称为智能合约的软件，它提供了一系列全新的机会。例如，它允许去中心化商业、去中心化证券交易、去中心化金融衍生品证券、全自动供应链管理或艺术家产权的自动执行和转让。由于在区块链上注册的数百万美元的资产或房地产契约由该软件处理，攻击或操纵它变得有利可图，正如最近的DAO和Parity钱包攻击在过去两年中已经证明的那样，由于智能合约软件的错误（bug），损失了超过2.5亿美元。该项目旨在通过以下方式弥合这一差距：(a)开发一种新颖的编程语言，该语言包含有效编写智能合约所需的最常见操作；(b)为该语言建立一个全面的验证环境，以协助初级软件工程师检查其正确性；(c)开发一个基于模板的自动合成工具，用于智能合约生成“设计正确”的软件；(d)使用拟议的生态系统对去中心化的oracle进行沙盒处理（其目的是将现实生活中的信息输入到区块链上），以大规模展示研究的有效性和实用性。

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.