The Supervisionary proof-checking kernel (or: a work-in-progress towards proof generating code)
Authors:
Dominic P. Mulligan,
Nick Spinale
Abstract:
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…
▽ More
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.
△ Less
Submitted 6 May, 2022;
originally announced May 2022.
Private delegated computations using strong isolation
Authors:
Mathias Brossard,
Guilhem Bryant,
Basma El Gaabouri,
Xinxin Fan,
Alexandre Ferreira,
Edmund Grimley-Evans,
Christopher Haster,
Evan Johnson,
Derek Miller,
Fan Mo,
Dominic P. Mulligan,
Nick Spinale,
Eric van Hensbergen,
Hugo J. M. Vincent,
Shale Xiong
Abstract:
Sensitive computations are now routinely delegated to third-parties. In response, Confidential Computing technologies are being introduced to microprocessors, offering a protected processing environment, which we generically call an isolate, providing confidentiality and integrity guarantees to code and data hosted within -- even in the face of a privileged attacker. Isolates, with an attestation…
▽ More
Sensitive computations are now routinely delegated to third-parties. In response, Confidential Computing technologies are being introduced to microprocessors, offering a protected processing environment, which we generically call an isolate, providing confidentiality and integrity guarantees to code and data hosted within -- even in the face of a privileged attacker. Isolates, with an attestation protocol, permit remote third-parties to establish a trusted "beachhead" containing known code and data on an otherwise untrusted machine. Yet, the rise of these technologies introduces many new problems, including: how to ease provisioning of computations safely into isolates; how to develop distributed systems spanning multiple classes of isolate; and what to do about the billions of "legacy" devices without support for Confidential Computing?
Tackling the problems above, we introduce Veracruz, a framework that eases the design and implementation of complex privacy-preserving, collaborative, delegated computations among a group of mutually mistrusting principals. Veracruz supports multiple isolation technologies and provides a common programming model and attestation protocol across all of them, smoothing deployment of delegated computations over supported technologies. We demonstrate Veracruz in operation, on private in-cloud object detection on encrypted video streaming from a video camera. In addition to supporting hardware-backed isolates -- like AWS Nitro Enclaves and Arm Confidential Computing Architecture Realms -- Veracruz also provides pragmatic "software isolates" on Armv8-A devices without hardware Confidential Computing capability, using the high-assurance seL4 microkernel and our IceCap framework.
△ Less
Submitted 6 May, 2022;
originally announced May 2022.
