Hacker News
points by snvzz 2 days ago | 0 comments
>You can point an LLM at any large codebase and it will find vulnerabilities, so "patch the planet" isn't very scalable.

So the solutions need to be structural.

e.g. relative to a monolith kernel, seL4 is small, has no known bugs (AI can try, but so far crickets) and is the only piece that needs to run privileged.

Everything running under seL4 benefits from the guarantees seL4 provides.

[–] Good4boothee 2 days ago
The solution needs to be convenient, in practice that trumps security every time. If i need to run my existing apps in Linux VM under seL4, others, fully featured hypervisors will look more enticing.
[–] yangm97 1 day ago
Genode appears to be very convenient if you are looking into a way to run microkernels for general purpose computing.
[–] cowlevel 1 day ago
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
It is only possible to draw the rest of the safe owl if you have a safe crayon.

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.

[–] 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 21 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.