RESEARCH
HACMS
HACMS was a DARPA program that ran roughly from 2012 to 2018. Kathleen served as the initial program manager for HACMS.
For decades, formal methods offered the promise of software that does not have exploitable bugs. Until recently, however, it has not been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. It has been proven to be fully functionally correct, ensuring the absence of a variety of implementation errors often exploited by hackers, and to enforce integrity and confidentiality properties. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution, including increased processor speed, better infrastructure like the Isabelle/HOL and Coq theorem provers, specialized logics for reasoning about low-level code, increasing levels of automation afforded by tactic languages and SAT/SMT solvers, and the decision to move away from trying to verify existing artifacts and instead focus on co-developing the code and the correctness proof. The HACMS program explored the promise and limitations of current formal methods techniques in the context of creating high-assurance software for vehicles, including quadcopters, helicopters, and automobiles.
People
- John Launchbury
- Ray Richards
- More than a hundred more people from DARPA, AFRL, and various performer organizations
Papers
- The HACMS Program: Using formal methods to eliminate exploitable bugs. Philosophical Transactions A, 375(2104), 2017.
Talks
- Using Formal Methods to Eliminate Exploitable Bugs
- Keynote, Formal Methods for the Informal Engineer
- Invited Talk, Chalmers Online Functional Programming Seminar Series
- Department Colloquium, Rice University, Houston, Texas
- Invited Talk, Formal Methods@Scale
- Department Colloquium, Pomona College, Claremont, California
- Invited Talk, Summer BOB, Berlin
- Plenary Keynote, ETAPS
- Keynote, Code Mesh LDN
- Invited Talk, SPLASH-I
- Keynote, IEEE Cybersecurity Development Conference
- Keynote, Tufts President’s Council
- Invited Talk, Workshop on Safety and Control for Artificial Intelligence
- Keynote, The 8th NASA Formal Methods Symposium
- Invited Talk, Royal Society
- Department Colloquium, University of Texas A&M
- Invited Talk, PEPM
- Invited Talk, YOW! Sydney
- Invited Talk, YOW! Brisbane
- Invited Talk, YOW! Melbourne
- Department Colloquium, Brown University
- Department Colloquium, Cornell University
- Invited Talk, USENIX Security
- AI Safety and Cybersecurity Panelist, CNAS AI and Global Security Summit
- Tufts Talks: Towards Less Hackable Cars
- Invited Talk, Tufts Alumni Event, New York
- Invited Talk, Tufts Alumni Event, San Francisco
- Invited Talk, Tufts Alumni Event, Los Angeles
- Invited Talk, Tufts Alumni Event, Boston
- HACMS: Provably Correct Software for Embedded Systems
- Invited Talk, Stanford Center for Automotive Research
- Keynote, UK Cyber Security Research Conference
- Keynote, International Conference on Functional Programming (ICFP)
- Invited Talk, Google I/O
- Keynote, ESCAR USA
- Kick-off Meeting: Airworthiness of Complex Systems Study Group
- National Security Agency
- New England Advanced Cyber Security Center Annual Conference
- Keynote, Second Annual Symposium, Maryland Cybersecurity Center
- Layered Assurance Workshop
- Keynote, ACM High Integrity Language Technology Conference
- Keynote, High Confidence Software Systems Symposium
Media Appearances
- Episode #15: Dr. Kathleen Fisher-Sparking the New Age of Formal Verification at DARPA. Building Better Systems Podcast. Jan 10, 2022.
- Thoughts on Secure Development. September 29, 2018.
- Is there anything hackers can’t hack? Now there is, thanks to a new way of coding, bigthink.com. Mar 22, 2018.
- Faces of the Foundation: Kathleen Fisher, The Hertz Foundation blog. Mar 5, 2018.
- Hands off the Wheel, BBC Radio 4 and BBC World Service. Jan 1, 2018.
- Hackable software in the driver’s seat, The Paralax.com, Dec 8, 2017.
- So You Want Digital Voting? Hackers Want It Even More, bigthink.com. Sep 17, 2017.
- How Hackers Can Control Your Car’s Brakes, Doors, and Steering—and Why Car Makers Can’t Stop Them, bigthink.com. Sep 9, 2017.
- How hacked computer code allegedly helped a biker gang steal 150 Jeeps, The Washington Post. June 1, 2017.
- Computer security is broken from top to bottom, The Economist. Apr 8, 2017.
- Computer Hacks of the Future, and How to Prevent Them, Science Friday. Feb 25, 2017. Panelist.
- DARPA: Nobody’s Safe on the Internet, Sixty Minutes. Feb 8, 2015.