Formally Verifying Industry Cryptography(computer.org)
computer.org
Formally Verifying Industry Cryptography
https://www.computer.org/csdl/magazine/sp/2022/03/09733177/1BENJJewLKw
22 comments
It’s great to see that proving code correct is starting to make inroads into commercial software development. Perhaps the term “Software Engineer” should be reserved for software developers who have the training/skills to formally prove software correct? The same way that Engineers in other industries have the formal training/skills needed to use mathematical models to build/construct correctly?
As someone with years of experience writing machine-checked proofs in Coq, I cannot imagine the term "Software Engineer" shifting to that meaning, even though it may make sense when compared to other engineering disciplines. The programmers who have no experience with this technology outnumber us many thousands to one. They'd never sign off on it.
That said, I'm all for anything that results in more appreciation for mathematical rigor in programming. It's like puling teeth trying to get colleagues to use tools/languages that help with reasoning about code (even just a good type system), and for a lot of programmers math seems to be an unapproachable alien language.
One thing I'd like to change about the software industry is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program. The misconception there is that the all of the program's behavior needs to be specified in order for formal verification to be useful. Why can't gradual formal verification be a thing?
That said, I'm all for anything that results in more appreciation for mathematical rigor in programming. It's like puling teeth trying to get colleagues to use tools/languages that help with reasoning about code (even just a good type system), and for a lot of programmers math seems to be an unapproachable alien language.
One thing I'd like to change about the software industry is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program. The misconception there is that the all of the program's behavior needs to be specified in order for formal verification to be useful. Why can't gradual formal verification be a thing?
Our approach for cryptographic systems is pretty much gradual verification. We target high risk or worrisome systems and verify piece by piece. It works! Formal verification is a relatively expensive technique so it's necessary (in my opinion) to target the places where you can achieve the best bang for buck.
For system reliability at scale, I think that stronger type systems and systematic testing techniques are probably the best choice. Anyway, that puts the system in a much better state if you want to apply formal verification later.
For system reliability at scale, I think that stronger type systems and systematic testing techniques are probably the best choice. Anyway, that puts the system in a much better state if you want to apply formal verification later.
and for a lot of programmers math seems to be an unapproachable alien language
is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program
I think the main problem is that it's too formal. Turning something that is really about simple logical deduction into thick abstract maths is sure to dissuade the majority of the people who might find it useful. The elitist gatekeeping attitude that cryptographers tend to have doesn't help either.
is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program
I think the main problem is that it's too formal. Turning something that is really about simple logical deduction into thick abstract maths is sure to dissuade the majority of the people who might find it useful. The elitist gatekeeping attitude that cryptographers tend to have doesn't help either.
A problem here is that it's not a simple logical deduction being converted to "thick abstract math". The math is the proof. A formal proof is necessary to verify the deduction.
I wholly agree it’s important to contextualize formal methods — and particularly in terms of levels of rigor. Typing your program is already basic formal methods, and we do ourselves a disservice by using language which places proofs outside the realm of typing, testing, etc.
I think the “middle ground” between things like typing and things like fully specified programs are things like CDK apps which hook IAM policy or network reachability tools to analyze your infrastructure (and, eg, exclude open ports on the backend).
Which is slowly happening, eg AWS or Prime Video.
https://aws.amazon.com/security/provable-security/
I think the “middle ground” between things like typing and things like fully specified programs are things like CDK apps which hook IAM policy or network reachability tools to analyze your infrastructure (and, eg, exclude open ports on the backend).
Which is slowly happening, eg AWS or Prime Video.
https://aws.amazon.com/security/provable-security/
I love math and a good type system. I know little about formal verification of code. Are there tools (ideally) or languages (for educational, if not production, use) you recommend I look at?
I went through Benjamin Pierce et. al - Logical Foundations [0] which uses Coq. It was great fun, and I am someone who has a pattern of shying away from mathematics a little too often. That said, I'm not the right person to tell you why and when Coq > all other proof systems. Pierce is famous though, and so are his books.
[0] https://softwarefoundations.cis.upenn.edu/
[0] https://softwarefoundations.cis.upenn.edu/
Can you elaborate a bit more on the kind of projects you have used Coq (and other tools) to prove correct? I am very much interested in moving in that direction career wise.
Some companies are using the title "Proof Engineer" to mean Software Developers that specialize in proving code/hardware correct. I think that's a great choice.
>Perhaps the term “Software Engineer” should be reserved for software developers who have the training/skills to formally prove software correct?
If I remember correctly my university used to offer a "software engineering" degree, which was a real engineering degree (in the sense you could take the professional engineer exam at the end of it) and had a number of common courses with the software development degree - the focus being on system engineering, low-level programming for embedded devices, and so on. I believe it was a mix of software dev and mechatronics or electrical engineering (?) and was aimed at students who wanted to work in medical, aerospace, and similar safety-critical fields.
But I can't see it listed on the current course offerings and suspect it has been discontinued - I think it was pretty unpopular due to the requisite math courses and generally having the same level of rigour as the other engineering degrees.
If I remember correctly my university used to offer a "software engineering" degree, which was a real engineering degree (in the sense you could take the professional engineer exam at the end of it) and had a number of common courses with the software development degree - the focus being on system engineering, low-level programming for embedded devices, and so on. I believe it was a mix of software dev and mechatronics or electrical engineering (?) and was aimed at students who wanted to work in medical, aerospace, and similar safety-critical fields.
But I can't see it listed on the current course offerings and suspect it has been discontinued - I think it was pretty unpopular due to the requisite math courses and generally having the same level of rigour as the other engineering degrees.
My university had a "school of computer science and software engineering" which was a joint school of the engineering department and the maths department.
Although the degree was very much a Bsc, I don't think getting a Beng was an option.
Although the degree was very much a Bsc, I don't think getting a Beng was an option.
I'm the author of this article. I'd be happy to answer questions if anyone has them.
> The last five years have seen formal verification flourish in diverse industry niches
Do you see formal verification as a relatively promising niche to get into? If so, what areas (among theorem proving, model checking, static analysis, type & effect systems, etc)?
Do you see formal verification as a relatively promising niche to get into? If so, what areas (among theorem proving, model checking, static analysis, type & effect systems, etc)?
Great question! Formal methods groups in industry are growing rapidly and popping up in surprising places. Amazon's group is probably the most famous, but I think pretty much every big tech company has something going on in the formal verification / static analysis space. There's also a lot going on in blockchain. It's definitely becoming harder to hire people with FM skills, so in that sense, I think it's a great space to get into.
The downside is that the space is quite fragmented and a lot of tools have a high skill bar. If I was starting out, I'd probably focus on static analysis (eg. Infer or something similar - https://github.com/facebook/infer) because those tools tend to be easier to learn, and they have the potential to scale to really big systems. In contrast, Coq is a fine tool, but most people learn it by going to grad school which isn't useful short term career advice.
There are lot of great interviews with practitioners on the Galois podcast, Building Better Systems - that might be a good place to start exploring: https://www.stitcher.com/show/building-better-systems
The downside is that the space is quite fragmented and a lot of tools have a high skill bar. If I was starting out, I'd probably focus on static analysis (eg. Infer or something similar - https://github.com/facebook/infer) because those tools tend to be easier to learn, and they have the potential to scale to really big systems. In contrast, Coq is a fine tool, but most people learn it by going to grad school which isn't useful short term career advice.
There are lot of great interviews with practitioners on the Galois podcast, Building Better Systems - that might be a good place to start exploring: https://www.stitcher.com/show/building-better-systems
Thanks for your reply. I must clarify I do have a theoretical background in formal methods (a research-oriented 2-year MSc in that topic).
When I graduated there were some interesting opportunities, but the field looked a bit too stale and I ended up moving into a slightly different research area (probabilistic model checking and probabilistic inference in general).
There is a lot of hype around theorem proving, particularly with dependent types. As you say static analysis (and model checking) might be a better bet due to scalability, unless transformer architectures get to the point where writing proofs can be done much faster? What do you think about more practical approaches such as Dafny?
When I graduated there were some interesting opportunities, but the field looked a bit too stale and I ended up moving into a slightly different research area (probabilistic model checking and probabilistic inference in general).
There is a lot of hype around theorem proving, particularly with dependent types. As you say static analysis (and model checking) might be a better bet due to scalability, unless transformer architectures get to the point where writing proofs can be done much faster? What do you think about more practical approaches such as Dafny?
I love Dafny - we've worked on it in the past in fact. Theorem proving is definitely something that's being applied in industry - our crypto verification project uses Coq in some places. There's definitely a lot of hype though, some of which seems a bit unrealistic to me. There's a long, long way to go before theorem proving is practical as a tool for general programming, rather than in ultra-important niches like core crypto libraries.
I'm curious about resources that are specifically meant to help people who've learned one proof environment learn others.
I started learning a little bit of Lean from the Natural Number Game, and subsequently worked through Logical Foundations (with the generous help of one of the coauthors!), and have continued learning Coq afterward.
Are there books or sites or exercises out there for "people who've already learned Isabelle and now would like to learn Coq", "people who've already learned Coq and now would like to learn Lean", "people who've already learned Coq and now would like to learn tools and frameworks for verifying protocols", "people who've learned OCaml or Haskell and now would like to learn Coq", etc.?
I started learning a little bit of Lean from the Natural Number Game, and subsequently worked through Logical Foundations (with the generous help of one of the coauthors!), and have continued learning Coq afterward.
Are there books or sites or exercises out there for "people who've already learned Isabelle and now would like to learn Coq", "people who've already learned Coq and now would like to learn Lean", "people who've already learned Coq and now would like to learn tools and frameworks for verifying protocols", "people who've learned OCaml or Haskell and now would like to learn Coq", etc.?
Have you tried Idris? It is a "practical" programming language that also gives you the full power of Dependent Types to prove your code correct. There is a great book "Type-Driven Development with Idris" that really helped me open my mind to the power of Dependent Types.
Yes, I'm borrowing that specific book from a friend who is really into functional programming, but I haven't read it.
It does look like Idris helps make it especially straightforward to write correct code and know when you've done so.
It does look like Idris helps make it especially straightforward to write correct code and know when you've done so.
I highly recommend the programming language Idris and the book "Type-Driven Development with Idris" if you want a more "practical" introduction to proving code correct. It is a great read and every chapter pretty much blew my mind :)
The cryptol-course [1] is also a good, practical introduction to the system discussed in this paper.
[1] https://github.com/weaversa/cryptol-course
[1] https://github.com/weaversa/cryptol-course