[06-16] Deductive Verification of Smart Contracts

文章来源:  |  发布时间:2021-06-10  |  【打印】 【关闭

Title:   Deductive Verification of Smart Contracts
Speaker: Dr. Ximeng Li (李希萌), Capital Normal University
Time:  10:30am, June 16th (Wednesday), 2021
Venue: 中科院软件园区5号楼334房间,计算机科学国家重点实验室报告厅


A blockchain is a distributed, replicated series of data records. It helps enforce the trust relationship between the parties who generate, and agree on, the on-chain data. Usually, programs called smart contracts can be written to define the business logics of the parties for producing new agreed-on data from existing data. Flaws in the design of blockchain protocols and programs (e.g., smart contracts) could lead to hijacked multi-party agreement on results favored by an attacker. In particular, if monetary data are affected, substantial economic loss could be resulted. In this talk, I introduce the basics of blockchains and smart contracts, and briefly outline the challenges in getting things right in their design and implementation. I then present some recent developments on the formal, deductive verification of smart contracts targeting the intermediate and high level smart contract languages. The concrete developments to be presented include a program logic for the formal verification of atomicity requirements for smart contracts at the source-level, and efforts in the formal verification of smart contracts expressed in the Ethereum intermediate language Yul.