What Happened to Formal Methods for Security?

Abstract

We asked 7 experts 7 questions to find out what has occurred recently in terms of applying formal methods (FM) to security-centric, cyber problems. We are continually reminded of the 1996 paper by Tony Hoare "How did Software Get So Reliable Without Proof?" [1] In that vein, how did we get so insecure with proof? Given daily press announcements concerning new malware, data breaches, and privacy loss, is FM still relevant or was it ever? Our experts answered with unique personal insights. We were curious as to whether this successful methodology in "safety-critical" has succeeded as well for today's "build it, hack it, patch it" mindset. Our experts were John McLean (Naval Research Labs), Paul Black (National Institute of Standards and Technology), Karl Levitt (University of California at Davis), Joseph Williams (CloudEconomist.Com), Connie Heitmeyer (Naval Research Labs), Eugene Spafford (Purdue University), and Joseph Kiniry (Galois, Inc.). The questions and responses follow.