11 ms·

Unhackable Kernel?

57 points by bootload 11y ago

pvdebbe 11y ago
From the title I readily thought about the Windows kernel and how it can't be tweaked and recompiled and improved like Linux. Now I know better...
ifdefdebug 11y ago
"unhackable"? After reading "How to Write Unmaintainable Code" [1] earlier, I expected to find some kernel code implementing all those valuable principles, not an article about a kernel proven secure against any attack :) [1] https://news.ycombinator.com/item?id=10237636 https://news.ycombinator.com/item?id=10237636
nickpsecurity 11y ago
The slides "achille" posted are a must-read for people understanding what they're actually doing rather than nonsense about "unhackable." For instance, the seL4 team is clear on risk areas of their proofs: http://sel4.net/Info/FAQ/proof.pml http://sel4.net/Info/FAQ/proof.pml What's really going here is significant work in high-assurance design and security of two systems. They're using best modern tools to help prove or even synthesize about every layer and component in those systems. They're also developing and improving tools to argue that they integrate in a way that's secure for the whole system. In the past, similar, high-assurance methods led to the most robust and secure software ever created per the experience reports. This work expands on such techniques while attempting to make the tools, methods, and software produced reusable in other projects. In short, they're applying The Right Thing philosophy to as much as possible. Galois's Ivory and Tower languages can be found here: http://ivorylang.org/ http://ivorylang.org/ seL4 is found here: https://sel4.systems/ https://sel4.systems/ CertiKOS, VeriML, and other FLINT work here: http://flint.cs.yale.edu/certikos/ http://flint.cs.yale.edu/certikos/ Termite Driver Synthesis here: https://github.com/termite2/Termite https://github.com/termite2/Termite CompCert here: http://compcert.inria.fr/ http://compcert.inria.fr/ A how-to on certified programming that's more accessible for newcomers: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
mschuster91 11y ago
What is the most worrying aspect of proven-unhackable kernels is that eventually these projects will be used to prevent people from modifying their system. Proven unjailbreakable phones are the wet dream of the mobile carrier industry - finally no piracy anymore and no way for users to get rid of bloatware.
- nickpsecurity 11y ago
  Sadly, you're correct. The protections that were on the Xbox 360 and in Apple phones started out as academic explorations in secure hardware. Many of these have direct application to DRM. Microsoft is heavily invested in them. It can still be done with user in control but device and OS manufacturers have opposite incentives.
- wingless 11y ago
  ...until someone develops a hardware exploit and starts selling kits. Which is already happening for many devices, by the way.
  - userbinator 11y ago
    That raises the barrier substantially, however. Also, you can bet that the hardware will be secured too - just look at the technology available currently for things like credit cards and payment systems (where I think the security is somewhat more justified.)
- mtgx 11y ago
  That may come soon anyway with Intel Skylake's SGX.
- gue5t 11y ago
  Maybe then we'll be able to convince people that they can't use benevolent hackers (geohotz, comex, et al.) as the get-out-of-jail-free card for having given money to companies that do not respect them. The current status quo of the open-source community being able to make use of closed-source hardware, often producing viable devices where the vendors had hoped to provide something locked-down and near useless (e.g. openwrting routers, or that amazon button thing) is very nice, but does substantially draw wind out of the sails of open hardware initiatives: with companies able to subsidize the cost of hardware using other revenue streams, groups aiming to produce open-source hardware have to deal with not only per-unit costs being much higher due to smaller production runs but also the ability of many companies to sell hardware below reasonable prices due to charging for associated proprietary services. If open hardware becomes the only hardware on which open software can run, its value proposition changes significantly for the better.
thoastbrot 11y ago
"a prank"? Crashing a car is a prank?
- Beltiras 11y ago
  The journalist driver was in on it. I would still not rate that as a "prank". I'd be way too worried about collateral damage resulting from it to take any part in such a stunt.
