Why is it all in the kernel?

Post by jubilanti » Wed, Aug 05, 2026, 1:05 PM UTC

inigyou wrote: post #29

ajb wrote: post #17

Earlier quoted context omitted.

The one thing that gives me concern in their is "nanoda [the external proof checker] is [now] tracked daily". Although that would have caught this issue, we also now live in a world in which some model is going to think that hacking the proof-checker distribution is the obvious way to obtain the proof it is after; I expect that attempts on that will be much more common than soundness bugs. However, this is said witho…

This used to be the bane of all machine learning experiments. It might have been lost to time but I once stumbled upon a big list of AI reward-hacks like this. Things like - we tried to develop fast cars, but the AI just made a really tall weighted stick that would fall over onto the finish line. And we tried to teach the AI not to lose in Tetris, so it hit pause whenever it was about to.

Post by inigyou » Wed, Aug 05, 2026, 2:22 PM UTC

eru wrote: post #32

inigyou wrote: post #26

Earlier quoted context omitted.

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.

Post by [deleted] » Wed, Aug 05, 2026, 3:27 PM UTC

inigyou wrote: post #26

__s wrote: post #23

Earlier quoted context omitted.

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.

Post by phendrenad2 » Wed, Aug 05, 2026, 6:53 PM UTC

yjftsjthsd-h wrote: post #2

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.

Post by inigyou » Wed, Aug 05, 2026, 11:05 PM UTC

eru wrote: post #38

inigyou wrote: post #36

Earlier quoted context omitted.

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?).