RESEARCH

< view all research areas

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

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