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…
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…