microkerneldude

4 ms·

1. 1.▲
   by microkerneldude 2y ago

   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
2. 2.▲
   by microkerneldude 2y ago

   the talk link will appear as soon as Everything Open uploads it
3. 3.▲
   by microkerneldude 6y ago

   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 battle between t
4. 4.▲
   by microkerneldude 6y ago

   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 the management/
5. 5.▲
   by microkerneldude 6y ago

   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 be pretty se
6. 6.▲
   by microkerneldude 6y ago

   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 regular use