[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部。 更多信息访问李希萌的个人主页：https://iec.cnu.edu.cn/szdw/sssds/js3/152042.htm |