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.
‘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.
2 replies →
> Theo de Raadt would spin in his grave
Isn't he still alive?
1 reply →