Hacker News Reader

Comment by eru | Hacker News Reader

Yes, the analogy might help. Though as far as I know the common OS kernel reply 'we have to stick it all in the kernel to achieve performance' doesn't apply to proof assistants.

View on HN

Yeah in theorem provers usually the opposite is true: "We want to put as little stuff as possible in the kernel because that's the part we need to verify by hand"

In an OS kernel that instinct is also true: 'we want to put as little as possible in the OS kernel, because that stuff can bring down the machine.'

That isn't true, as there are many things that can bring down the machine. If your X or Wayland server crashes, it brings down your machine.

No, that is true, even if not uniquely. A kernel bug can easily bring down the machine. Maybe Xorg can also manage it... although IMHO that also sounds like a kernel bug (surely it's the kernel's job to ensure no user program can do that?)... but that doesn't make the kernel safe. And I suspect it's easier to take down the machine from ring 0 than a display server even if both can do it.

It doesn't, it just loses your session

A kernel panic doesn't bring down the CPU, nor the hard drive, or the RAM, or the power supply unit. So if we're being pedantic, the machine is still up.

Well, a kernel bug gets write access to everything. A bug in userland is a bit more constrained in what it can do.

That counts especially for accidental bugs and denial of service. To make a userland bug exploited adversarially not impact the rest of the system requires more hardening of the kernel.

Yeah a userland bug just gets all my passwords, SSH keys, personal secrets and whatever.

Say it with me - there's no practical difference.

You are talking about a single user system.

You can compartmentalise further.

Modern processors even give you these 'rings' to help with the hardware side of that, if you want to.

Yes, these are the standard excuses. But has anyone actually thought about them in the last twenty years, in the context of the way we actually use computers?

Eh, yes? Just look the discussions surrounding the development of any web browser? Or look at the permissions system in Android or iOS or on Mac (and perhaps even Windows?).

So you acknowledge a browser bug is just as bad as a kernel bug.

A bug in the website itself is just as bad, if it's a website you care about.

They differ in how easy a fix is to develop and roll out, and what the blast radius is.

Reply on news.ycombinator.com