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

21–27 of 27 posts

Re: Verified Correctness and Security of OpenSSL HMAC

#21

Post by nickpsecurity »

jeffreyrogers wrote: post #14
derefr wrote: post #11

Earlier quoted context omitted.

...which is a big reason why I find it insane that people aren't more interested in microkernel (or unikernel+hypervisor, which ends up in the same place) designs. If you can have a tiny trust-kernel that has been proof-checked, keep everything else outside of it, and the things outside of it can only communicate with (or even observe) their peers via messages sent through it, then you don't need to worry about inclu…

I think the problem is that operating systems aren't that useful until they have applications and a userbase. Some projects (like Mirage[1] and a few others) try to get around this by building on top of Xen, but that creates a lot of friction. [1]: http://openmirage.org/

This is true. It's also why most serious projects are paravirtualizing OS's such as NetBSD or Linux. QNX and Minix 3 leverage code from NetBSD. Most of the L4's do a L4 Linux that runs Linux in user-mode on the tiny kernel. I link to specific examples in another comment here. Even the CHERI secure processor project ported FreeBSD (CheriBSD) to it for the need to keep legacy software.

That's a serious issue that's killed a number of past projects. At least many modern ones learned the lesson and are acting accordingly.

Re: Verified Correctness and Security of OpenSSL HMAC

#22

Post by nickpsecurity »

YAYERKA wrote: post #12
mpu wrote: post #5

Writing the definition of sha 256 in Coq must have been of great fun, hehe.

"Verification of a Cryptographic Primitive: SHA-256", Andrew Appel https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf

Thanks for the link. I always enjoy reading Appel's work.

Re: Verified Correctness and Security of OpenSSL HMAC

#23

Post by nickpsecurity »

hypotext wrote: post #17

Here's the full paper: http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf

Thanks. My favorite part is your thorough breakdown of the assurance case in section one. For redoing security evaluations, I recommended [1] a while back that vendors illustrate the assurance levels of each component in their systems. Your breakdown looks closer to my recommendation than most things I've seen. Such a breakdown is both honest and shows exactly where improvements (or mitigations) need to happen.

Otherwise, verifications were as practical and good as I'd expect. My favorite section to scope out, Related Work, gave me new insights as usual. You also had a useful idea of future work [2]. All together, great work.

[1] https://www.schneier.com/blog/archives/2014/04/friday_squid_...

[2] "One important future step is to con- dense commonalities of these libraries into an ontology for crypto-related reasoning principles, reusable across multiple language levels and realised in multiple proof assistants. "

Re: Verified Correctness and Security of OpenSSL HMAC

#24

Post by nickpsecurity »

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

True. That's why formal verification is only one of many techniques in high assurance (A1/EAL7) evaluations. The methods are all a check against each other with the minds of the designers and evaluators being the strongest check. That might seem counter-intuitive given we're doing formal verification due to people's inability to write code. Yet, people equipped properly can see mistakes in good specs or designs much better than they can do tedious work (eg low-level code) without error.

So, in high assurance, we use every tool at our disposal to counter problems and then some for redundancy. Works out fine. That said, I have a nice paper for you if you want to see how screwed up formal verification can get:

http://www.cypherpunks.to/~peter/04_verif_techniques.pdf

Things have gotten a bit better but plenty of truth left in that paper.

Re: Verified Correctness and Security of OpenSSL HMAC

#25

Post by Dewie3 »

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.

Either you reasonably need machine-checkable proofs of the software confirming to a spec, or you don't and can settle for less secure methods. Then be honest and lay out what parts of the program are verified, which are proven ~informally by hand, which has been reviewed by several people, which uses a lot of tests, and so on. Risk/reward analysis like anything else (but obviously not straightforward).

Formal verification is probably so young/not widespread as a discipline that we'll probably see peanut gallery concern trolling "this is really cool! But... " like your comments for the next twenty years or so.

Re: Verified Correctness and Security of OpenSSL HMAC

#26

Post by dlitz »

dmix wrote: post #13
derefr wrote: post #11

Earlier quoted context omitted.

...which is a big reason why I find it insane that people aren't more interested in microkernel (or unikernel+hypervisor, which ends up in the same place) designs. If you can have a tiny trust-kernel that has been proof-checked, keep everything else outside of it, and the things outside of it can only communicate with (or even observe) their peers via messages sent through it, then you don't need to worry about inclu…

Do you have any examples of this type of approach being used in any projects? I'd be curious to check out how it works code-wise.

I'm not sure if this matches the description, but seL4 supposedly has a pretty well-developed proof system: https://sel4.systems/

Re: Verified Correctness and Security of OpenSSL HMAC

#27

Post by tptacek »

dlitz wrote: post #26
dmix wrote: post #13

Earlier quoted context omitted.

Do you have any examples of this type of approach being used in any projects? I'd be curious to check out how it works code-wise.

I'm not sure if this matches the description, but seL4 supposedly has a pretty well-developed proof system: https://sel4.systems/

Worth keeping in mind that L4 kernels do much, much less than conventional operating systems. They're more like libraries for building useful OS's on top of.
Post reply on HN