I used to promote these architectures. They assumed two things: (a) hardware was trusted and (b) TCB was written securely. The problem is that attackers are finally hitting hardware in ways that bypass software protections. They’re all over it. The Genode TCB was also written in C++. One article shows an Ada port in progress. Should’ve used Rust this time given its temporal safety, maturity, and massive ecosystem.
Hopefully, Genode keeps improving into something that gets uptake. What will definitely come out of it is Genode’s developers will be worth high, six digits for how thoroughly they know every layer of the stack. It’s impressive how much stuff they’ve clean-slated vs reusing legacy options from UNIX’s world.
Btw, anyone interested in this might be interested in high-assurance, separation kernels (pdf) that inspired their approach. Well, theirs comes from Nizza Architecture (pdf) inspired by SK’s. Then, there’s application of these principles to hypervisors such as NOVA, Muen, and mCertiKOS. The CertiKOS people are part of DeepSpec that tries to address my complaint about hardware, too.