Dominic Mulligan

I am a Principal Applied Scientist within the Automated Reasoning Group at Amazon Web Services, Cambridge, UK. I work on the verification of correctness and security properties of ultra low-level code. For details of my employment history and education see my about page. My publications page also contains details of my academic publications, position papers, and patents. I also occassionally write blog posts about technical and non-technical topics, which can be found here.

Site changelog

Site announcement 2025-01-05

I have reconfigured my website, moving away from the Hugo static site generator in favour of hand-written HTML. As part of this process I have added some missing publications to my publications page and details of my accepted patents.

Journal paper announcement 2024-05-23

I am delighted to announce that the paper Private delegated computations using strong isolation has been accepted into a special issue on advances in emerging privacy-preserving computation at IEEE transactions on emerging topics in Computer Science (TETCSI).

The paper was co-authored with Mathias Brossard, Guilhem Bryant, Basma El Gaabouri, Xinxin Fan, Alexandre Ferreira, Edmund Grimley-Evans, Christopher Haster, Evan Johnson, Derek Miller, Fan Mo, Nick Spinale, Eric van Hensbergen, Hugo J. M. Vincent, and Shale Xiong.

Journal paper announcement 2024-05-23

I am delighted to announce that the paper All watched over by machines of loving grace — describing the Supervisionary proof-checking system for HOL — has been accepted in the post-proceedings of TYPES 2022.

Conference paper announcement 2024-02-27

I am delighted to announce that the paper A verification methodology for the Arm Confidential Computing Architecture co-written with Anthony Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Nathan Chong, and Gustavo Petri has now been accepted for publication at OOPSLA/SPLASH 2023.

New job announcement 2022-07-01

I have now left Arm Research and have taken up a position as a Principal Applied Scientist within the Automated Reasoning Group at Amazon Web Services in Cambridge..

Position paper announcement 2022-06-27

I am delighted to announce the recent publication of the Arm Trustworthy AI position paper, a documented which I contributed to.

Technical report announcement 2022-05-25

I am delighted to announce the recent release of an Arm Research technical report on the IceCap and Veracruz confidential-computing projects.

The report, Private delegated computations using strong isolation, is co-authored by Mathias Brossard, Guilhem Bryant, Basma El Gaabouri, Xinxin Fan, Alexandre Ferreira, Edmund Grimley-Evans, Christopher Haster, Evan Johnson, Derek Miller, Fan Mo, Nick Spinale, Eric van Hensbergen, Hugo J. M. Vincent, Shale Xiong, and me.

Workshop abstract announcement 2022-05-25

I am delighted to announce that the abstract, Scalable assurance via verifiable hardware-software contracts , has been accepted for presentation at the Workshop on Open-source Computer Architecture Research (OSCAR 2022), co-located with ISCA.

This paper was co-written with Yao Hsiao, Gustavo Petri, Nikos Nikoleris, and Caroline Trippel, with Yao presenting this work at the workshop.

Site announcement 2021-12-12

I am pleased to announce that electronic copies of all of my papers have now been moved over from my old website and can be found on my publications page.

Workshop paper announcement 2021-11-26

I am delighted to announce that The Supervisionary proof-checking kernel, or: a work-in-progress towards proof-generating code — which I co-authored with Nick Spinale — has been accepted for presentation at the workshop on Principles of Secure Compilation (PriSC 2022), co-located with POPL.

Programme committee announcement 2021-11-26

I am honoured to have been invited to serve on the Open Confidential Computing Conference (OC3 2021) programme committee.

Please, consider submitting a talk proposal! Derek Miller, from the Veracruz project, presented a talk at last year’s OC3 event which had a great mix of interesting talks and was very well attended.

Journal paper announcement 2021-10-04

I am pleased to announce that the paper A highly-available move operation for replicated trees has now been accepted for publication in IEEE Transactions on Parallel and Distributed Systems (TPDS). This is joint work with Martin Kleppmann, Victor Gomes, and Alastair Beresford.

Invited talk announcement 2021-09-15

I would like to thank Prof. Kevin Butler for inviting me to give a keynote talk at the Technical Demo Conference within the Florida Institute for Cybersecurity Research (FICS) at the University of Florida.

Conference paper announcement 2021-09-07

I am delighted to announce that the paper Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations has been accepted for publication at the IEEE/ACM International Symposium on Microarchitecture (MICRO) 2021.

This is a paper co-written with Yao Hsiao (Stanford), Gustavo Petri (Arm Research), Nikos Nikoleris (Arm Research), and Caroline Trippel (Stanford).

Invited conference paper announcement 2021-09-07

I am delighted to announce the invited paper Confidential Computing—a brave new world has been accepted by the IEEE International Symposium on Secure and Private Execution Environment Design (SEED 2021).

This was written with some of my colleagues at Arm: Gustavo Petri, Nick Spinale, Gareth Stockwell, and Hugo Vincent.

Post announcement 2021-04-27

I have written a technical post explaining the motivation, and some of the design choices, behind the Vercruz confidential computing project.

Site announcement 2020-08-05

I have now moved my bibliography over from my old website. The list can be found here.

Site announcement 2020-07-02

Due to increasing unreliability of my website host, and regular security issues with WordPress, I have moved to a static site hosted on Github pages.