Formally Verifying Industry Cryptography

https://www.computer.org/csdl/magazine/sp/2022/03/09733177/1BENJJewLKw

by todsacerdoti • 4 years ago

52 22 4 years ago

mbrodersen• 4 years ago

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?

ebingdom• 4 years ago

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?

zmgsabst• 4 years ago

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/

HWR_14• 4 years ago

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?

userbinator• 4 years ago

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.

mikedodds4• 4 years ago

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.

jnash4• 4 years ago

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.

waste_monk• 4 years ago

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.

NickNameNick• 4 years ago

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.

jnash4• 4 years ago

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.

mikedodds4• 4 years ago

I'm the author of this article. I'd be happy to answer questions if anyone has them.

nextos2• 4 years ago

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)?

mikedodds4• 4 years ago

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

jnash4• 4 years ago

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 :)

AlotOfReading• 4 years ago

The cryptol-course [1] is also a good, practical introduction to the system discussed in this paper.

[1] https://github.com/weaversa/cryptol-course

Formally Verifying Industry Cryptography

Related Stories