3 ms·

I used to think only crazy ivory-tower research project proposed rebuilding our operating systems from the ground up using sound methods, proved correctness in

by zellyn 10y ago

I used to think only crazy ivory-tower research project proposed rebuilding our operating systems from the ground up using sound methods, proved correctness in the inner parts, and better languages: a nice idea, but a bit crazy, and unlikely to succeed outside of academia. The more time goes by, and the more ubiquitous our computing devices become, the crazier it seems not to take this approach. It sounds like Fuchsia is (might be?) a step in the right direction… I'm excited to see what happens there.

nickpsecurity 10y ago
One low to medium work end, it's Muen separation kernel and Redox OS that show using better languages to knock out issues. On the high end, see ancient GEMSOS, seL4/L4.Verified, Microsoft's VerveOS, and DeepSpec's CertiKOS. For hardware, it's Cambridge CHERI, Nagarakette et al's Watchdog CPU's, or crypto-related stuff in Joshua Edmison's dissertation. Fuchsia is at least a microkernel but I don't know if they use methods others do to eliminate 0-days or covert channels.
- zellyn 10y ago
  Do any of the actually-bulletproof ones have enough momentum to have any likelihood of one day being widely used? It's sad that so many of them always seem to meander into dead-ends, or result in proprietary offshoots aimed at high-assurance environments. :-(
  - nickpsecurity 10y ago
    There always has to be a core group of knowledgeable people either developing or maintaining submissions to them. It's just the nature of the game for highest quality/reliability/security. So far, this has produced almost entirely proprietary or academic solutions with the FOSS ones not receiving nearly the contributions they need. You can't just scratch an itch and improve something that's nearly NSA-proof most of the time. Only FOSS project actively soliciting and sometimes integrating best-of-breed components from high-assurance field is Genode OS framework. They recently went AGPL, though, for non-proprietary license. That's not promising... The others stopped getting any maintenance or their people and/or I.P. get poached into corporate circles.
    - zellyn 10y ago
      Man, that makes me sad. I guess Fuchsia might end up being better than nothing. I wish one of the Google/Facebook/Apple/Microsoft/Amazons of the world would take up the flag and commit to a 10- to 20- year project :-)
      - nickpsecurity 10y ago
        It would be really nice given that Schell originally quoted 2 years per system on a verified kernel. The verified ones did always take 1-3 years but just using safe languages on verified kernels could be quicker. Google, Facebook, and Apple have nobody from high-assurance that I'm aware despite their resources. Microsoft Research snagged quite a few but they just build prototypes or tools that most of Microsoft doesn't use. None of the big names care overall that I can tell even though it would help them on certain components. Microsoft at least deployed SLAM intro production for drivers and applied formal verification to parts of Hyper-V. IBM had Paul Karger work with them on a security-enhanced CPU and smartcard OS (Caernarvon) with pieces of both being sold to customers. Otherwise, I don't know of anything happening with big companies and high-assurance tech. Only smartcard vendors seem to do it regularly for specific components in the hardware (esp MPU's) or software (esp JavaCard or MULTOS).
logicallee 10y ago
But when it's trivial to try QUADRILLION fuzzing operations (sixteen four gigahertz cores do this many operations every 4.1 hours) do you really need formal correctness? Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state? We have so much power it's obscene. We're producing SHA-1 collisions without damaging or analyzing the algorithm, just using brute force. Why not take that approach to kernel security? I'd sooner trust code whose quintillion input and output states have been exhaustively brute-forced over a few months (so that literally every possible path and value that code can take has ACTUALLY been run), than code which has been formally proven to be correct but without having been subject to such a test.
- caf 10y ago
  Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state? No. Take a simple function that has two 64-bit numbers as input and one output; your sixteen 4Ghz cores would take over 11 billion times the current age of the universe to verify it. You can, instead, do things like symbolic execution... and it turns out, that kind of thing is often a big part of "formally proven correct".
  - logicallee 10y ago
    What do fuzzers do in practice? (I am not up on the state of the art)? They try to explore edge cases, but how do they know what is likely to be an edge case? Or how do they try to get coverage of their fuzzing?
    - cnvogel 10y ago
      They no longer just try out random combinations or cover the input space exhaustively (which is not feasible anyway). Nowadays they use instrumentation in the fuzzed/tested code to have guidance in what direction the input should be modified to get more cases the code covered. Good example: http://lcamtuf.coredump.cx/afl/ http://lcamtuf.coredump.cx/afl/
    - 10y ago