- mrweasel 11y ago
  Honestly, I still have issues with that story. Either someone shouldn't be allowed to put computers in cars or someone is lying. I almost refuse to believe it's possible to jump from the entertainment system to the computers controlling the car. Designing a car where those two systems are connected in any way other than maybe power and one-way signalling from the car to the entertainment system would be reckless to an almost criminal extend. Honestly, what engineer would suggest something like that?
  - titanomachy 11y ago
    The guys who did the hack chose the Jeep exactly for this reason -- an unregulated data pipe between the entertainment computer and the critical-systems computer. They analysed hundreds of cars and chose the worst-designed one they could find.
deleted 11y ago
[deleted]
doe88 11y ago
Not sure about the unhackable claims part but it seems at least to be an interesting project. This is a formally verified L4 derived micro-kernel, its code is open-source (GPL2, BSD). Homepage: https://sel4.systems/ https://sel4.systems/ Github: https://github.com/seL4/seL4 https://github.com/seL4/seL4 Related course (already posted on HN i think but can't find its associated thread): http://www.cse.unsw.edu.au/~cs9242/14/lectures/ http://www.cse.unsw.edu.au/~cs9242/14/lectures/
- amirmc 11y ago
  They also have http://sel4.com http://sel4.com -- why wouldn't they use the .com as the canonical site instead of a more obscure .systems? (I say this because sel4.systems is linked from within the original article). Also, the link http://sel4.systems/FAQ/proof.pml http://sel4.systems/FAQ/proof.pml is a 404 (linked within the article where it says "Last year, Heiser’s team proved mathematically that their kernel is unhackable."). I guess this is meant to link to http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml (where the claims are far more measured).
  - sanxiyn 11y ago
    I don't think claims are more measured. It is more detailed, yes, but claims are still extremely strong. "Integrity means that data cannot be changed without permission, and confidentiality means that data cannot be read without permission." seL4 claims both. I think "unhackable" is a good enough summary.
    - andrewchambers 11y ago
      Hacking includes guessing credentials. I don't think this protects against bad passwords etc.
    - amirmc 11y ago
      I didn't mean to imply that the claims were not strong. Just that they're more careful/specific (which is a good thing for this kind of work). Also, saying a piece of software is "unhackable" is akin to saying a ship is "unsinkable".
deleted 11y ago
[deleted]
sanxiyn 11y ago
The primary paper to read is "Comprehensive formal verification of an OS microkernel" (2014). http://dl.acm.org/citation.cfm?id=2560537 http://dl.acm.org/citation.cfm?id=2560537
- tempVariable 11y ago
  That is $15 for non-members. First Google result for "Comprehensive formal verification of an OS microkernel" is a PDF link on ssrg.nicta.com.au. Good enough for me.
achille 11y ago
Note that the SEL4 kernel is only a small portion of this project. They've secured the entire stack, top to bottom. HACMS leverages a number of other projects including the CompCert verifying C compiler, Verve OS Theorem prover, model checkers. You also need need proofs for the communication protocol, the IP stack, secured device drivers, memory protection units, control systems that can detect attacks, etc. Just a proven kernel won't keep the helicopter flying, you've got to secure everything. Additionally you need to reason about execution time and memory constraints. Slides: http://www.cyber.umd.edu/sites/default/files/documents/symposium/fisher-HACMS-MD.pdf http://www.cyber.umd.edu/sites/default/files/documents/sympo... Presentation from Kathleen Fisher, the researcher who's won the DARPA grant for the program: * https://www.youtube.com/watch?v=YqRdbgRPYw8 https://www.youtube.com/watch?v=YqRdbgRPYw8
- petra 11y ago
  Interesting lecture by DARPA. It also refers to their secure UAV project, which is as anexample to embedded system: http://ssrg.nicta.com.au/projects/TS/SMACCM/ http://ssrg.nicta.com.au/projects/TS/SMACCM/ They also released a formally proven real-time OS.
