I'll admit I've never played with or looked into Genode, so I can't meaningfully comment on it.
Regarding seL4, I haven't played with it but I did read their whitepaper. I believe they are setting the gold standard for microkernels in reliability and correctness. Not many systems can claim to have a formally-verified trusted computing base of not only their source code, but the binary artefacts too. This is the closest kernel project I know of that can potentially mitigate against attacks as described in the paper "Reflections on Trusting Trust" by Ken Thomson.
That is not to say that their approach is fool-proof. Like any proof, they make assumptions, which in this case is that the base hardware (CPU, MMU, memory...) does and only does what their specification claims, which the long list of erratas in Intel CPUs as well as Spectre, Meltdown, rowhammer, the Intel Management Engine debacle and others showed that they definitely don't. Not that other hardware vendors are immune too, by the way.
Their formally-verified proof is also limited to the microkernel. So while they claim to guarantee that userland processes can't compromise the microkernel nor compromise other userland processes through the microkernel (which does have its uses in embedded systems requiring high reliability), it has no bearing on what the userland does. Heartbleed wouldn't have been stopped by seL4 for example, not to mention social engineering, evil maid attacks, DMA attacks, attacks on packaging system (I lost count of the number of NPM modules that were compromised over the years), not to mention plain user stupidity.
In a way, "Reflections on Trusting Trust" by Ken Thomson has never been more relevant than today. On a typical Linux desktop operating system, we effectively blindly assume that hundreds of millions of lines of code, taken from tens of thousands of code repositories from the Internet, written in mostly unsafe languages (or languages whose interpreters/VMs are written in unsafe languages), running on a monolithic kernel with tens of millions of code written in C, running on hardware that is effectively a big black box, does what they're supposed to do and nothing more.
Even if you do audit stuff, a human can't possibly audit everything from the LLVM compiler to your web browser, not to mention we are effectively emotionally-driven, tribal-minded, chemically-influenced, prejudiced, illogical and error-prone ape brains and anyone pretending to be a perfect Vulcan is either delusional or lying.
Not to mention, I just read their whitepaper and thought to myself "yeah, sounds good". I haven't actually audited seL4, their methodology and their proof, so... As the meme says: everything is fine?
Before I trigger panic attacks, I do have to note that humans abstract away reality until we can handle it, whether it's in engineering, manufacturing, physics, food supply chains, sociology or anything else. This is effectively how our society operates: mostly that problems we don't deal with directly are taken care of by somebody else in good faith. That is not to say we can't mitigate reality if we're willing to put in the price, but except in mathematics we are never building on first principles.
> but except in mathematics we are never building on first principles
In practice, mathematicians also assume "that problems we don't deal with directly are taken care of by somebody else in good faith". We use theorems that others proved, and we trust that the authors and the reviewers did their job, without inspecting the proofs ourselves. Sometimes mistakes slip through, but they are usually caught fairly quickly, and can be fixed locally.
In other words, we are less strict than we like to think we are, but we get away with it perfectly well.
Regarding seL4, I haven't played with it but I did read their whitepaper. I believe they are setting the gold standard for microkernels in reliability and correctness. Not many systems can claim to have a formally-verified trusted computing base of not only their source code, but the binary artefacts too. This is the closest kernel project I know of that can potentially mitigate against attacks as described in the paper "Reflections on Trusting Trust" by Ken Thomson.
That is not to say that their approach is fool-proof. Like any proof, they make assumptions, which in this case is that the base hardware (CPU, MMU, memory...) does and only does what their specification claims, which the long list of erratas in Intel CPUs as well as Spectre, Meltdown, rowhammer, the Intel Management Engine debacle and others showed that they definitely don't. Not that other hardware vendors are immune too, by the way.
Their formally-verified proof is also limited to the microkernel. So while they claim to guarantee that userland processes can't compromise the microkernel nor compromise other userland processes through the microkernel (which does have its uses in embedded systems requiring high reliability), it has no bearing on what the userland does. Heartbleed wouldn't have been stopped by seL4 for example, not to mention social engineering, evil maid attacks, DMA attacks, attacks on packaging system (I lost count of the number of NPM modules that were compromised over the years), not to mention plain user stupidity.
In a way, "Reflections on Trusting Trust" by Ken Thomson has never been more relevant than today. On a typical Linux desktop operating system, we effectively blindly assume that hundreds of millions of lines of code, taken from tens of thousands of code repositories from the Internet, written in mostly unsafe languages (or languages whose interpreters/VMs are written in unsafe languages), running on a monolithic kernel with tens of millions of code written in C, running on hardware that is effectively a big black box, does what they're supposed to do and nothing more.
Even if you do audit stuff, a human can't possibly audit everything from the LLVM compiler to your web browser, not to mention we are effectively emotionally-driven, tribal-minded, chemically-influenced, prejudiced, illogical and error-prone ape brains and anyone pretending to be a perfect Vulcan is either delusional or lying.
Not to mention, I just read their whitepaper and thought to myself "yeah, sounds good". I haven't actually audited seL4, their methodology and their proof, so... As the meme says: everything is fine?