[nickpsecurity]

There's quite a few that's been developed in both business and academia with some deployed. NSA didn't do shit except maybe backdoor the closed ones. Genode.org is one of better-structured one's that's FOSS and usable today. Build on it.

You can also negotiate source from one of the separation kernel vendors, compile it on target of your choice, and port L4Linux (user-mode Linux) to it to keep legacy apps. CHERI processor and CheriBSD are open source. EROS source was published and could be extended. JX Operating System has almost everything under JVM's safety protections with relatively small TCB. Cool tools like Softbound and Astree knock out bugs in what's left.

There's many tools to start with to get smaller, strong TCB's. They're just the only one's the open-source community doesn't work on. Tiny, tiny set of exceptions. People not wanting to worry about it can just build on Tinfoil Chat: largely eliminated TCB with clever use of data diodes and physical separation. A Moxie-coded version of that portable to arbitrary embedded systems could be made NSA-proof. So, there's options for anyone wanting to get started.

Meanwhile, I'll keep using GPG on airgapped machines with diverse hardware and interface protection. Only thing that works per Snowden leaks. For now...