- mtgx 11y ago
  So can you create a general purpose OS with something like this, or is it only useful for embedded stuff, like say voting machines?
  - tptacek 11y ago
    It is unlikely that anyone is going to create a general-purpose operating system based directly on an L4 kernel. L4 is incredibly simple. The more reasonable thing to do with L4 is to run another OS on top of it.
    - hga 11y ago
      I know of this effort: http://genode.org/ http://genode.org/ More specifically, I'd wonder about efforts to create not (necessarily) POSIX based stuff on top of seL4 etc.
Klasiaster 11y ago
But still software running on top of it might not be secure and proven. And as well the hardware is another area for attacks and failures.
dvh 11y ago
How practical is this, does it have sata? usb? network? bash? some compiler?
- sanxiyn 11y ago
  It is practical enough to autopilot UAV.
9fb29947 11y ago
There is no such thing as an unhackable system.
- rhaps0dy 11y ago
  Not yet. But there may be in the future. Many things proved impossible have shown to be possible in the past.
  - Beltiras 11y ago
    Gödel's Incompleteness Theorem might be abstractable to this. Any system so inaccessible as to be unhackable might be functionally impaired beyond usefulness.
    - jdefr89 11y ago
      Godel's theorem is great for claims like this. Have they proved that the "theorem proving" software has no mistakes?
      - hga 11y ago
        There's this: http://proof-technologies.com/holzero/index.html http://proof-technologies.com/holzero/index.html and I see some other things that I interpret as moving in that direction.
nabla9 11y ago
Current cream of the crop: IBM System z is EAL5 rated (Semiformally Designed and Tested) Integrity-178B is EAL6 rated (Semiformally Verified Design and Tested). It's used in aviation systems: Airbus A380, F-16, F-22, F-35 and B-2. Currently the only EAL7+ rated (Formally Verified Design and Tested) devices are data diodes. Maybe seL4 can be first OS to get this rating?
- nickpsecurity 11y ago
  The SCOMP STOP OS, GEMSOS, ASOS, LOCK, and Boeing SNS platforms were all produced to Orange Book A1 class that's largely EAL7-equivalent. STOP, GEMSOS, and SNS were all certified at A1. They're all still available for purchase. For reasons illustrated here [1], they've either dropped to EAL5+ or not been re-certified under Common Criteria. Boeing SNS kept its EAL6-7 development assurance, though, while GEMSOS is available [2] in original form via Aesec w/ various prototype applications. The new kids on the block, under MILS and SKPP banner, are taking chances with certifications that Old Guard knows are a financial trap given U.S. govt's promises aren't reliable. Private certifications against these criteria and with open-ended, pen tests are better route for cost-benefit tradeoff. [1] http://lukemuehlhauser.com/wp-content/uploads/Bell-Looking-Back-Addendum.pdf http://lukemuehlhauser.com/wp-content/uploads/Bell-Looking-B... [2] http://aesec.com/ http://aesec.com/ [3] https://web.archive.org/web/20150819095124/http://www.cis.upenn.edu/~KeyKOS/ https://web.archive.org/web/20150819095124/http://www.cis.up... (Added No 3 to represent capability-security systems given KeyKOS was fielded and had a B3/EAL6 assurance argument. Neat architecture.) Note: The Bell paper showed both how commercial systems couldn't be trusted on a network and potential NSA IAD subversion back then. Aesec's Evaluation Report is interesting reading both for how to do high assurance architecture plus for risks like hardware they didn't see coming back then. It needs to be put on trusted hardware or ported to strong, hardware TCB. CHERI, maybe, since GEMSOS uses segmented protections.
- hackuser 11y ago
  I went to lookup EAL in Wikipedia and discovered something interesting: The exact same information as above on the EAL page (with a little on the Integrity OS page). Either the info above is from Wikipedia, or perhaps the commenter above also wrote those sections of the Wikipedia pages, or the commenter read something else that was based on those Wikipedia pages. The web is an interesting place.
nerdy 11y ago
It can be just like that "Unsinkable" ship!
hackuser 11y ago
SEL4 previously discussed at HN: https://news.ycombinator.com/item?id=7938149 https://news.ycombinator.com/item?id=7938149

