论文标题
监督检查检查内核（OR：朝着证明生成代码的工作中的工作）
The Supervisionary proof-checking kernel (or: a work-in-progress towards proof generating code)
论文作者
论文摘要
交互式定理证明软件通常围绕可信赖的验证检查内核设计，即能够对定理进行认证的唯一系统组件。不受信任的自动化过程位于内核之外，并将其驱动以通过API推导新定理。内核和不信任的自动化通常以同一编程语言（“元语言”）实现，通常是ML家族中某些功能性编程语言。米尔纳（Milner）在他的LCF证明助手中引入的这种策略是一种可靠性机制，旨在确保该系统所产生的任何所产生的定理的任何逻辑中的理论确实都需要。 不断变化的粘贴，操作系统通常也围绕受信任的内核进行设计，这是一个特权组件，除其他外，还可以在用户空间软件和硬件中调节交互。不受信任的过程通过在硬件特权边界上发出内核系统来与系统交互。这样，操作系统内核监督用户空间流程。 尽管表面上是非常不同的，但我们看到两种内核的任务是求解相同的任务：面对与未经信任的代码的无限互动，强制执行系统不变性。然而，解决该问题的两个解决方案（由各种内核采用）截然不同。 在此摘要中，我们探讨了设计验证检查内核作为监督软件，其中内核和不信任代码之间的分离是通过特权执行的，而不是编程语言模块边界和类型的抽象。我们描述了有关监督检查检查内核的工作，并简要绘制其独特的系统接口。然后，我们描述了监督内核的一些潜在用途。
Interactive theorem proving software is typically designed around a trusted proof-checking kernel, the sole system component capable of authenticating theorems. Untrusted automation procedures reside outside of the kernel, and drive it to deduce new theorems via an API. Kernel and untrusted automation are typically implemented in the same programming language -- the "meta-language" -- usually some functional programming language in the ML family. This strategy -- introduced by Milner in his LCF proof assistant -- is a reliability mechanism, aiming to ensure that any purported theorem produced by the system is indeed entailed by the theory within the logic. Changing tack, operating systems are also typically designed around a trusted kernel, a privileged component responsible for -- amongst other things -- mediating interaction betwixt user-space software and hardware. Untrusted processes interact with the system by issuing kernel system calls across a hardware privilege boundary. In this way, the operating system kernel supervises user-space processes. Though ostensibly very different, squinting, we see that the two kinds of kernel are tasked with solving the same task: enforcing system invariants in the face of unbounded interaction with untrusted code. Yet, the two solutions to solving this problem, employed by the respective kinds of kernel, are very different. In this abstract, we explore designing proof-checking kernels as supervisory software, where separation between kernel and untrusted code is enforced by privilege, not programming language module boundaries and type abstraction. We describe work on the Supervisionary proof-checking kernel, and briefly sketch its unique system interface. We then describe some potential uses of the Supervisionary kernel.
