Robigalia: seL4 and Rust
It&#x27;s the same foolish concept people have been reinventing since early secure UNIX&#x27;s hosted on security kernels. Long story short, it was impossible without breaking applications and lots of staff back when UNIX had &quot;dozens&quot; of system calls. It&#x27;s not going to work this time.<p>The solution high assurance security adopted was to virtually or physically isolate a UNIX&#x2F;Linux stack that interacted with security-critical software that ran directly on microkernel and through mediated interfaces. This resulted in commercial work like INTEGRITY-178B and LynxSecure with Nizza, Perseus, and OKL4&#x2F;OKLinux in OSS space. Look up &quot;Mikro-SINA VPN&quot; (yes with a k) for great case study. Middleware like Camkes was developed for integration. Similarly, kernels like INTEGRITY and PikeOS developed safe&#x2F;secure runtimes that ran directly on kernel for Ada and Java.<p>What this project and all others like it need to do is this:<p>A. Drop all efforts at rebuilding UNIX in language X.<p>B. Get a user-mode version of Linux running on it with user-space drivers on microkernel for one, easily-acquired board.<p>C. Redirect safe language efforts on creating a secure runtime on the microkernel.<p>D. Create middleware tools along lines of Protocol Buffers, ZeroMQ, or LANGSEC stuff. These should allow seemless, efficient integration between untrusted (esp GUI) stuff in Linux VM and trusted stuff in safe lang uage runtime.<p>E. Begin on a POSIX-like runtime whose components can be stripped on a case-by-case basis. Focus on syscalls used by critical libraries and services first.<p>F. The current goal of full POSIX. 99% dont make it to E. If they get here, then great. If to E, then we get at least some apps. If to C and D, then we at least have trustworthy runtime.<p>That&#x27;s my two cents worth and builds on what&#x27;s historically happened in these efforts.