57 points by bootload 11y ago

From the title I readily thought about the Windows kernel and how it can't be tweaked and recompiled and improved like Linux. Now I know better...

ifdefdebug 11y ago

"unhackable"? After reading "How to Write Unmaintainable Code" [1] earlier, I expected to find some kernel code implementing all those valuable principles, not an article about a kernel proven secure against any attack :) [1] https://news.ycombinator.com/item?id=10237636 https://news.ycombinator.com/item?id=10237636

nickpsecurity 11y ago

The slides "achille" posted are a must-read for people understanding what they're actually doing rather than nonsense about "unhackable." For instance, the seL4 team is clear on risk areas of their proofs: http://sel4.net/Info/FAQ/proof.pml http://sel4.net/Info/FAQ/proof.pml What's really going here is significant work in high-assurance design and security of two systems. They're using best modern tools to help prove or even synthesize about every layer and component in those systems. They're also developing and improving tools to argue that they integrate in a way that's secure for the whole system. In the past, similar, high-assurance methods led to the most robust and secure software ever created per the experience reports. This work expands on such techniques while attempting to make the tools, methods, and software produced reusable in other projects. In short, they're applying The Right Thing philosophy to as much as possible. Galois's Ivory and Tower languages can be found here: http://ivorylang.org/ http://ivorylang.org/ seL4 is found here: https://sel4.systems/ https://sel4.systems/ CertiKOS, VeriML, and other FLINT work here: http://flint.cs.yale.edu/certikos/ http://flint.cs.yale.edu/certikos/ Termite Driver Synthesis here: https://github.com/termite2/Termite https://github.com/termite2/Termite CompCert here: http://compcert.inria.fr/ http://compcert.inria.fr/ A how-to on certified programming that's more accessible for newcomers: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/

mschuster91 11y ago

What is the most worrying aspect of proven-unhackable kernels is that eventually these projects will be used to prevent people from modifying their system. Proven unjailbreakable phones are the wet dream of the mobile carrier industry - finally no piracy anymore and no way for users to get rid of bloatware.

nickpsecurity 11y ago
Sadly, you're correct. The protections that were on the Xbox 360 and in Apple phones started out as academic explorations in secure hardware. Many of these have direct application to DRM. Microsoft is heavily invested in them. It can still be done with user in control but device and OS manufacturers have opposite incentives.
wingless 11y ago
...until someone develops a hardware exploit and starts selling kits. Which is already happening for many devices, by the way.
- userbinator 11y ago
  That raises the barrier substantially, however. Also, you can bet that the hardware will be secured too - just look at the technology available currently for things like credit cards and payment systems (where I think the security is somewhat more justified.)
mtgx 11y ago
That may come soon anyway with Intel Skylake's SGX.
gue5t 11y ago
Maybe then we'll be able to convince people that they can't use benevolent hackers (geohotz, comex, et al.) as the get-out-of-jail-free card for having given money to companies that do not respect them. The current status quo of the open-source community being able to make use of closed-source hardware, often producing viable devices where the vendors had hoped to provide something locked-down and near useless (e.g. openwrting routers, or that amazon button thing) is very nice, but does substantially draw wind out of the sails of open hardware initiatives: with companies able to subsidize the cost of hardware using other revenue streams, groups aiming to produce open-source hardware have to deal with not only per-unit costs being much higher due to smaller production runs but also the ability of many companies to sell hardware below reasonable prices due to charging for associated proprietary services. If open hardware becomes the only hardware on which open software can run, its value proposition changes significantly for the better.

thoastbrot 11y ago

"a prank"? Crashing a car is a prank?

