Keynote: AI for formal verification; formal verification for AI

No ratings

Presented at Code Blue 2024 by

David Dalrymple

For over a decade, it has been known that formal verification workflows are sufficient to create software that is free of exploitable bugs. It also appears to be necessary. AI systems are increasing rapidly in their ability to assist in these workflows, and to make them accessible to increasingly less specialist engineers. While AI can also assist with many other workflows, formal verification in some form still seems to be necessary to make AI reliable enough to provide a net benefit to cybersecurity. AI could also be used to formally verify at other levels of abstraction than functional correctness, from the concurrency of distributed systems down to the electromagnetics of the hardware. In a small number of years, this will vastly expand the scope of what can be considered “practical” to formally verify, and most forms of cyberattack will become history. At the same time, formal verification and cybersecurity have crucial roles to play in ensuring and assuring that increasingly powerful AI systems do not go rogue and cause a global catastrophe. Our future could be bright, but our communities need to work together.