Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Verified Correctness and Security of OpenSSL HMAC

katherineye.com

Post reply on HN
Print view View original

1–10 of 27 posts

Re: Verified Correctness and Security of OpenSSL HMAC

#2

Post by jeffreyrogers »

I always find these sorts of things interesting and research in this area is something I try to pay attention to whenever it comes to my attention, for example here is another recent paper about verifying curve25519 http://dl.acm.org/citation.cfm?id=2660370.

However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense. Humans are pretty good at doing proofs, so it seems that with a comparable amount of time you could just have a human verify that the C implementation matched the spec. (Yes, I know that this result goes a bit beyond that by using compcert, etc.)

Now obviously the state of the art is progressing and it's getting easier to formally verify properties of programs, but I wonder whether it will ever be feasible to make this part of everyday software development. Anyways, these are just my half-baked ramblings since this isn't a topic I've thought about a whole lot, but I'm interested to hear other peoples perspectives.

Re: Verified Correctness and Security of OpenSSL HMAC

#3

Post by nmrm2 »

jeffreyrogers wrote: post #2

I always find these sorts of things interesting and research in this area is something I try to pay attention to whenever it comes to my attention, for example here is another recent paper about verifying curve25519 http://dl.acm.org/citation.cfm?id=2660370 . However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense. Humans are p…

> Humans are pretty good at doing proofs

A few problems with human-style proofs:

* Cost of proof construction: Using computational tools allows us to offload large portions of the proof to decision procedures, automated proof strategies, and invariant generators. This substantially reduces the effort involved in coming up with a proof in the first place.

* Cost of validation: Humans make mistakes all the time. Peer/self reviewing a proof of that size and complexity in order to ensure that the proof does not contain errors will dominate the total proof writing time. (Edit: with computers we get proof checking for free.)

> Now obviously the state of the art is progressing and it's getting easier to formally verify properties of programs, but I wonder whether it will ever be feasible to make this part of everyday software development.

Part of the reason for doing these large verification projects is to figure out what, exactly, makes verification so difficult and time-consuming. And then developing new technology to make formal proof development cheaper. Many of these large verification efforts result in an offshoot of papers about new techniques for proving, or new design considerations for theorem provers, or new libraries that will make similar proofs in the future easier.

Re: Verified Correctness and Security of OpenSSL HMAC

#4

Post by yodsanklai »

jeffreyrogers wrote: post #2

I always find these sorts of things interesting and research in this area is something I try to pay attention to whenever it comes to my attention, for example here is another recent paper about verifying curve25519 http://dl.acm.org/citation.cfm?id=2660370 . However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense. Humans are p…

> However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense.

I suppose the effort wasn't just to prove this software correct, but to develop a methodology that allows proving other similar software.

> I wonder whether it will ever be feasible to make this part of everyday software development

I think that's where we're headed. For one thing, verification could be much easier with a language that was designed to ease verification (not C!).

We can also expect to eventually have a lot of proved correct components that we'll glue together using some languages that makes it easy to prove that the composition is correct.

Re: Verified Correctness and Security of OpenSSL HMAC

#6

Post by mpu »

jeffreyrogers wrote: post #2

I always find these sorts of things interesting and research in this area is something I try to pay attention to whenever it comes to my attention, for example here is another recent paper about verifying curve25519 http://dl.acm.org/citation.cfm?id=2660370 . However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense. Humans are p…

It's not really a 'bit beyond'. The proof is about the machine code that runs on the CPU! It's a huge abstraction gap from C and it is the result of years of formal proofs and PL research.

About the effort being worth it or not, I believe that security critical programs MUST have formal proofs. Vulnerabilities in this kind of software are extremely costly. The same goes for software whose failure can be of danger for humans (c.f. the Toyota debacle).

Re: Verified Correctness and Security of OpenSSL HMAC

#8

Post by tptacek »

mpu wrote: post #6
jeffreyrogers wrote: post #2

I always find these sorts of things interesting and research in this area is something I try to pay attention to whenever it comes to my attention, for example here is another recent paper about verifying curve25519 http://dl.acm.org/citation.cfm?id=2660370 . However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense. Humans are p…

It's not really a 'bit beyond'. The proof is about the machine code that runs on the CPU! It's a huge abstraction gap from C and it is the result of years of formal proofs and PL research. About the effort being worth it or not, I believe that security critical programs MUST have formal proofs. Vulnerabilities in this kind of software are extremely costly. The same goes for software whose failure can be of danger for…

A surprisingly large number of lines of code become security critical by dint of inclusion in security critical systems designed by others, or in support systems for those critical systems.

Re: Verified Correctness and Security of OpenSSL HMAC

#9

Post by gRKKOeQT16 »

0x0 wrote: post #7

Even coq have had its bugs where it was possible to prove that true is false: https://github.com/clarus/falso

Coq's kernel isn't particularly small so bugs are to be expected. The bug exploited in "falso", however, was outside the kernel. It never threatened correctness of existing Coq proofs.
Post reply on HN