By Grigore Rosu, Everett Hildenbrandt, Daejun Park, Shuvendu Lahiri
Testing shows the presence, not the absence of bugs” (Dijkstra, 1969). Although remarkable progress has been made in testing during the last 50 years, exhaustive testing is still infeasible in most cases and we have learned, sometimes the hard way, that the remaining bugs can have catastrophic consequences.
The nature of the blockchain, where code that accesses a shared state is public and can be invoked by anybody from anywhere, amplifies both the speed at which bugs are found by hackers and the consequences of their exploits. Testing is therefore simply insufficient here. Formal verification is the only known viable alternative.
This talk will explain what formal verification is in the context of blockchain smart contracts, tokens and protocols, why it is becoming increasingly critical, how it is done, and what tools are available. Several approaches are covered, from automated and light-weight that find bugs to interactive and comprehensive that analyze all the behaviors, from high-level source-code that developers write and understand to low-level bytecode that is executed by node clients.
This talk also aims to raise awareness that, contrary to common misunderstanding where formal verification is confused with code auditing, it takes significantly more effort to formally verify a program than to write the program first place. Think 9x more! Indeed, a rule of thumb at NASA is that 20% of a project’s budget goes into code writing and 80% goes into verification and validation; and NASA code is not public and nobody but NASA can invoke it once deployed.