The Great Security Update: AI ∧ Formal Methods with Kathleen Fisher of RAND & Byron Cook of AWS

Episode Summary

Executive Summary: Kathleen Fisher and Byron Cook explain how formal methods can materially improve software and AI security by turning desired properties into machine-checkable proofs. They argue AI worsens both attack and defense, but also enables faster proof generation, auto-formalization, and large-scale code rewrites toward memory-safe, policy-compliant systems. AWS’s automated reasoning tools show how natural-language policies can be translated into formal checks for agents and software.

Main Topics: AI’s impact on the cyber threat landscape: Both guests argue AI amplifies every stage of cyber offense—from novices to nation-states—by scaling attack speed, expertise, and parallelism, while also boosting defenders. Formal methods fundamentals: Formal methods are presented as algorithmic proof search for software properties, ranging from type checking and memory safety to full functional correctness. Proofs, assumptions, and assurance levels: The discussion emphasizes that proofs are always conditional on assumptions (hardware, ISAs, OS APIs, specs), so formal methods increase assurance rather than create absolute certainty. System-level verification case studies: Examples include CompCert, seL4, Hackams helicopter and quadcopter demonstrations, and AWS’s verified policy interpreter, showing how local proofs compose into system-wide guarantees. GenAI as an accelerator for formal methods: Language models can help translate specs, find invariants, ranking functions, and proofs, lowering the barrier to formal verification and generating training data from verified artifacts. AWS automated reasoning checks and policy compliance: AWS is applying formal reasoning to natural-language policies and AI-agent outputs, using multiple translations and theorem provers to verify or disambiguate policy compliance. Software rewrites, sandboxing, and future security: The guests foresee a large-scale move from insecure legacy code to memory-safe, formally checked code, especially for cloud, agentic AI, and sandboxing superintelligent systems.

Key Arguments: AI helps attackers at all expertise levels and across the full cyber kill chain, but the same AI also strengthens defenders by automating reasoning and proof discovery. Formal methods are not all-or-nothing; they span a spectrum from type checking to full functional correctness, and different guarantees are appropriate for different systems. There is no such thing as 100% assurance; proofs depend on assumptions about hardware, instruction sets, operating systems, and specifications. The hardest part of formal verification is usually specifying the system correctly, not proving the spec once written. Formal methods can deliver system-wide security guarantees when combined across layers, as shown in helicopter and hypervisor examples. Generative AI can dramatically improve formal methods by drafting specs, generating proofs, and creating correct training data from verified outputs. AWS has already used formal methods to verify policy interpretation, network reachability, and customer-facing analyzers, and now extends this to AI-agent guardrails. A future software stack rewritten with AI-assisted formal methods could substantially reduce vulnerabilities, especially by moving from C to memory-safe languages like Rust. Even if code is formally verified, software security still competes with usability, availability, and flexibility, so organizations must choose appropriate security levels rather than absolute perfection. Natural-language policies can be formalized into logic, allowing AI systems to answer questions accurately and flag ambiguity instead of hallucinating policy interpretations.

Data Points: MATS alumni working in AI safety/security: 80% - Promotional note at the beginning of the episode MATS fellows co-authored publications: 120+ - Promotional note about the MATS program MATS publications citations: 7,000+ - Promotional note about the MATS program MATS stipend: $15,000 - Program funding described in the sponsor segment MATS compute budget: $12,000 - Program funding described in the sponsor segment AWS policy interpreter rate: over a billion times per second - Byron Cook describes how often AWS’s policy interpreter is invoked Verification accuracy: up to 99% - Claim about AWS automated reasoning checks for translating and validating natural-language policies Hackams program duration: 2011–2016 - DARPA program cited as a major formal-methods case study SEL4 proof artifact size: ~10,000 lines of C and ~100,000 lines of Isabelle - Referenced in the separation-kernel example Red team exposure: 6 weeks of knowledge - Initial Boeing helicopter red-team hacking baseline Amazon adoption timeline: since 2014 - Kathleen Fisher notes she joined Amazon in 2014 and began building customer-facing reasoning tools AICC cyber competition: AI plus cyber could find and fix bugs at speed and scale - Used as evidence that AI-assisted remediation is becoming practical

Pivotal Quotes: "AI helps everyone do better at cyber attacks or attacks, or whatever the part of the cyber kill chain you're functioning, AI helps you do better." — Kathleen Fisher: Summarizing how AI changes the offense-defense balance across skill levels "It’s the algorithmic search for proofs." — Byron Cook: A concise definition of formal methods for software verification "The hardest part is figuring out what you want to prove." — Byron Cook: Explaining why specification work dominates verification projects

Implications: Formal methods plus AI could become a practical path to safer software, policy-compliant agents, and large-scale code modernization. The near-term bottleneck is better specs and adoption, not theory.