Hacker News Reader

Comment by gherkin0 | Hacker News Reader

Yes.

One project is SeL4, which is a provably correct microkernel. I listened to a talk by one of the developers and it sounded like they were getting funding from DARPA.

https://sel4.systems/About/seL4/

I also remember reading on Wikipedia about some proprietary closed-source OS that's used by the US government to work with very highly classified information. Apparently the requirement was that the kernel and every program be formally verified, so it had very limited features. IIRC, it still maintained, but newer versions support a Linux environment for less classified work.

Unfortunately, I don't remember what it was called so I can't link to the page.

edit: found it:

https://en.wikipedia.org/wiki/XTS-400

https://en.wikipedia.org/wiki/Trusted_Computer_System_Evalua...

> Examples of A1-class systems are Honeywell's SCOMP, Aesec's GEMSOS, and Boeing's SNS Server.

View on HN

Always good to see someone familiar with them. Unfortunately, NSA is transitioning to some new program that allows rapid certification of COTS security products at what looks like EAL1 and in IIRC about 90 days. Great for time to market and COTS acquisition but bad for security.

Fortunately, DARPA, NSF, and other organizations are funding a lot of good work. Here's a few:

http://www.crash-safe.org/

https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/

http://www.cs.rutgers.edu/~santosh.nagarakatte/softbound/ (See hardware papers like Hardbound and Watchdog)

http://safecode.cs.illinois.edu/sva.html

http://scholar.lib.vt.edu/theses/available/etd-10112006-2048...

Much of Galois Inc's work is government funded. That includes CRYPTOL language, Ivory language, Xen work, Haskell work, and so on. NSA partly funded demo's from Praxis (now Altran) on their Correct by Construction process with Z specs and SPARK Ada code. They built SPARK, too.

So, lots of stuff going on that is already practical. There's even more that are academic prototypes or exist in simulation. Leaving them off for now.

The problem is that at a certain level of government, you will have administrators who aren't technical experts and who have no interest in deferring to the opinions of technical experts.

Such folks just don't want to bother with the limitations that a secure system implies, even if such a system became much more featureful than the present ones. They want their Windows/Mac and probably want it for their work-groups.

It's not just a lack of technical know-how but a variety of psychological tendencies that stands against this. It's taken a long time for companies to develop UIs that people want to use but the existence of these "easy to UIs" is a barrier to any UI which requires even a small amount of training to use.

So? Hiring a UI expert to do a trivial amount of user testing is basically all that's required. You don't need to turn something into Windows to make it usable. As long as the basic activities are relatively painless, people have zero problem using an archaic system.

Order a report and make a revision. Repeat a couple times if you have to.

Fine. Then those people don't get access to secure systems or information that needs to be secured. Just don't let them have any kind of job that means they need to work with information that should be secure. Let them have their Windows/Mac machine, and let them work on writing Word docs and Powerpoint about stuff that nobody cares about.

Unforunately that's not how government (or any large institution) works. That person has enough political capital to hold onto that job, or probably they wouldn't have obtained the job in the first place. Try firing or moving them and you might find that someone powerful, whose good will you need in order to get important things done, will be unhappy with you.

Just don't let them have any kind of job that means they need to work with information that should be secure.

No, you don't understand that "those people" are in charge of the American state already. This is what the ruling elite looks like, not geeks or technical experts - lawyers, business school grads and ideologues generally. No one else is going to tell them they don't get access ... because they are in charge.

Hillary Clinton's email server and Sarah Palin's hotmail account were both symptoms of this.

Secure systems are much more than just a verified kernel or userland.

None of that matters if you are using it in a modern processor full of backdoors and malicious technologies like AMT/IME/PSP.

You mean like the kind of highly classified information that Hillary Clinton kept on her home server? :) was she running a probably secure microkernel?

Not a provably secure microkernel, nor even a probably secure one. Nor, probably, even a microkernel at all.

Might have run on a Windows NT variant. That was sort-of supposed to be a microkernel.

Reply on news.ycombinator.com