honestly LLMs could probably write drivers in CompCert C or some other formally verified dialect. having AI discharge proof obligations seems like a terrific use for all this newly-developed mathematical process.
you could have the driver code prove it implements a spec, that there's no UB, that hardware invariants are maintained, that routines take a fixed time to execute.
the formal driver spec must still be written by sober, well-caffeinated humans of course.
Then vibe up the ones you need for yourself.
‘Click to write and install driver’
> 'Click to write and install driver’
Theo de Raadt would spin in his grave — after the security implications of this to OpenBSD gives him a fatal aneurysm.
Either that, or he'll surprise-launch OpenLLM, a model bundled in the next OpenBSD release that produces driver code free of security bugs.
honestly LLMs could probably write drivers in CompCert C or some other formally verified dialect. having AI discharge proof obligations seems like a terrific use for all this newly-developed mathematical process.
you could have the driver code prove it implements a spec, that there's no UB, that hardware invariants are maintained, that routines take a fixed time to execute.
the formal driver spec must still be written by sober, well-caffeinated humans of course.
That's also assuming the device is fully documented and that hardware behaves exactly as documented.
Anyone who has done any work with hardware can confirm that neither of these things is ever true. :(
> Theo de Raadt would spin in his grave
Isn't he still alive?
> — after the security implications of this to OpenBSD gives him a fatal aneurysm.