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.
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?
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.
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).
They also have 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 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).
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.
It seems like, in light of the mathematical proof, it may be reasonable to say "does not contain exploitable software vulnerabilities".
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".
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.
This is why you address system security holistically. There are countless projects that sprang from the Aegis processor that address the fact that RAM and devices aren't trustworthy. One had the start of an EAL7 argument for security of software from all those attacks via the hardware mechanism without modifying the processor's internal RTL. Another shows security of information flow of a design down to the gates. Others are about just synthesizing correct designs that arbitrary parties can produce for a fab and composing them into a trustworthy system.
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.
It looks like their website has been changed. I started writing a Pull Request to fix the README links for the FAQ and Contribution guidelines, but actually printing, signing and scanning a CLA put me off.
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.
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.
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.
Huh, I'm surprised I'm seeing this first in a HN comment.
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.
That's because Joanna is against it and will aggressively defend their platform choice. After our argument online [1], she posted this essay [2] comparing QubesOS to other things. She censored my piece-by-piece counter, too, lol. She did eventually do something with trusted path and mentioned QubesOS could be ported to different platforms. So, there's some progress... Honestly, it wasn't clear whether she really understood INFOSEC (esp TCB concept) based on her replies so I avoid QubesOS.
I remember one good argument she made, a reductionist one that if the firmware on your Ethernet adapter can be hacked without recourse or relief from the OS (she gave a specific example), reducing the Xen part of TCB was not too relevant.
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 firmware. It's true and orthogonal. Just as the DARPA project is doing, you use the best tech and method for each part of the job. The recommendations I gave her were for kernel up mainly for isolation. Drivers should be written robustly, synthesized, use trusted hardware, and/or mediate the hardware.
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.
My complaint about browsers is less about architecture (I mean, when using multiple processes is a vast improvement of the state of the art on the ground...), than what I gather is the vast amount of work required to get today's standard web pages to render well.
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.
Oh I see what you mean. Yes, it's become an oligopoly with a huge barrier to entry. The typical solution is to separate all these components with safer implementations, isolation, and/or interfaces. What I referenced do those. If you want to solve it directly, you have to make the code trustworthy. That's... another matter entirely.
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 few more thoughts, without having looked at your references or even having more than a vague idea of the (necessary) architecture of browsers (it's fiddly front end stuff I don't like all that much as a domain), and for that matter at this point I'm just looking at all this because I don't like how things are, how they've developed since Multics and the Lisp Machine (the latter, admittedly not a secure system), and looking for what to try to do next with my life:
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!
"it's fiddly front end stuff I don't like all that much as a domain"
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:"
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:
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.
Experience/skillsets: "SCIENCE!", but because $$$ ended up doing systems and software, mostly backend with the occasional GUI, C, C++ (have sworn off of), Perl (ditto), the various Lisps, esp. functional programming, going to look at ML next. A bit of kernel, embedded, or akin experience, e.g. a MS-DOS TSR filesystem. UNIX(TM) since 1978. Also see https://www.linkedin.com/in/haroldancell
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 ha...
Interesting background. You worked on a bit more interesting projects than me as mine were limited by spare time and cash. Anyway, how would you explain to someone who learned computing in the 90's why ITS was an excellent design vs UNIX? Does the Wikipedia article cover it? Was some amazing features given the time period. I remember there were references to it in the UNIX Hater's Handbook, too. Their crash-proofing strategy was ingenius, too. Doubt it would work with today's trolls but good for that crowd.
"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 uniq...
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:
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.
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,...
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
The article states that he's just guessing at what happened leading up to the fraudulent request. (If I'm reading right.) So, no way to know what would stop the first part. The actual attack was a common one where a request comes in without strong authentication and an authorized user carries it out. Neither QubesOS nor any other low-level architecture I mentioned would stop that as it's an application-layer concern. There's a little irony in your comment, though, given that one of the Nizza demonstrators in mid-2000's was doing eCommerce by splitting the UI and security critical parts over a microkernel. Did that for GPG email, too. So, even they recognized the problem and demo'd a two-part solution. I sent that to Joanna in our exchange.
"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.
I'm not sure. Ph.T. apparently followed both the Schneier's blog discussions and QubesOS mailing list. We were discussing many methods of using separation kernels for desktops, security appliances, inline-media encryptors, VPN's, and more. Going through details for a year or two.
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.
I enjoy reading your comments here at HN. Would you care to provide a link to your blog? I understand if you would like to keep the personas disconnected.
Why thank you! :) Your profile was an amusing read, too, haha. I don't maintain a blog: post on high-profile one's like Schneier's instead to get good techniques out there to wide audience. Reference copies stay there due to host's integrity and good peer review with me keeping links to many. I've been pulling them into local copies gradually to turn into a web site which will be powered with medium assurance tech at a minimum (esp my blog/comment signature scheme). Practice what I preach & build on it sort of thing.
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.
Running on L4 family's work is one option I suggested to QubesOS team years ago. Nice to see someone trying. It will tricky with seL4 as they have embedded focus and QubesOS is a desktop OS. I'm sure the requirements, obstacles, and fixes will make for enlightening reading for anyone doing similar projects.
Gödel's Incompleteness Theorem might be abstractable to this. Any system so inaccessible as to be unhackable might be functionally impaired beyond usefulness.
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.
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.)
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.
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.
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.
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.
(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.
"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 :)
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:
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:
65 comments
[ 2.9 ms ] story [ 74.4 ms ] threadI 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?
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.
http://dl.acm.org/citation.cfm?id=2560537
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:
* https://www.youtube.com/watch?v=YqRdbgRPYw8
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...
http://sel4.systems/pipermail/devel/2015-March/000312.html
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.
https://news.ycombinator.com/item?id=9969961
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 d...
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 ha...
"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 uniq...
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,...
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.
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.
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...
[2] http://aesec.com/
[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.
https://news.ycombinator.com/item?id=7938149
[1] https://news.ycombinator.com/item?id=10237636
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/
seL4 is found here:
https://sel4.systems/
CertiKOS, VeriML, and other FLINT work here:
http://flint.cs.yale.edu/certikos/
Termite Driver Synthesis here:
https://github.com/termite2/Termite
CompCert here:
http://compcert.inria.fr/
A how-to on certified programming that's more accessible for newcomers:
http://adam.chlipala.net/cpdt/