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 announcement2025-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 announcement2024-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 announcement2024-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 announcement2024-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 announcement2022-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 announcement2022-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 announcement2022-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 announcement2022-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 announcement2021-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 announcement2021-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 announcement2021-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 announcement2021-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.
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 announcement2021-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 announcement2021-04-27
I have written a technical post explaining the motivation, and some of the design choices, behind the Vercruz
confidential computing project.
Site announcement2020-08-05
I have now moved my bibliography over from my old website. The list can be found here.
Site announcement2020-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.