-
A modest proposal: explicit support for foundational pluralism
Authors:
Martin Berger,
Dominic P. Mulligan
Abstract:
Whilst mathematicians assume classical reasoning principles by default they often context switch when working, restricting themselves to various forms of subclassical reasoning. This pattern is especially common amongst logicians and set theorists, but workaday mathematicians also commonly do this too, witnessed by narrative notes accompanying a proof -- "the following proof is constructive", or "…
▽ More
Whilst mathematicians assume classical reasoning principles by default they often context switch when working, restricting themselves to various forms of subclassical reasoning. This pattern is especially common amongst logicians and set theorists, but workaday mathematicians also commonly do this too, witnessed by narrative notes accompanying a proof -- "the following proof is constructive", or "the following proof does not use choice", for example. Yet, current proof assistants provide poor support for capturing these narrative notes formally, an observation that is especially true of systems based on Gordon's HOL, a classical higher-order logic. Consequently, HOL and its many implementations seem ironically more committed to classical reasoning than mainstream mathematicians are themselves, limiting the mathematical content that one may easily formalise. To facilitate these context switches, we propose that mathematicians mentally employ a simple tainting system when temporarily working subclassically -- an idea not currently explored in proof assistants. We introduce a series of modest but far-reaching changes to HOL, extending the standard two-place Natural Deduction relation to incorporate a taint-label, taken from a particular lattice, and which describes or limits the "amount" of classical reasoning used within a proof. Taint can be seen either as a simple ty** system on HOL proofs, or as a form of static analysis on proof trees, and partitions our logic into various fragments of differing expressivity, sitting side-by-side. Results may pass from a "less classical" fragment into a "more classical" fragment of the logic without modification, but not vice versa, with the flow of results between worlds controlled by an inference rule akin to a subty** or subsumption rule.
△ Less
Submitted 20 February, 2023;
originally announced February 2023.
-
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.
-
OpSets: Sequential Specifications for Replicated Datatypes (Extended Version)
Authors:
Martin Kleppmann,
Victor B. F. Gomes,
Dominic P. Mulligan,
Alastair R. Beresford
Abstract:
We introduce OpSets, an executable framework for specifying and reasoning about the semantics of replicated datatypes that provide eventual consistency in a distributed system, and for mechanically verifying algorithms that implement these datatypes. Our approach is simple but expressive, allowing us to succinctly specify a variety of abstract datatypes, including maps, sets, lists, text, graphs,…
▽ More
We introduce OpSets, an executable framework for specifying and reasoning about the semantics of replicated datatypes that provide eventual consistency in a distributed system, and for mechanically verifying algorithms that implement these datatypes. Our approach is simple but expressive, allowing us to succinctly specify a variety of abstract datatypes, including maps, sets, lists, text, graphs, trees, and registers. Our datatypes are also composable, enabling the construction of complex data structures. To demonstrate the utility of OpSets for analysing replication algorithms, we highlight an important correctness property for collaborative text editing that has traditionally been overlooked; algorithms that do not satisfy this property can exhibit awkward interleaving of text. We use OpSets to specify this correctness property and prove that although one existing replication algorithm satisfies this property, several other published algorithms do not. We also show how OpSets can be used to develop new replicated datatypes: we provide a simple specification of an atomic move operation for trees, an operation that had previously been thought to be impossible to implement without locking. We use the Isabelle/HOL proof assistant to formalise the OpSets approach and produce mechanised proofs of correctness of the main claims in this paper, thereby eliminating the ambiguity of previous informal approaches, and ruling out reasoning errors that could occur in handwritten proofs.
△ Less
Submitted 14 May, 2018; v1 submitted 11 May, 2018;
originally announced May 2018.
-
Verifying Strong Eventual Consistency in Distributed Systems
Authors:
Victor B. F. Gomes,
Martin Kleppmann,
Dominic P. Mulligan,
Alastair R. Beresford
Abstract:
Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of cor…
▽ More
Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, develo** proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.
△ Less
Submitted 29 August, 2017; v1 submitted 6 July, 2017;
originally announced July 2017.
-
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
Authors:
Murdoch J. Gabbay,
Dominic P. Mulligan
Abstract:
We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The resulting denotations are smaller and better-behaved, in ways we make precise, than functional valuation-based models.
Using these new models, we then develop a g…
▽ More
We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The resulting denotations are smaller and better-behaved, in ways we make precise, than functional valuation-based models.
Using these new models, we then develop a generalisation of λ-term syntax enriching them with existential meta-variables, thus yielding a theory of incomplete functions. This incompleteness is orthogonal to the usual notion of incompleteness given by function abstraction and application, and corresponds to holes and incomplete objects.
△ Less
Submitted 31 October, 2011;
originally announced November 2011.
