3 ms·

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

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/ 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/XTS-400 https://en.wikipedia.org/wiki/Trusted_Computer_System_Evaluation_Criteria#A_.E2.80.94_Verified_protection 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.

chatmasta 11y ago
You mean like the kind of highly classified information that Hillary Clinton kept on her home server? :) was she running a probably secure microkernel?
- AnimalMuppet 11y ago
  Not a provably secure microkernel, nor even a probably secure one. Nor, probably, even a microkernel at all.
  - eru 11y ago
    Might have run on a Windows NT variant. That was sort-of supposed to be a microkernel.
joe_the_user 11y ago
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.
- erikpukinskis 11y ago
  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.
- AnimalMuppet 11y ago
  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.
  - hackuser 11y ago
    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.
  - joe_the_user 11y ago
    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.
nickpsecurity 11y ago
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/ http://www.crash-safe.org/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ http://www.cs.rutgers.edu/~santosh.nagarakatte/softbound/ http://www.cs.rutgers.edu/~santosh.nagarakatte/softbound/ (See hardware papers like Hardbound and Watchdog) http://safecode.cs.illinois.edu/sva.html http://safecode.cs.illinois.edu/sva.html http://scholar.lib.vt.edu/theses/available/etd-10112006-204811/unrestricted/edmison_joshua_dissertation.pdf 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.
lolidaisuki 11y ago
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.

chatmasta 11y ago

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

AnimalMuppet 11y ago
Not a provably secure microkernel, nor even a probably secure one. Nor, probably, even a microkernel at all.
- eru 11y ago
  Might have run on a Windows NT variant. That was sort-of supposed to be a microkernel.

joe_the_user 11y ago

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.

erikpukinskis 11y ago
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.
AnimalMuppet 11y ago
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.
- hackuser 11y ago
  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.
- joe_the_user 11y ago
  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.

nickpsecurity 11y ago

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/ http://www.crash-safe.org/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ http://www.cs.rutgers.edu/~santosh.nagarakatte/softbound/ http://www.cs.rutgers.edu/~santosh.nagarakatte/softbound/ (See hardware papers like Hardbound and Watchdog) http://safecode.cs.illinois.edu/sva.html http://safecode.cs.illinois.edu/sva.html http://scholar.lib.vt.edu/theses/available/etd-10112006-204811/unrestricted/edmison_joshua_dissertation.pdf 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.

lolidaisuki 11y ago

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.