On: Verified Correctness and Security of OpenSSL HMAC

[dmix]

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.

[nickpsecurity → dmix]

I link to quite a few microkernel-based examples in the recent post below. Skip to my reply to @Thoth with all the links.

https://www.schneier.com/blog/archives/2015/05/friday_squid_...

[dlitz → dmix]

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

[tptacek → dlitz]

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.