Thread by @EvanWeb3

Many people have posted great explanations of the Wormhole exploit. This is not another breakdown of the attack. Instead, let's talk about smart contract auditing vs. verification.
#Crypto #web3 #Wormhole #SmartContracts
1/x

By and large, smart contract developers are being responsible - following best security practices, using the best dev tools, and making sure their contracts are audited before deployment. But is trusting auditing as the last line of defense the right approach?
2/x

We all know how important it is to keep commits small since it's hard to reason about a large body of code. Auditors have to understand and probe the entire system. Given it's very much a human-in-the-loop process, it's not surprising auditing is a long and expensive process.
3/x

It must be frustrating for developers to deal with smart contract auditing. It adds an additional step to the development process. Developers are not in control of the deployment schedule. It's expensive and not a guarantee.
4/x

And auditing is fundamentally limiting the growth of the ecosystem. @Mysten_Labs' mission is to bring 10 million developers into web3. If they are all dependent on auditing, how many auditors are needed?! This is not scalable.
5/x

Can the process be automated? Not currently. It's not easy to build a fully statically analyzable programming language. Solidity has dynamic features that have been exploited repeatedly. Rust is a complex language. Verification tools exist. But they are not perfect.
6/x

We believe using math to prove contract correctness is the right path. It shifts the burden from a system-wide, human-in-the-loop, imprecise practice to a process that is 1) automated, 2) can be integrated into CI flow. So, what is the state of art today?
7/x

Imagine a flow where a smart contract developer carefully turn code comments into specifications in their program - local (function) / global (module) pre and post conditions, invariants, etc.
8/x

The formal verification tool would inform the developer whether the code is provably correct. And if it's not, it will spit out anti-examples to help the developer correct their code. This flow would significantly reduce the auditing overhead. Fewer exploits. More developers!
9/x

What if the specifications are wrong or absent? Ultimately developers must employ secure programming practices. There is a need for experts to help new developers write comprehensive specifications. The good thing is it fits perfectly in the incremental development process.
10/x

While at Novi Research, we spent a lot of energy designing the Move language and the Move prover. The co-design approach ensures the all the Move programs are formally verifiable. This will be a critical piece for everything @Mysten_Labs builds.
11/x

Take a look at the keynote by our esteemed colleague Prof. David Dill. Here is the paper www-cs.stanford.edu/~yoniz/cav20.p… if you want to learn more about the science.
/fin