可证明可信的系统。
Provably trustworthy systems.
作者信息
Klein Gerwin, Andronick June, Keller Gabriele, Matichuk Daniel, Murray Toby, O'Connor Liam
机构信息
Data61, CSIRO, Sydney, Australia
School of Computer Science and Engineering, UNSW, Sydney, Australia.
出版信息
Philos Trans A Math Phys Eng Sci. 2017 Oct 13;375(2104). doi: 10.1098/rsta.2015.0404.
We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We then show two complementary techniques for scaling these methods to larger systems: proof engineering, to estimate verification effort; and code/proof co-generation, for scalable development of provably trustworthy applications.This article is part of the themed issue 'Verified trustworthy software systems'.
我们展示了近期在从头开始构建和扩展具有形式化、机器可检查证明的可信系统方面的工作，包括在二进制机器代码层面的操作系统内核。我们首先简要概述seL4微内核验证以及如何使用它来构建经过验证的系统。然后，我们展示了两种将这些方法扩展到更大系统的互补技术：证明工程，用于估计验证工作量；以及代码/证明协同生成，用于可扩展地开发可证明可信的应用程序。本文是主题为“经过验证的可信软件系统”的特刊的一部分。
Zotero 插件