Hacker News Reader

> 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.

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

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.

...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 including untrusted code in your app.

Instead, you just slap any and all untrusted code into microservices (microdaemons?) in their own security domains/sandboxes/VMs/whatever, and speak to them over the kernel's message bus (or in the VM case, a virtual network), and suddenly they can't hurt you any more.

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.

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 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_...

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.

Too be fair it looks like they're "just" using CompCert to go from C to asm. CompCert has been around for a while and is a verified compiler, which itself is quite an accomplishment.

But yes, it is remarkable how far things have come with regards to formal methods. But it is still quite tedious to do unless you're an academic working in the field.

I know the project quite well, it's led by Appel and is called Verified Software Toolchain. They not only compile their code with compcert but also use its correctness theorem to derive the validity of the Assembly code!

My main comment addresses some of this. I think the consensus on this is that most software will use other techniques with lower barrier to entry that leverage stuff built with higher assurance. For example, certain imperative (Ada) and functional (Ocaml) seem to prevent all kinds of errors with decent performance. The Middle Way is to make the toolchain and critical libraries high assurance while the developer uses the basic features of the language with a decent software process. The process aims for good requirements, conservative design, reuse of proven implementation strategies, and good coding styles. These get checked, analyzed, and turned into machine code by trustworthy components.

Such an approach knocks out the vast majority of problems. The rest get squeezed out incrementally over time as research and development continues.

> 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.

> 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... <same old FUD>" like your comments for the next twenty years or so.