by zellyn 10y ago

nickpsecurity 10y ago

One low to medium work end, it's Muen separation kernel and Redox OS that show using better languages to knock out issues. On the high end, see ancient GEMSOS, seL4/L4.Verified, Microsoft's VerveOS, and DeepSpec's CertiKOS. For hardware, it's Cambridge CHERI, Nagarakette et al's Watchdog CPU's, or crypto-related stuff in Joshua Edmison's dissertation. Fuchsia is at least a microkernel but I don't know if they use methods others do to eliminate 0-days or covert channels.

zellyn 10y ago
Do any of the actually-bulletproof ones have enough momentum to have any likelihood of one day being widely used? It's sad that so many of them always seem to meander into dead-ends, or result in proprietary offshoots aimed at high-assurance environments. :-(
- nickpsecurity 10y ago
  There always has to be a core group of knowledgeable people either developing or maintaining submissions to them. It's just the nature of the game for highest quality/reliability/security. So far, this has produced almost entirely proprietary or academic solutions with the FOSS ones not receiving nearly the contributions they need. You can't just scratch an itch and improve something that's nearly NSA-proof most of the time. Only FOSS project actively soliciting and sometimes integrating best-of-breed components from high-assurance field is Genode OS framework. They recently went AGPL, though, for non-proprietary license. That's not promising... The others stopped getting any maintenance or their people and/or I.P. get poached into corporate circles.
  - zellyn 10y ago
    Man, that makes me sad. I guess Fuchsia might end up being better than nothing. I wish one of the Google/Facebook/Apple/Microsoft/Amazons of the world would take up the flag and commit to a 10- to 20- year project :-)
    - nickpsecurity 10y ago
      It would be really nice given that Schell originally quoted 2 years per system on a verified kernel. The verified ones did always take 1-3 years but just using safe languages on verified kernels could be quicker. Google, Facebook, and Apple have nobody from high-assurance that I'm aware despite their resources. Microsoft Research snagged quite a few but they just build prototypes or tools that most of Microsoft doesn't use. None of the big names care overall that I can tell even though it would help them on certain components. Microsoft at least deployed SLAM intro production for drivers and applied formal verification to parts of Hyper-V. IBM had Paul Karger work with them on a security-enhanced CPU and smartcard OS (Caernarvon) with pieces of both being sold to customers. Otherwise, I don't know of anything happening with big companies and high-assurance tech. Only smartcard vendors seem to do it regularly for specific components in the hardware (esp MPU's) or software (esp JavaCard or MULTOS).

logicallee 10y ago

But when it's trivial to try QUADRILLION fuzzing operations (sixteen four gigahertz cores do this many operations every 4.1 hours) do you really need formal correctness? Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state? We have so much power it's obscene. We're producing SHA-1 collisions without damaging or analyzing the algorithm, just using brute force. Why not take that approach to kernel security? I'd sooner trust code whose quintillion input and output states have been exhaustively brute-forced over a few months (so that literally every possible path and value that code can take has ACTUALLY been run), than code which has been formally proven to be correct but without having been subject to such a test.

caf 10y ago
Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state? No. Take a simple function that has two 64-bit numbers as input and one output; your sixteen 4Ghz cores would take over 11 billion times the current age of the universe to verify it. You can, instead, do things like symbolic execution... and it turns out, that kind of thing is often a big part of "formally proven correct".
- logicallee 10y ago
  What do fuzzers do in practice? (I am not up on the state of the art)? They try to explore edge cases, but how do they know what is likely to be an edge case? Or how do they try to get coverage of their fuzzing?
  - cnvogel 10y ago
    They no longer just try out random combinations or cover the input space exhaustively (which is not feasible anyway). Nowadays they use instrumentation in the fuzzed/tested code to have guidance in what direction the input should be modified to get more cases the code covered. Good example: http://lcamtuf.coredump.cx/afl/ http://lcamtuf.coredump.cx/afl/
  - 10y ago