For those unwilling to compromise, the stack begins … http://ts.data61.csiro.au/projects/seL4/ Easy introductions: seL4 is free: What does this mean for you? (2015) https://www.youtube.com/watch?v=lRndE7rSXiI From L3 to seL4: What have we learned in 20 years of L4 microkernels? (2014) https://www.youtube.com/watch?v=RdoaFc5-1Rk (from here: https://docs.sel4.systems/GettingStarted.html ) https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ The seL4 kernel is a burgeoning project that’s been creating a buzz in the security world for its uncompromising capability-based security model that comes with end-to-end proofs of conformance to its formal specification. It’s a microkernel, and it’s the fastest of its ilk. It says, “Security is no excuse for poor performance!”, and then backs it up. It’s open source. It’s free. It’s an increasingly relevant disruption in the Operating Systems monolith. https://research.csiro.au/tsblog/introducing-device-untyped-memory-sel4/ These invariants allow us to prove that any kernel memory access is not to a device register, no matter what the initialisation component does, and no matter whether it is trusted or not. This means, verification helped us to not only improve one specific case, but also makes sure this entire kind of problem will not re-occur, and to reduce the trust that is necessary in the rest of the system. More¦ https://research.csiro.au/tsblog/ Plenty to learn, plenty to improve (from the raspberry pi 3 link above): There is no silver-tongued way to say, that seL4 has a fairly involved build-dependency set-up procedure. We know it’s tedious, and we’re working on it. Here’s the simple description: you’ll need a compiler toolchain that can target your platform, and the “Repo” script, which is really just a script released by Google, that is a git submodule-management replacement. We use some Python scripts to generate some headers and our custom bitfield functions, so you’ll need some python modules. Slap on an XML parser which we use to generate our syscall invocation stubs, and ncurses for our “make menuconfig”, and you’re good to go. O—M—G, sounds too difficult for folks round ’ere ... ;D Hero level bonus for the significance junkie who just can't get enough and is not in need of a trigger warning, cry-in, or sky-scream: Plug in SNABB as an isolated ubermaxx performance user space network snack and build that GPL chaff-filled I2P module the world awaits with baited breath… Dang, you know you love it :)