Fisher Kathleen, Launchbury John, Richards Raymond
Department of Computer Science, Tufts University, Medford, MA, USA
DARPA, Arlington, VA, USA.
Philos Trans A Math Phys Eng Sci. 2017 Oct 13;375(2104). doi: 10.1098/rsta.2015.0401.
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'.
几十年来，形式化方法一直承诺能提供没有可利用漏洞的经过验证的软件。然而，直到最近，还无法验证具有足够复杂性以实用的软件。最近，这种情况发生了变化。SeL4是一个开源操作系统微内核，其效率足以用于广泛的实际应用。其设计者证明它在功能上完全正确，确保不存在缓冲区溢出、空指针异常、使用后释放错误等，并保证完整性和保密性。CompCert验证C编译器将源C程序映射到可证明等效的汇编语言，确保编译器中不存在可利用的漏洞。有几个因素促成了这场革命，包括更快的处理器、更高的自动化程度、更广泛的基础设施、专门的逻辑以及共同开发代码和正确性证明而非验证现有工件的决定。在本文中，我们探讨了当前形式化方法技术的前景和局限性。我们在国防高级研究计划局（DARPA）的HACMS项目背景下讨论这些问题，该项目的目标是创建用于车辆（包括四轴飞行器、直升机和汽车）的高可信度软件。本文是主题为“经过验证的可信软件系统”的特刊的一部分。
