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/LionsOS/ – not yet verified, but will be.
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 networking equipment, it's always a…
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 system in its TCB. What Xen has over seL4 is…
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 if you get that right, your system can…
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. Deployments: There are seL4-based devices in…
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/LionsOS/ – not yet verified, but will be.
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 networking equipment, it's always a…
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 system in its TCB. What Xen has over seL4 is…
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 if you get that right, your system can…
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. Deployments: There are seL4-based devices in…