MIT Panel: Provably Secure: Math Against Superintelligent Hackers

This post is crossposted from my Substack, Structure and Guarantees, where I explore how formal verification and related ideas might scale to more complex intelligent systems. Here I set the stage for a panel I’ll moderate at MIT, on the potential for formal verification to defend against a set of related cybersecurity risks from highly capable AI.

This week, I want to announce a panel I’m moderating at MIT. It’s on the subject of how formal verification can help against cybersecurity threats by increasingly powerful AI systems. It will take place on Tuesday, November 17th, at 4:30 PM, followed by a 5:30 PM reception, in MIT room 32-155.

This event is run by our College of Computing, and please visit their web page for the event if you would like to register for free. Registration, open to the public, is only for in-person participation. There is no livestreaming online, though we will record the panel and post a video online, not too long after the event.

The Panel and the Panelists

Worry is growing around AI agents escaping containment and acting against the interests of the organizations that built them. The latest LLMs are also finding cybersecurity vulnerabilities in important software at an alarming pace. This panel surveys an old computer-science technique with new promise: formal verification, mathematical proof about the behavior of programs. Can such proofs be applied to important computing infrastructure, to guarantee agent containment and find all security bugs of certain kinds, future-proofing against more-powerful LLMs? Our discussion brings together experts on the topic from across academia, government, and industry. We hope to hit on topics of interest both to experts in this technical field and to a broader audience concerned with policy and other strategic questions.

Our panelists:

Byron Cook started his journey through formal verification with PhD work in formalizing the interface between CPUs and software. He then worked for many years at Microsoft Research, where he made important contributions in model checking, one of the first formal verification approaches to be scaled for serious industry impact. In 2014, he took a leap of faith, joining Amazon Web Services to lead a new effort in applying formal verification throughout the organization, to improve cybersecurity and system reliability. The project succeeded beyond all expectations, with formal methods now woven deep into how AWS builds and operates, increasingly paired with AI to prove the correctness of systems at scale and AI itself. The AWS Automated Reasoning Group, founded by Byron in 2016, contributes across many business units to strengthen internal systems and build tooling that makes it easier for other organizations to apply formal verification, probably the largest buy-in to diverse formal verification by any company.

Noah Evans started his research career in systems software and high-performance computing at IBM and Bell Labs. Later he joined the new formal-methods team being spun up at Sandia National Laboratories, one of several U.S. national labs charged with securing the nation’s nuclear stockpile. The team found great success proving correctness and security of hardware and software, including in several projects he led, with the team growing into one of the largest in formal methods in U.S. government-adjacent organizations. He recently moved to Draper Laboratory near MIT, continuing to lead efforts applying principled techniques to cybersecurity in national defense.

Armando Solar-Lezama did undergraduate research in high-performance computing and started exploring formal methods in his PhD work, where his thesis reinvigorated the area of program synthesis, generating code from its mathematical requirements. In particular, he and his collaborators introduced the technique of program sketching, where automated tools fill in gaps left in code. He then joined the computer-science faculty at MIT. After quite some time making the case that “this stuff can really work,” the generative-AI boom made that point clear to everyone, and Armando has been helping make sense of the relative strengths and weaknesses of machine learning and logical methods, to create the next generation of tools that combine the two.

There will be plenty to talk about, not just recapping the big ideas of formal verification before the rise of AI agents but also considering whether the same techniques can help deal with AI as cyberattacker and AI as system that we want to confine safely or otherwise control. Another key question is how to build confidence in formal specifications to check against code written by agents that may understand computing better than we do. The panelists bring nicely complementary backgrounds in terms of application domains and technical approaches, so I expect some great words of wisdom to be uttered.

I’ll be happy to consider your suggestions within the comments to this post, on questions to ask during the panel.

What I’ve Written on this Topic

The panel will be focused on what the panelists have to share, but I can still include a little outline here of my own related articles!

Let me start with cybersecurity. I explained how applying formal verification to complex systems brings immediate security benefits, even subject to standard gotchas like concerns of choosing the right specifications to prove. I made my version of the case that AI-powered attackers will be so good at finding bugs that we can no longer depend on vulnerabilities staying secret, leading to a recommendation that we get used to rewriting all the code, all the time, taking lessons from databases in how to write unambiguous specifications and generate code from them automatically and reliably. We should move quickly, since we’re in easy mode now, where AI agents “think” relatively similarly to how humans think, which shouldn’t be expected to last for long.

I’ve had a lot to say more broadly about formal verification, starting with presenting it from an evolutionary perspective and sketching applications to safe recursive self-improvement and paranoid AI agents exchanging software code with each other. One big message is the value of end-to-end formal verification, where, ironically, we can derive stronger mathematical assurance in systems by proving even more of their parts, where one might think that writing more lines of specification and proof just increases opportunities for mistakes. Considering the question of superintelligent AI and how we can set it up to interact safely with us, I proposed autonomous evidence factories as a model with a central role for formal verification. I’m also in the middle of a sequence of articles on how to derive good code automatically with proof of correctness, through series of small proven rewrites, with examples so far in high-level software, hardware, and low-level software.

Coming Up

We’ll return to that sequence next, with a pair of posts going into more detail on the classic theorem-prover data structure the e-graph. My prior article gave an example of a programming domain where after-the-fact correctness checking of program rewrites was relatively tractable to do automatically. E-graphs are one of the best-known tools used in such checking for more-complex programs. Next week, we’ll look at how they work, and the week after we’ll look at an application in compiler correctness. Then I’ll add one more example of deriving proven C programs step-by-step, before stepping back to consider what kind of unifying architecture helps divide up code-generation work for larger projects across these techniques, while requiring minimal trust in tool implementations.