Formal verification is the act of proving or disproving a specified algorithm.
What makes a good specification?
- It should accurately capture the intent of the developer
- It should also encode all of the assumptions of the smart contract
- This is much easier said than done
- It should be easy to understand & should follow a standard
- It should put the contract in the scope of a bigger picture
- However, any specification is better than no specification!
- As long as it can be tested, regardless of mathematical or abstract basis, it is advantageous
Verifying hardware vs. smart contracts/blockchains
- Smart contracts are bounded by their execution times & are generally very simple
- There is great demand from users for this technology
- There is an opportunity to set standards for software
- Ethereum, for example, has non-deterministic specification, a huge improvement
Challenges of formal verification
- Interactive theorem proving is not user-friendly
- Smart contracts are difficult to prove-- they must be represented in a mathematical model first
- Most companies don't have people with the strong backgrounds required to do this
- There's a wide range of correctness techniques possible: formal, semi-formal & informal
- The context matters for what technique may be best
- Formal verification is super expensive & still not a total guarantee
How can we develop tools/approaches that are accessible to users?
- Logical formulas are reasonable for users to understand
- Alternatively, tools which require the user to just copy & paste without deep understanding are a possibility
- Sufficiently motivated developers are needed to improve these tools
- It is also useful to take these approaches out of academia-- more broad participation can increase accessibility
How can formal verification become mainstream?
- It is still the user's responsibility to understand the contract they are interacting with
- A bottom-up push from users being selective will incentivize rigorous development
- Developers need to respond & enable them
Role of auditors
- Auditors should inform the team of what may be useful & available
- However, it is the team's responsibility to follow up on this themselves
- They should complain more about the tools!
Challenges of verifying most complex contracts
- The more complicated, the more experimental your contract will be
- New specifications must be written instead of reusing old building blocks
- It is crucial to find all of the vulnerabilities