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.
翻译:互动的线性验证软件通常围绕一个可信赖的校验内核设计,这是唯一能够验证理论的系统组成部分。 不信任的自动化程序位于内核之外, 并驱动它通过一个 API 来推导新的理论。 内核和不信任的自动化通常是用同一个编程语言执行的 -- " 元语言" -- 通常是MLL家族中一些功能性编程语言。 由 Milner 在其 LCF 校验助理 中引入的这一战略是一个可靠性机制, 目的是确保系统产生的任何所谓的词性能确实由逻辑中的理论产生。 改变托盘, 操作系统也通常围绕一个值得信任的内核, 一个负责( 除其他外) 校验的特权和不信任的自动化程序。 不信任程序与系统互动, 发出内核系统呼叫硬件特权界限。 以这种方式, 操作的内核内核系统监督用户- 进程。 尽管表面上非常不同, 直观, 我们发现, 解内核的两类的内核系统是用来解释, 解内部的代码, 和内部的系统是用来解释。