4 ms·

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 fo

by mpu 11y ago

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

tptacek 11y ago
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.
- derefr 11y ago
  ...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.
  - dmix 11y ago
    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 11y ago
      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_bl_479.html#c6697743 https://www.schneier.com/blog/archives/2015/05/friday_squid_...
    - dlitz 11y ago
      I'm not sure if this matches the description, but seL4 supposedly has a pretty well-developed proof system: https://sel4.systems/ https://sel4.systems/
      - tptacek 11y ago
        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.
  - jeffreyrogers 11y ago
    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/ http://openmirage.org/
    - nickpsecurity 11y ago
      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.
jeffreyrogers 11y ago
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.
- mpu 11y ago
  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!

by mpu 11y ago

tptacek 11y ago

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.

derefr 11y ago
...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.
- dmix 11y ago
  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 11y ago
    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_bl_479.html#c6697743 https://www.schneier.com/blog/archives/2015/05/friday_squid_...
  - dlitz 11y ago
    I'm not sure if this matches the description, but seL4 supposedly has a pretty well-developed proof system: https://sel4.systems/ https://sel4.systems/
    - tptacek 11y ago
      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.
- jeffreyrogers 11y ago
  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/ http://openmirage.org/
  - nickpsecurity 11y ago
    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.

jeffreyrogers 11y ago

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.

mpu 11y ago
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!