Why is it all in the kernel?
lawrencecpaulson.github.io84 points by ibobev 6 days ago
84 points by ibobev 6 days ago
Proof assistant kernel, not operating system kernel - in case, like me, you clicked in hoping to debate the merits of microkernels vs monolithic:) Although I suppose there is a significant analogy, since the argument here... if I understood right... is very close to the classic 'and now a small defect in a device driver just panicked the system or gave an attacker root', just in math terms.
Ha, I actually wrote a paper pushing on this "kernel" pun between OSs and proof-checkers [1], designing a HOL kernel structured like an OS kernel.
[1]: https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...
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.
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.