logoalt Hacker News

est31 • today at 2:21 AM • 1 reply • view on HN

That's a fair question, and actually one I ask myself too.

AI doesn't give a strong guarantee that things work though, while Rust gives a much stronger (not absolute) guarantee.

But maybe the way of the future is to auto-generate proofs that the code is memory safe and then just leave things where they are, instead of doing rewrites that require maintainer buy ins. The advantage of C plus proofs would be that the AI generated proofs could live separately so it wouldn't touch workflows of the maintainers.

The only required output they have to process is evidence of vulnerabilities in changes proposed to them. They could outsource even that to contributors.


Replies

imtringued • today at 1:50 PM

I'm thinking a language change isn't enough... At least not for a kernel.

There has to be a pseudo userspace type of way to build a kernel driver. Basically, user space programs are fine, but kernel drivers need their own form of encapsulation without expensive context switches.

Something like memory encryption or memory access bounds. During the handoff you do not change the address space, you just restrict access to a subset of the kernel memory.

It's possible that we might need CHERI on stack pointers, specifically function arguments, because that makes it possible to grant a function access to a subset of the memory.