points by cowlevel 1 day ago | 0 comments
You still have to draw the rest of the owl though. A proven secure starting point is neat but it's not actually the system you want to build.
[–] snvzz 1 day ago
[–] cowlevel 21 hours ago
Front page of HN today: a full exploit chain in Microsoft Edge using only logic bugs. seL4 would not have prevented this: https://news.ycombinator.com/item?id=50285319
[–] snvzz 20 hours ago
It would have prevented it. e.g.
>Of course, you’d want to try ../… Yes, it does let you escape the temporary folder...
This is absolute bull on seL4 by construction. "sandboxes" that prevent access that the OS otherwise grants. In seL4, this component would not need a sandbox in the first place, because it would never have a capability to some VFS path it doesn't need to access.
This sort of escape relies on ambient security, which is the security model of UNIX and Windows NT. Access is granted by default and then restricted, rather than simply not granted. A broken security model.
And, unlike a demonstrated shitty browser sandbox, seL4 formally guarantees isolation. Capabilities cannot be forged.
seL4 is the choice that allows for a safe system to be built. Any other choice of kernel currently available does lack the mechanisms and guarantees.