Researcher profile

Dominic P. Mulligan

Dominic P. Mulligan contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 13 - UnverifiedVerification L1Unclaimed author
2works
0followers
3topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

2 published item(s)

preprint2022arXiv

Private delegated computations using strong isolation

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.

preprint2022arXiv

The Supervisionary proof-checking kernel (or: a work-in-progress towards proof generating code)

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.