We can't find the internet
Attempting to reconnect
Something went wrong!
Hang in there while we get back on track
"Formally Verifying Everybody's Cryptography" by Mike Dodds, Joey Dodds (Strange Loop 2022)
Formal verification expert Mike Dodds shares strategies for verifying cryptographic code, discussing the challenges of understanding complex software, the power of symbolic testing, and the benefits of proof composition and reuse.
- Formal verification needs to target software that is not easy to understand, making it challenging.
- To verify code, you need to get the right abstraction, write code that is easy to understand, and prove properties about the code.
- Proofs are about building trust in the security of software, and they can be used to verify cryptographic code.
- It’s difficult to verify code that is highly optimized and has many bugs, as it’s hard to understand how it works.
- Cryptographic code is particularly hard to verify because it is highly optimized and has a lot of subtle mathematical mistakes.
- The best way to verify code is to write good tests, especially symbolic testing, which can help catch bugs.
- Proofs can be composed together to verify larger pieces of software.
- Formal verification can be used to verify not just the code, but also the specifications of the code.
- The process of formal verification is complex and requires a deep understanding of the code and the specifications.
- The output of a proof is a mathematical model of the code’s behavior, which can be used to show that the code is secure.
- Proofs can be reused in different contexts, making them a valuable investment.
- The goal of formal verification is to build trust in the security of software, and it can be used to verify a wide range of software, from cryptographic code to industrial automation software.