2 ms·

I am certain that seL4[0] is the way to go, as it is the only way to have the guarantee (formal proofs) that there's no getting around capabilities. 0. https:/

by snvzz 4y ago

I am certain that seL4[0] is the way to go, as it is the only way to have the guarantee (formal proofs) that there's no getting around capabilities. 0. https://sel4.systems/ https://sel4.systems/

mikewarot 4y ago
seL4 is a kernel, not an operating system. Genode builds upon it, which is where my hope currently resides.
- snvzz 4y ago
  Sure, but my point is: You need seL4 underneath to build a system with actual capabilities. Nothing else can be trusted. (and non-seL4 would be slower, anyway ;)