Hacker News Reader

Comment by achille | Hacker News Reader

Note that the SEL4 kernel is only a small portion of this project. They've secured the entire stack, top to bottom.

HACMS leverages a number of other projects including the CompCert verifying C compiler, Verve OS Theorem prover, model checkers. You also need need proofs for the communication protocol, the IP stack, secured device drivers, memory protection units, control systems that can detect attacks, etc.

Just a proven kernel won't keep the helicopter flying, you've got to secure everything. Additionally you need to reason about execution time and memory constraints.

Slides: http://www.cyber.umd.edu/sites/default/files/documents/sympo...

Presentation from Kathleen Fisher, the researcher who's won the DARPA grant for the program:

* https://www.youtube.com/watch?v=YqRdbgRPYw8

View on HN

So can you create a general purpose OS with something like this, or is it only useful for embedded stuff, like say voting machines?

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.

I know of this effort: http://genode.org/

More specifically, I'd wonder about efforts to create not (necessarily) POSIX based stuff on top of seL4 etc.

NICTA/UNSW have apparently started working on a QubesOS port

https://my.cse.unsw.edu.au/thesis/thesis_topic_details.php?I...

http://sel4.systems/pipermail/devel/2015-March/000312.html

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.

[1] http://pastebin.com/5fnh8g2S

[2] http://theinvisiblethings.blogspot.com/2012/09/how-is-qubes-...

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.

https://news.ycombinator.com/item?id=9969961

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:"

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

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

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.

why ITS was an excellent design vs UNIX

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!

It's funny you mentioned the PC losering problem because he countered his own claim later (see p3):

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.

QubesOS would have saved that Bitpay executive $2mln who fell for an old phishing trick http://www.americanbanker.com/news/bank-technology/bitcoin-p...

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.

https://os.inf.tu-dresden.de/Studium/KMB/WS2014/11-Security-...

What/Who is "@Ph.T." referring to in the linked discussion?

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.

The documentation for genode OS framework is a full free book (creative commons) http://genode.org/documentation/release-notes/15.05#Comprehe...

Interesting lecture by DARPA. It also refers to their secure UAV project, which is as anexample to embedded system:

http://ssrg.nicta.com.au/projects/TS/SMACCM/

They also released a formally proven real-time OS.

> Just a proven kernel won't keep the helicopter flying, you've got to secure everything.

Including making sure that some moron doesn't keep his password on a post-it note on his monitor.

Reply on news.ycombinator.com