Reference. The HACMS program: using formal methods to eliminate exploitable bugs

Kathleen Fisher, John Launchbury, Raymond Richards · Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences · 2017 · DOI
For decades, formal methods have offered the promise of verified 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. Its designers proved it to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and guaranteeing integrity and confidentiality. 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 faster processors, increased automation, more extensive infrastructure, specialized logics and the decision to co-develop code and correctness proofs rather than verify existing artefacts. In this paper, we explore the promise and limitations of current formal-methods techniques. We discuss these issues in the context of DARPA’s HACMS program, which had as its goal the creation of high-assurance software for vehicles, including quadcopters, helicopters and automobiles. This article is part of the themed issue ‘Verified trustworthy software systems’.

Cite
Cite as @fisher-2017-the (helia, typst) · \cite{fisher-2017-the} (LaTeX)
BibTeX
bibtex · 1 line
@article{fisher-2017-the, title={The HACMS program: using formal methods to eliminate exploitable bugs}, volume={375}, ISSN={1471-2962}, url={http://dx.doi.org/10.1098/rsta.2015.0401}, DOI={10.1098/rsta.2015.0401}, number={2104}, journal={Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences}, publisher={The Royal Society}, author={Fisher, Kathleen and Launchbury, John and Richards, Raymond}, year={2017}, month=Sept, pages={20150401} }
hayagriva YAML (typst)
yaml · 17 lines
fisher-2017-the:
  type: article
  title: 'The HACMS program: using formal methods to eliminate exploitable bugs'
  author:
  - Fisher, Kathleen
  - Launchbury, John
  - Richards, Raymond
  date: 2017-09
  page-range: '20150401'
  serial-number:
    doi: 10.1098/rsta.2015.0401
  parent:
    type: periodical
    title: 'Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences'
    publisher: The Royal Society
    issue: 2104
    volume: 375
Download: fisher-2017-the.bib · fisher-2017-the.yml
Cited by (1)

Formal Methods for the Informal Engineer: Workshop Recommendations sarma-2021-formalarXiv · 2021
Formal Methods for the Informal Engineer (FMIE) was a workshop held at the Broad Institute of MIT and Harvard in 2021 to explore the potential role of verified software in the biomedical software ecosystem. The motivation for organizing FMIE was the recognition that the life sciences and medicine are undergoing a transition from being passive consumers of software and AI/ML technologies to fundamental drivers of new platforms, including those which will need to be mission and safety-critical. Drawing on conversations leading up to and during the workshop, we make five concrete recommendations to help software leaders organically incorporate tools, techniques, and perspectives from formal methods into their project planning and development trajectories.
DOI · arXiv
Cites 48 works (1 here)
With notes (1)

Finding and Understanding Bugs in C Compilers yangFindingUnderstandingBugsPLDI · 2011
Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers.
PDF · DOI · pldb
External (47)
fisher-2017-the reference entries/refs/fisher-2017-the/fisher-2017-the.hel