[06-16] Deductive Verification of Smart Contracts

Title: Deductive Verification of Smart Contracts
Speaker: Dr. Ximeng Li (李希萌), Capital Normal University
Time: 10:30am, June 16th (Wednesday), 2021
Venue: 中科院软件园区5号楼334房间,计算机科学国家重点实验室报告厅
Abstract: 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.
Bio: 李希萌,首都师范大学讲师,硕士生导师。研究兴趣为形式化验证,目前主要关注区块链程序和架构的形式化建模和定理证明。于2010年至2018年初在丹麦技术大学获得硕士、博士学位,并先后在丹麦、德国开展博士后研究工作,主要研究方向为程序的信息流安全验证。曾参加欧盟和德国科研项目2项,其中包括与空中客车公司的合作研发项目。现主持国家自然科学基金青年项目1项、北京市教委科技计划一般项目1项。在形式化方法和信息安全领域重要期刊和国际会议发表论文十余篇,合著专著1部。