[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|
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.