Beltiras 11y ago
The journalist driver was in on it. I would still not rate that as a "prank". I'd be way too worried about collateral damage resulting from it to take any part in such a stunt.
mrweasel 11y ago
Honestly, I still have issues with that story. Either someone shouldn't be allowed to put computers in cars or someone is lying. I almost refuse to believe it's possible to jump from the entertainment system to the computers controlling the car. Designing a car where those two systems are connected in any way other than maybe power and one-way signalling from the car to the entertainment system would be reckless to an almost criminal extend. Honestly, what engineer would suggest something like that?
- titanomachy 11y ago
  The guys who did the hack chose the Jeep exactly for this reason -- an unregulated data pipe between the entertainment computer and the critical-systems computer. They analysed hundreds of cars and chose the worst-designed one they could find.

deleted 11y ago

[deleted]

doe88 11y ago

Not sure about the unhackable claims part but it seems at least to be an interesting project. This is a formally verified L4 derived micro-kernel, its code is open-source (GPL2, BSD). Homepage: https://sel4.systems/ https://sel4.systems/ Github: https://github.com/seL4/seL4 https://github.com/seL4/seL4 Related course (already posted on HN i think but can't find its associated thread): http://www.cse.unsw.edu.au/~cs9242/14/lectures/ http://www.cse.unsw.edu.au/~cs9242/14/lectures/

amirmc 11y ago
They also have http://sel4.com http://sel4.com -- why wouldn't they use the .com as the canonical site instead of a more obscure .systems? (I say this because sel4.systems is linked from within the original article). Also, the link http://sel4.systems/FAQ/proof.pml http://sel4.systems/FAQ/proof.pml is a 404 (linked within the article where it says "Last year, Heiser’s team proved mathematically that their kernel is unhackable."). I guess this is meant to link to http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml (where the claims are far more measured).
- sanxiyn 11y ago
  I don't think claims are more measured. It is more detailed, yes, but claims are still extremely strong. "Integrity means that data cannot be changed without permission, and confidentiality means that data cannot be read without permission." seL4 claims both. I think "unhackable" is a good enough summary.
  - andrewchambers 11y ago
    Hacking includes guessing credentials. I don't think this protects against bad passwords etc.
  - amirmc 11y ago
    I didn't mean to imply that the claims were not strong. Just that they're more careful/specific (which is a good thing for this kind of work). Also, saying a piece of software is "unhackable" is akin to saying a ship is "unsinkable".

deleted 11y ago

[deleted]

sanxiyn 11y ago

The primary paper to read is "Comprehensive formal verification of an OS microkernel" (2014). http://dl.acm.org/citation.cfm?id=2560537 http://dl.acm.org/citation.cfm?id=2560537

tempVariable 11y ago
That is $15 for non-members. First Google result for "Comprehensive formal verification of an OS microkernel" is a PDF link on ssrg.nicta.com.au. Good enough for me.

achille 11y ago

Note that the SEL4 kernel is only a small portion of this project. They've secured the entire stack, top to bottom. HACMS leverages a number of other projects including the CompCert verifying C compiler, Verve OS Theorem prover, model checkers. You also need need proofs for the communication protocol, the IP stack, secured device drivers, memory protection units, control systems that can detect attacks, etc. Just a proven kernel won't keep the helicopter flying, you've got to secure everything. Additionally you need to reason about execution time and memory constraints. Slides: http://www.cyber.umd.edu/sites/default/files/documents/symposium/fisher-HACMS-MD.pdf http://www.cyber.umd.edu/sites/default/files/documents/sympo... Presentation from Kathleen Fisher, the researcher who's won the DARPA grant for the program: * https://www.youtube.com/watch?v=YqRdbgRPYw8 https://www.youtube.com/watch?v=YqRdbgRPYw8

petra 11y ago
Interesting lecture by DARPA. It also refers to their secure UAV project, which is as anexample to embedded system: http://ssrg.nicta.com.au/projects/TS/SMACCM/ http://ssrg.nicta.com.au/projects/TS/SMACCM/ They also released a formally proven real-time OS.
mtgx 11y ago
So can you create a general purpose OS with something like this, or is it only useful for embedded stuff, like say voting machines?
- tptacek 11y ago
  It is unlikely that anyone is going to create a general-purpose operating system based directly on an L4 kernel. L4 is incredibly simple. The more reasonable thing to do with L4 is to run another OS on top of it.
  - hga 11y ago
    I know of this effort: http://genode.org/ http://genode.org/ More specifically, I'd wonder about efforts to create not (necessarily) POSIX based stuff on top of seL4 etc.

