Automated Smart Contract Synthesis and Verification for Distributed Ledger Blockchain Technology

比特币!以太坊区块链!加密经济学! 在过去的一年里，这些词成为了全球的头条新闻。基于分布式账本的技术（DLT）的承诺-也被称为“价值互联网”-已经使世界电气化，并为技术带来了兴奋，这是上世纪90年代互联网进入主流时最后一次看到的。完全去中心化治理的可能广泛采用和潜在的技术理念有望动摇商业、金融和隐私/安全等领域。从2016年以来的投资流入（超过任何其他技术领域）来看，它有望在全球范围内重新定义社会的社会经济结构。这些技术的发展几乎完全发生在主流技术领域之外，由自称"密码朋克"的个人推动。大学和他们的研究人员基本上都是旁观者。这是一个问题。因此，至关重要的是，这些创新都是基于健全的技术原则，使良好的治理和 * 社会进步。DLT的一个主要优势是称为智能合约的软件的分布式部署，这带来了一系列全新的机会。例如，它允许去中心化的商业、去中心化的证券交易、去中心化的金融衍生证券、全自动化的供应链管理或艺术家财产权的自动执行和转让。由于在 * 区块链上注册的数百万美元资产或真实的房地产契约由该软件处理，攻击或操纵它变得有利可图，正如最近的DAO和Parity钱包攻击在过去两年中已经证明的那样，由于智能合约软件的错误（错误），损失超过2.5亿美元。该项目旨在通过以下方式弥合这一差距：（a）开发一种新型编程语言，包括高效编码智能合约所需的最常见操作;（B）为这种语言构建一个全面的验证环境，以帮助检查正确性，即使是新手软件工程师的水平;（c）为智能合约开发基于模板的自动合成工具，生成"设计正确"的软件，以及使用所提出的生态系统来沙盒分散的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.