4 ms·

provably-correct microkernels like seL4 are popular for "cross-domain solutions" that simultaneously handle unclassified and classified information while ensuri

provably-correct microkernels like seL4 are popular for "cross-domain solutions" that simultaneously handle unclassified and classified information while ensuring separation. NSA requirements for such systems are strict and right now most of the options are commercial, like BAE XTS-400. More defense contractors are looking towards seL4 and the NSA seems to be encouraging it for the benefit of a shared, open-source platform across these specialized projects. I believe seL4 is also used for the firmware on Qualcomm modems now, but it's a little hard to follow if they've switched from OKL4 which was a related project.

sterlind 3y ago
I thought commingling classification/user clearance levels on the same hardware fell out of favor a while ago, because of side channels (with speculative execution being the final nail in the coffin.) Isn't seL4 more used for things like data diodes, cryptographic equipment and military hardware? Stuff that you need to keep from getting hacked or malfunctioning, but not time-shared with untrusted users.
- Veserv 3y ago
  Nah, multilevel security fell out of favor because no large commercial vendor could do it. They retracted the requirements over a decade ago because it prevented Microsoft and IBM from bidding on government contracts to “secure” their infrastructure.
  - kjs3 3y ago
    Well, Microsoft made some half-assed runs at Orange Book compliance (e.g. Windows NT without floppies/CDs...or networking), but Trusted AIX was a real thing with real users. Having been involved in a couple of MLS Unix implementations, IMO it didn't fall out of favour because no vendor could do it, it fell out of favour because no one could effectively run it in production. The admin overhead of a 'real' TCSEC validate system is formidable, and at some point someone decided 'useable with admins with 6 months of training (e.g. privates and corporals)' was more important than 'checks all the boxes', and the boxes that needed to be checked changed.

sterlind 3y ago

I thought commingling classification/user clearance levels on the same hardware fell out of favor a while ago, because of side channels (with speculative execution being the final nail in the coffin.) Isn't seL4 more used for things like data diodes, cryptographic equipment and military hardware? Stuff that you need to keep from getting hacked or malfunctioning, but not time-shared with untrusted users.

Veserv 3y ago
Nah, multilevel security fell out of favor because no large commercial vendor could do it. They retracted the requirements over a decade ago because it prevented Microsoft and IBM from bidding on government contracts to “secure” their infrastructure.
- kjs3 3y ago
  Well, Microsoft made some half-assed runs at Orange Book compliance (e.g. Windows NT without floppies/CDs...or networking), but Trusted AIX was a real thing with real users. Having been involved in a couple of MLS Unix implementations, IMO it didn't fall out of favour because no vendor could do it, it fell out of favour because no one could effectively run it in production. The admin overhead of a 'real' TCSEC validate system is formidable, and at some point someone decided 'useable with admins with 6 months of training (e.g. privates and corporals)' was more important than 'checks all the boxes', and the boxes that needed to be checked changed.