Klasiaster 11y ago

But still software running on top of it might not be secure and proven. And as well the hardware is another area for attacks and failures.

dvh 11y ago

How practical is this, does it have sata? usb? network? bash? some compiler?

sanxiyn 11y ago
It is practical enough to autopilot UAV.

9fb29947 11y ago

There is no such thing as an unhackable system.

rhaps0dy 11y ago
Not yet. But there may be in the future. Many things proved impossible have shown to be possible in the past.
- Beltiras 11y ago
  Gödel's Incompleteness Theorem might be abstractable to this. Any system so inaccessible as to be unhackable might be functionally impaired beyond usefulness.
  - jdefr89 11y ago
    Godel's theorem is great for claims like this. Have they proved that the "theorem proving" software has no mistakes?
    - hga 11y ago
      There's this: http://proof-technologies.com/holzero/index.html http://proof-technologies.com/holzero/index.html and I see some other things that I interpret as moving in that direction.

nabla9 11y ago

Current cream of the crop: IBM System z is EAL5 rated (Semiformally Designed and Tested) Integrity-178B is EAL6 rated (Semiformally Verified Design and Tested). It's used in aviation systems: Airbus A380, F-16, F-22, F-35 and B-2. Currently the only EAL7+ rated (Formally Verified Design and Tested) devices are data diodes. Maybe seL4 can be first OS to get this rating?

nickpsecurity 11y ago
The SCOMP STOP OS, GEMSOS, ASOS, LOCK, and Boeing SNS platforms were all produced to Orange Book A1 class that's largely EAL7-equivalent. STOP, GEMSOS, and SNS were all certified at A1. They're all still available for purchase. For reasons illustrated here [1], they've either dropped to EAL5+ or not been re-certified under Common Criteria. Boeing SNS kept its EAL6-7 development assurance, though, while GEMSOS is available [2] in original form via Aesec w/ various prototype applications. The new kids on the block, under MILS and SKPP banner, are taking chances with certifications that Old Guard knows are a financial trap given U.S. govt's promises aren't reliable. Private certifications against these criteria and with open-ended, pen tests are better route for cost-benefit tradeoff. [1] http://lukemuehlhauser.com/wp-content/uploads/Bell-Looking-Back-Addendum.pdf http://lukemuehlhauser.com/wp-content/uploads/Bell-Looking-B... [2] http://aesec.com/ http://aesec.com/ [3] https://web.archive.org/web/20150819095124/http://www.cis.upenn.edu/~KeyKOS/ https://web.archive.org/web/20150819095124/http://www.cis.up... (Added No 3 to represent capability-security systems given KeyKOS was fielded and had a B3/EAL6 assurance argument. Neat architecture.) Note: The Bell paper showed both how commercial systems couldn't be trusted on a network and potential NSA IAD subversion back then. Aesec's Evaluation Report is interesting reading both for how to do high assurance architecture plus for risks like hardware they didn't see coming back then. It needs to be put on trusted hardware or ported to strong, hardware TCB. CHERI, maybe, since GEMSOS uses segmented protections.
hackuser 11y ago
I went to lookup EAL in Wikipedia and discovered something interesting: The exact same information as above on the EAL page (with a little on the Integrity OS page). Either the info above is from Wikipedia, or perhaps the commenter above also wrote those sections of the Wikipedia pages, or the commenter read something else that was based on those Wikipedia pages. The web is an interesting place.

nerdy 11y ago

It can be just like that "Unsinkable" ship!

hackuser 11y ago

SEL4 previously discussed at HN: https://news.ycombinator.com/item?id=7938149 https://news.ycombinator.com/item?id=7938149