Viewing profile — microkerneldude

seL4 is a bit more than a hypervisor, but it's definitely very low-level. In terms of a useful seL4-based system, you may want to look at https://trustworthy.systems/projects/Lions…

the talk link will appear as soon as Everything Open uploads it

Simpler versions of such devices exist, eg HENSOLDT Cyber markets a secure VPN gateway that is built on seL4. Over the years we've been in on-and-off discussions with vendors of ne…

In terms of security, the answer is a clear yes. Xen is kernel of 100+kSLOC of unverified code, while seL4 is verified. On top of that, Xen has Dom0 and thus a complete Linux syste…

Re scalability of verification: you don't have to verify everything to get a massive security/safety boost. A well-structured system has a small trusted computing base (TCB), and i…

Thanks for featuring my white paper. Some responses to some of the comments. "Opinionated": guilty as charged. However, I claim that the opinions are well-grounded in fact. Deploym…