Unhackable Kernel?
newscientist.com
newscientist.com
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/sympo...
Presentation from Kathleen Fisher, the researcher who's won the DARPA grant for the program:
More specifically, I'd wonder about efforts to create not (necessarily) POSIX based stuff on top of seL4 etc.
https://my.cse.unsw.edu.au/thesis/thesis_topic_details.php?I...
I read qubes-devel with interest and have not noticed anything from these guys, but it sounds like a great project.
I really hope it's something that turns into an actual maintained project instead of dying after the paper is out like so many security-focused research projects, but the lack of communication doesn't give me great hope.
[1] http://pastebin.com/5fnh8g2S
[2] http://theinvisiblethings.blogspot.com/2012/09/how-is-qubes-...
It's worth noting that the seL4 people haven't tried to formally verify it on x86 (and there's no 64 bit port to date that I know of, outside of possibly the lowRISC GSoC effort which I should check up on), only ARMv6 and v7 (which, I'll grant, also has to do with academic efforts to verify ARM in general). If you're that serious, seL4 serious, there's a good argument you should eschew Intel and start with some of the less chaotic ARM systems (i.e. not so much kitchen sink ones from the mobile world like the Broadcom chips the Raspberry Pies use).
I take her as trying something rather different, the pragmatic approach of getting the best security possible out of our existing infrastructure, hence the use of x86, Xen, Fedora, etc., based in part on her experience when figuratively putting on a black hat. She's discovered a lot of exploits, hasn't she? (lowRISC also includes an effort with tags to make our existing C/C++ infrastructure safer).
And without the prospect of a "secure" web browser aside from perhaps Servo someday, maybe....
re x86 vs ARM. It's true. Remember, though, that I didn't tell her to use seL4: just re-use work in L4 family projects like Nizza or OKL4 to get their security + performance benefits. The idea is you get a good start, make sure you can swap in/out components, and someone puts a verified one in place later. This is exactly the approach GenodeOS team took along with using many things I recommended in other post. Only gripe with them is they're doing too many things at once rather than focusing on getting at least one in best, production mode.
That said, I agree with keeping off x86. I've recommended ARM, MIPS, SPARC, and RISC-V for future work. SPARC is nice due to open specs, no licensing past $99 trademark, and GPL hardware available. RISC-V people building all kinds of things. SPARC and MIPS have already been modified for enhanced security by academics several times over. So, SPARC (esp Gaisler), MIPS, and RISC-V are my recommendations in that order putting usability/extensibility over pricing.
re pragmatic approach. Sure, I agree with that part. The resulting approach combined things top on the CVE list onto a platform she published exploits for and criticized in other posts. Gotta wonder how far its security would go. ;) She was a good bug-hunter, though, when she understood how something worked. Didn't seem to understand strong, security engineering so I predicted QubesOS would be good for vanilla malware w/ some containment of advanced attacks. Basically, a nice improvement on and replacement for Compartmented Mode Workstations's. The TCB size and implementation are just too complex for high security.
re secure browsers. For full-featured experience, you'll need either virtualization or my old KVM-switch method. More research in the former has only made the latter look more trustworthy over time haha. Anyway, I referenced a number of more-secure browser architectures in the comment below. Enjoy seeing variations of The Right Thing in action. :) Now, if only mainstream would put effort into improving those instead of the monolithic ones. Chrome was at least an OP-inspired attempt. Due credit for them.
There are, what, 4 state of the art rendering engines? (Two Microsoft, which has lots of money to spend, Webkit (now Apple and Google forked??), and Firefox's.) And there's much, much more to the security story for browsers.
Then again, this is not a topic I've looked closely at, maybe there's more hope than I think, and continuing financial losses might prompt more rigor, although I don't recall the worse ones being purely browser exploits.
There are a few approaches to this. One is to apply compiler transformations that make the code memory-safe along with interface checks at sys-call level. An example is Softbound+CETS albeit I'm not saying it's worked on a browser. Several have compiled C programs to run in a Java or other managed environment. Another example is a lighter security approach called control flow integrity where you just try to block code injections with data or pointer protection. Control Pointer Integrity is most interesting right now with several HW accelerators. The next approach is using software or hardware obfuscation to make it where the incoming attack (a) wouldn't hit its target or (b) would be mangled/detected by crypto work at HW level. This has been ported to Linux. CheriBSD is another, DARPA-funded effort that uses custom hardware (CHERI) and tooling to let you incrementally protect legacy stuff with capabilities.
So, quite a few ways to deal with it. As usual, the problem is that our machines and languages make it easy to cause a vulnerability with common, fundamental operations. Making those operations fundamentally safe[r] knocks out a lot of that risk. Traditional techniques, like separation kernels, can try to isolate and detect the rest. That's my take on how to deal with being stuck with codebases like Webkit. Still work but feels less impossible.
A lot of what you suggest for directly solving it strike me as hacks not to my taste, but I'll look harder at that sort of thing in the future.
Absent that:
If you're going to modularize it, the interfaces are going to be complex and error prone, in part what I view as the difference between relatively easier to trust ciphers such as AES and much more fragile cryptosystems/cryptographic protocols (the one bit of real research I've done here was in 1979, trying to design an public key based authentication server; no success then, I gather it took half a decade to get to the not obviously broken stage).
It's got to be fast; for now, ever faster as web pages get more and more complicated.
Although one cause of that, calling out to zillions of different sources, admits to speed ups if you can incrementally/concurrently deal with the bits as you get them ... which of course makes the system more complicated.
(There's probably a space for a browser distribution that thoroughly pretends to be from a mobile source and gets those simpler pages. :-)
Firefox/Mozilla may be in the process of killing itself, worsening the oligopoly:
Objectively, I hear they're dramatically losing market share AKA $$$ for further development.
Related to that, poor organizational management.
I heard on HN that they're preparing to move to a multiprocess architecture which will nuke their extension ecosystem, which is one of their core advantages. This is one of those nasty security-usability tradeoffs, or at least probably due to some of the above resource and organizational issues, plus perhaps security issues, the API presented to extensions won't allow them to do much. Chrome of course has this "problem".
I guess what I'll personally do is concentrate on the lower level, tentatively starting with an Raspberry Pi seL4 port (I know, stop laughing, it's the most stable (long life promise) and widely available ARM platform for learning), wait to see how Servo plays out (see above Mozilla problems), and then return to this, maybe it's less "impossible" than I sense right now. Although still plenty impossible in the approaches my taste prefers that can't be used for the foreseeable future.
Thanks a lot for your contributions to all these HN security discussions!
What (briefly) is your experience or skillset so I can better target my recommendations?
"A lot of what you suggest for directly solving it strike me as hacks not to my taste, but I'll look harder at that sort of thing in the future."
The problem is that the Web, Windows, and UNIX stacks are all hacks built on hacks with tons of compromises and many bad design choices. Anything that preserves their functionality without a rewrite is going to be hackish. So, we then decide where to put hacks among libraries, source-to-source translators, libraries, OS's, hardware, etc. I tried to name off more sensible one's to avoid readers having headaches I had going through 10,000 papers of this shit. ;)
"If you're going to modularize it, the interfaces are going to be complex and error prone"
Interface errors account for vast majority. Margaret Hamilton, Dijsktra, Robert Schell, and Paul Karger all independently discovered that w/ solutions presented. The consensus is you need to document the pre-conditions, post-conditions, and properties that always hold. Type-checking, Design-by-Contract, and similar techs help. Generic functions and good design helps keep complexity down. Functional languages with strong typing are best at making this safe and concise at same time. So, it doesn't have to be bad unless your tools suck.
"much more fragile cryptosystems/cryptographic protocols "
Sort of. Those do much more than just decompose: theory, design, implementation, distributed of all that... a tall order. Understanding the positive effect of decomposition and layering will be obvious if you look at this on p8 "Layered Design:"
http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf
Now, try to imagine a description of how VMware or KVM do the same thing. It would probably be much more complex with looping around and such. The decomposition makes it easier to understand w/ sensible interfaces. That's how it's supposed to be done anyway.
"trying to design an public key based authentication server; no success then"
As I said, crypto protocols are extra hard to do right. It's the kind of thing that should get intense tool support. The state-of-the-art in high assurance is NSA and Rockwell-Collins tool that goes from a flowchart & specs in (Simula?) to generated code or hardware with verification checks for a processor whose security is verified. An example for the rest of us and ideal for your case is combining CRYPTOL for algorithm, state machines for overall code, and SPARK for implementation language. The protocol logic would be implemented with this kind of tool:
http://www.dsi.unive.it/~modesti/anbx/
I call out plenty of people for their methods. Yet, it was understandably hard to pull off public key servers a few years after they were invented on 1970's computers. Even the people inventing INFOSEC sucked at security back then. ;)
"It's got to be fast; for now, ever faster as web pages get more and more complicated."
It does. Hence our hacks to work with normal, highly-optimized software. However, some old stuff was still faster. JavaScript is utter garbage. One alternative (Juice) used Oberon language for applets with ZIP'd abstract syntax trees. Let you type-check it, interface-check it, and then compile it super-fast to fast binary. Client-server apps could use efficient stacks, implementation languages, avoid rendering they didn't need, etc. So, plenty room for improvement especially if we use plugins or stand-alone apps where possible. Facebook Messenger, etc are ditching the Web that way.
"browser distribution that thoroughly pretends to be from a mobile source and gets those simpler pages. :-)"
Good thinking: I thought of that one, too. Still in backlog. Another model I worked out was ultra-fast, thin-client (phone or netbook) connected to a secure, desktop browser running on best hardware it could. Turns out that a variant of that (for efficiency) was done by mobile companies like Opera. So, it's possible.
"Objectively, I hear they're dramatically losing market share AKA $$$ for further development." "that they're preparing to move to a multiprocess architecture which will nuke their extension ecosystem"
That is potentially bad. I don't know about their management. Can only hope for the best there. Good news is many of the best extensions are actively maintained or should be ported in event plugin architecture changes. So, here's hoping there too. This from Wikipedia bothers me:
"making Yahoo! Search the default search experience for Firefox in North America effective December 2014.[7] However, it is also to be noted that Yahoo! Search is a merely a front-end to Microsoft's search engine Bing, and Microsoft takes a 12% cut of all revenue from the search business per the deal."
Yahoo itself is in a shaky position and Bing gets a cut? That's risky esp with what they made on Google. I'd have gotten expenses in order instead. Maybe.
"starting with an Raspberry Pi seL4 port (I know, stop laughing, it's the most stable (long life promise)"
It and Beagle port. No laughing here: do what you can. Check out Genode as well as they're among more mature of L4-based architectures. Maybe better integrate it with seL4, Linux virtualization with either, or middleware for integrating components in protection domains. These are low-hanging fruit.
"Thanks a lot for your contributions to all these HN security discussions!"
Appreciate it. The few who might benefit are the only reason I post. Well, I enjoy it too but still. ;)
Multics, ITS and the Lisp Machine are my ne plus ultra systems, but UNIX(TM) was good and available. I like the ITS/Lisp Machine development style, and in theory the FONC/VPRI and seL4 ones, but believe a modern web browser is a non-negotiable for users, and impractical with any of them, hence my angst.
Retired by disability, but should still be up for a few more serious projects, hence my looking at this arena which addresses many of my pain points. Anyway:
"JavaScript is utter garbage." Well, it has a lot of Scheme in it, so I'm not quite so hostile ... but I haven't use it except for a few months in 1997 ^_^. With any luck WebAssembly (https://github.com/WebAssembly) will make things a little less painful, the flip side of the "oligopoly" is only having to convince 4 organizations (Apple, Google, Microsoft, Mozilla). To restate, the problem for the foreseeable future is the 2nd part of Postel's law, "be liberal in what you accept from others"; an objective of mine is a "desktop" that doesn't suck and has survival value, which requires a web browser that accepts, shall we say, the "best effort" of others' web pages. Or why since the early days browsers would so their best to display something in HTML without closing tags.
I believe "survival value" is very important, it's a quality of ultimate computer viri like the UNIX family that Richard Gabriel was getting at in his Worse is Better essays (https://www.dreamsongs.com/WorseIsBetter.html). A browser's ultra-complicated moving target requires creating, co-opting, or allying with a big community of developers. Hmmm, and only by doing the latter are you likely to develop fundamentally better approaches, which need buy-in from enough of the browser "oligopoly".
"Good news is many of the best [Firefox] extensions are actively maintained or should be ported in event plugin architecture changes."
That's just not going to happen per https://news.ycombinator.com/item?id=10097630 and https://news.ycombinator.com/item?id=10099240 although I suppose there's time for Mozilla to change course, but that would require their current management to get a clue or be replaced. One bottom line for me is that Servo should be a Maximum Effort instead of a "research project". There's a lot more to be said, but probably best by email if you're interested (hga@ancell-ent.com).
Me-> "starting with an Raspberry Pi seL4 port (I know, stop laughing, it's the most stable (long life promise)"
"It and Beagle port."
I seriously considered the Beagle ecosystem, but noted it's not "stable", TI makes no representation about continuing manufacture of any given board, and the earlier (and $$$) non-Bone ones don't seem to be available. But the BeagleBone Black (BBB) was a surprise smash hit (good price + very capable industrial controller SoC, e.g. can implement a 100MHz logic analyzer), so much so it had limited availability for more than a year, and now two companies are making them.
But the Raspberry Pi huge, and committed to continued manufacture of their boards, albeit with respins. And a lot cheaper, BBB $55, first gen Pis $25 and $30, new Pi 2 $40; for just messing with seL4 I bought a $25 A+. The TCB is ridiculous, albeit ideal for for OEMs, but all things considered I judged it the best for an initial learning platform. If the BBB shows staying power I'll seriously consider it.
"going to look at ML next"
Do Ocaml for its maturity. However, if you like TCB's, might be worth it to see if FLINT certifying compiler for ML works on modern stuff and passes a battery of tests. Source-to-object code assurance plus ML correctness is powerful for tool development. My recurring idea is combining a version of it with programs extracted from Coq specifications for robust tooling.
"a modern web browser is a non-negotiable for users"
Maybe. Lots of large companies get by forcing use of terminals, client-server, and minimalist web stuff. There's also browser ports to alternative OS's like Haiku, MorphOS, and even OpenVMS at one point. So, there's room for tradeoffs. Past that, create a Linux API in a VM and put it in there.
" the flip side of the "oligopoly" is only having to convince 4 organizations (Apple, Google, Microsoft, Mozilla)"
I'm hoping that's the case. Microsoft prototyping one with Mozilla, JS as assembly, and HTML5 provide some hope. Doubt we'll get something radical like Juice project that's really better, though. I'm watching WebAssembly from a distance to see how it plays out.
"that Richard Gabriel was getting at"
Damnit, I reference that meme here all the time lol. He went back and forth with me knowing it was true after seeing the first essay. Spread like a virus with just good enough done the way others are doing it. The lesson to learn. Hard to get quality or security that way, though. Call up Trusted Xenix people to see where... wait, they don't exist anymore!?
Getting browser vendors on this is low probability of success. It's why we're all working around (HW/kernel stuff) and sometimes right through them (eg compiler stuff). As you said, it's too complicated and several scheming-ass companies are in control of it. I'll add too much legacy code. Although strange that Mozilla is throwing away a lot of theirs: might be killing their differentiator. Not sure as I'd have to see why various people used it.
"I seriously considered the Beagle ecosystem, but noted it's not "stable","
Good arguments against Beagle and for Rasp Pi. Yeah, seL4 is a start. Remember, though, that it's just a separation kernel: you have to build everything useful. Very barebones. You have your work cut out for you.
Well, first refer to the first Worse is Better essay, which directly compares The Right Thing/MIT vs. Worse is Better/New Jersey styles in handling of interruption of long system calls (invisible PCLUSER back out vs. return with error and require you to try again: https://www.dreamsongs.com/RiseOfWorseIsBetter.html).
For a few details, the security model was very well matched to the threat model (although they were forced to add login password protection :-), and while constrained in a whole bunch of weird ways, e.g. the 3 local filename components were limited to 6 6 bit-characters, one 36 bit word, total number of directories were the number of words that would fit on a page, 512 I think, it had all sorts of features I miss. E.g. plugable I/O filter and error mechanisms, a [machine-name]: convention, e.g. "AI:DIR;FNAME1 FNAME2" which I think worked on all file accesses, or the general ecosystem's Chaosnet convention of string character ports. And then there's a feature ported to UNIX by Jim Kulp, a hacker with a foot in both worlds, shell job control (^Z and friends). And on MIT-MC, a ECL KL-10 (~2xVAX 11/780), it was seriously fast. I never learned the guts of this (doomed) architecture, but the results spoke for themselves, and exceeded any PDP-10/Decsystem 20 OS I know about.
At the highest level, ITS+TECO EMACS+Maclisp was the prototype for the Lisp Machine.
As for the ML language family, I'm going for the original formula first, because of all the research I want to be able to better follow that uses it, an allergy to objects I've developed ^_^, and the TCB issue, e.g. the active CakeML project: https://cakeml.org/ I gather that pretty much anything Magnus Myreen is or has worked on is worth looking at, e.g. he's the guy who solved the seL4 HOL -> CompCert impedance mismatch by going backwards, from GCC produced binary to auto-generated models of what that binary did. If I like ML, I'm sure I'll learn Ocaml, if not, Myreen helped develop a down to the machine code validated LISP for some ACL2 related work: http://www.cl.cam.ac.uk/~mom22/jitawa/
Exactly what I do depends on whether I can grok HOL/this style of proving, haven't done that sort of thing since 1977....
Me-> "a modern web browser is a non-negotiable for users"
Maybe.
If you want to develop an end user OS that lots of people will use, that might develop a big enough developer community to survive, and that will of course address that very big pain point, well, those are all goals I hold and that I can to contribute to, one way or another. And your exception of "Lots of large companies get by forcing use of terminals, client-server, and minimalist web stuff." doesn't work for the knowledge workers that require access to the unconstrained web. That's so critical nowadays that the PRC still allows it (all but North Korea?), a ticketed programmer friend of mine does his day to day work with access to the web, starting in 1996 I would never accept a programming job that didn't give me such access, etc. etc. The ability to quickly find an answer (if it exists :-) to most any question you can ask from anywhere in the world is just too critical.
Hmmm, come to think of it, I'm not exactly enthused by the prospect of trying to run Gnu EMACS on a "secure"/validated system (and I know the C code very well, worked on the parent it forked on for a couple of years. Which just happens to be James Gosling's first C code base with a bytecode interpreter :-).
One additional comment on "Worse is Better": Java is an unique? modern example of a "Right Way" system winning, so the "why" would be worth looking at. Ditto the story of Clojure's success, built on top of the JVM.
And, yeah, WRT to what seL4 provides, 9,000 lines of code, a fair number of them due to oddities of the hand translation from Haskell to C, isn't going to do much for you, I know it's just the start. But a porting project, and then getting it to do something (blink lights via GPIO or whatever) is for me a good way to start working my way up the stack, learn ARM, etc.
Thanks a lot for this discussion and giving me hope WRT to intermediate ways to address the web browser problem!
https://www.dreamsongs.com/Files/worse-is-worse.pdf
The other stuff you mention are good for the time. Extra props for getting work done in direction of LISP machines. I could see that I'd have enjoyed using that system besides the odd quirks you mentioned. Plus, the name of the network is way cooler than the other guys'. ;)
re Magnus/ML. I had CakeML in my collection but didn't know about Jitawa + Milawa. I remember skipping it seeing "verified lisp" in abstract while rushing through ACM/IEEE stuff and thinking "I already have VLISP so who cares." However, I appreciate your link because Milawa was a great find: an answer to the "Do you trust the prover?" question that people keep asking. Plus, Jitawa verifying a LISP and it were a nice combo. Knew Magnus was smart but that's extra smart.
Anyway, looking at your update, I see CakeML now has a verified compiler and other cool stuff. I might stop recommending FLINT except for diversity. CakeML seems to be the one to build on with VeriML too limited imho: a portable compiler & runtime is always better than an interpreter for Getting Shit Done (TM). So, I appreciate that link.
Your HOL work might be tricky. I'll be interested in hearing your experience later as it will inform how other software/systems people might fare. If it's difficult or even before you start, you might want to check out Chlipala's methodology here:
http://adam.chlipala.net/cpdt/
It's more like the FLINT style than HOL. He's produced many solid works with that. His site (link on top) also has interesting tools for various use cases: Bedrock (verified assembly), Ur/Web (correct-by-construction web apps), contribute to Ynot (writing/verifying imperative code), and so on. What they built with it is obvious from descriptions. Their pace has been faster than full verification groups while knocking out lots of errors. There's also more investment of academic brains into Coq theorem prover so each work might benefit from others.
Now, a link to help you with what you're actually doing. The seL4 work at some point referenced this book on using Isabelle/HOL for verification. Might be what you need to learn it all. I'd try it first. Stay on it if you're able to do real stuff w/ projects you referenced. Otherwise, backtrack to try Chlipala's methods.
http://concrete-semantics.org/
re browsers. Yes, they're critical for reasons you mentioned. There's a simple solution, though, which I used for years: physical separation w/ KVM switches and guards for information sharing. The browser stuff runs in a PC that handles it. Most of key work or trusted data on other system. The content is translated to formats that make verification easier or at least where you have trusted programs. The guard mediates flow of data to ensure files move back and forth without attacks on memory or transport. It's built as strong you can make it. KVM and drag-n-drop software make it easier to use. Tenix's Interactive Link is an implementation that's very similar.
re Worse is Better & Java. I semi-agree. Java is a horrid platform that was successful for these reasons: (a) similarity to existing, mainstream languages, (b) tooling in form of IDE's + libraries, (c) perceived advantages, and mainly (d) massive money in marketing by huge, enterprise firm. So, the strategy worked. Google, Mozilla, and Apple are all using the strategy with effectiveness. One needs deep pockets plus major connections to consumers and industry, though. Meanwhile, Python and Julia are examples (for me) of The Correct Thing with enough traits to make them successful despite lack of millions in funding, widespread industry support, etc. So, there's that approach too. Still an open topic where I have no definite answer.
re seL4. Good luck on the ARM, kernel, and HOL learning projects. Will keep you busy for some time I imagine with make a few less hairs on your head after righting with hardware and kernel-level issues. ;)
"Thanks a lot for this discussion and giving me hope WRT to intermediate ways to address the web browser problem!"
You're welcome and thanks to you, too. It's been an interesting one. Do give me feedback on the Concrete Semantics and Isabelle stuff later so I can assess minimal level of talent that can use it.
Just logically separating administrative VMs with credentials from email VMs would have been good enough to thwart this. We can always fork Qubes and play around with whatever other VM templates such as OpenBSD, seL4 x86/genode port or experimental encrypted overlay kernel.org kernels
"We can always fork Qubes and play around with whatever other VM templates such as OpenBSD, seL4 x86/genode port or experimental encrypted overlay kernel.org kernels"
That's true. It's why I found the seL4 and QubesOS work interesting. Additionally, as they showed up, I've suggested various projects to those interested in improving QubesOS assurance. These included capability extensions for Xen, the Xenon project, several projects that knock risk out of Dom0, components like Nitpicker, and so on. To be clear, I don't see QubesOS as worthless or all bad so much as redundant in some ways, weaker technologically in others, and a vast usability improvement in yet others. Use and improve it if you want for sure with definite benefits over a vanilla Windows or Linux box. Just know the limitations of the security approach and that efforts might be better spent elsewhere.
Here's a recent report on the 2005 Nizza architecture's design along with other projects that built on it if you're curious what it was like. Notice how they understood where the software risks were, systematically eliminated what they could, and kept metrics on the TCB to back it up. On other end, I couldn't even get Joanna to agree user-mode drivers were more robust despite a decade plus evidence of this.
https://os.inf.tu-dresden.de/Studium/KMB/WS2014/11-Security-...
At some point, Ph.T. saw all that and asked about it on the QubesOS mailing list only to get our claims and their location in a comment section dismissed. That prompted my reply to the mailing list and argument that followed. That there's 250,000+ people lurking there for good information was why I put much of my design info there instead of my own blog.
For now, I email the .txt files with the links and what posts I've pulled to whoever is really interested. Send me an email at the address in my profile and I'll return a [substantial] subset of my designs/essays along with a sample framework for high security.
Including making sure that some moron doesn't keep his password on a post-it note on his monitor.
http://ssrg.nicta.com.au/projects/TS/SMACCM/
They also released a formally proven real-time OS.
Homepage: https://sel4.systems/
Github: 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/
Also, the link 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 (where the claims are far more measured).
"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.
Also, saying a piece of software is "unhackable" is akin to saying a ship is "unsinkable".
Unfortunately, it's true that might not be enough to prevent attacks in some settings. For example, see Govindavajhala and Appel's "Using Memory Errors to Attack a Virtual Machine".
https://www.cs.princeton.edu/~appel/papers/memerr.pdf
In this case, they show that even given correct software safety guarantees, they can write a program which requires only one bit flip in any of a large number of RAM locations in order to achieve privilege escalation or violate the safety guarantees. They can then heat or irradiate the DRAM chips and make such a bit flip likely to occur. Since they can't control which bit will flip, it might sometimes crash the computer, but it's more likely to make their attack succeed.
So, one thing to study with systems like this is whether hardware fault injection can compromise the security guarantees in a way that would allow an attack to succeed.
The problem, if not specific attack, has been known a long time. The Tandem NonStop architecture assumed that its memory, I/O, and key components could fail. So, they designed system to work correctly regardless plus linear scaling of resources. My proposal was to integrate above technologies with older, non-patented version of NonStop for high security and availability.
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?
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.
https://web.archive.org/web/20130718103347/http://cygnacom.c...
[1] http://lukemuehlhauser.com/wp-content/uploads/Bell-Looking-B...
[3] 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.
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.
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.
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:
seL4 is found here:
CertiKOS, VeriML, and other FLINT work here:
http://flint.cs.yale.edu/certikos/
Termite Driver Synthesis here:
https://github.com/termite2/Termite
CompCert here:
A how-to on certified programming that's more accessible for newcomers:
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?