-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html
More file actions
217 lines (183 loc) · 9.92 KB
/
index.html
File metadata and controls
217 lines (183 loc) · 9.92 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
<!DOCTYPE html>
<html>
<head>
<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-003LVMP0GC"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag() { dataLayer.push(arguments); }
gtag('js', new Date());
gtag('config', 'G-003LVMP0GC');
</script>
<title>Dominic Mulligan's homepage</title>
<link rel="stylesheet" href="main.css">
<meta name="author" content="Dominic Mulligan">
<meta charset="utf-8">
<meta name="keywords" content="formal methods, confidential computing, Rust, Isabelle/HOL">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="preconnect" href="https://fonts.googleapis.com">
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
<link
href="https://fonts.googleapis.com/css2?family=Cormorant+Garamond:ital,wght@0,300;0,400;0,500;0,600;0,700;1,300;1,400;1,500;1,600;1,700&family=Montserrat:ital,wght@0,100..900;1,100..900&family=Source+Code+Pro:ital,wght@0,200..900;1,200..900&display=swap"
rel="stylesheet">
</head>
<body>
<h1>Dominic Mulligan</h1>
</body>
<p>I am a <emph>Principal Applied Scientist</emph> within the <emph>Automated Reasoning Group</emph> at <emph>Amazon Web
Services</emph>, 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 <a href="./about.html">about</a> page.
My <a href="./publications.html">publications</a> 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 <a href="./blog-posts/posts.html">here</a>.
</p>
<h2>Site changelog</h2>
<div class="news-item">
<span class="news-title">Site announcement</span>
<span class="news-date">2025-01-05</span>
<p>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 <a href="./publications.html">publications</a>
page and details of my accepted patents.</p>
</div>
<div class="news-item">
<span class="news-title">Journal paper announcement</span>
<span class="news-date">2024-05-23</span>
<p>I am delighted to announce that the paper <emph>Private delegated computations using strong isolation</emph> has
been accepted into a special issue on advances in emerging privacy-preserving computation at <emph>IEEE transactions
on emerging topics in Computer Science (TETCSI)</emph>.</p>
<p>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.</p>
</div>
<div class="news-item">
<span class="news-title">Journal paper announcement</span>
<span class="news-date">2024-05-23</span>
<p>I am delighted to announce that the paper <emph>All watched over by machines of loving grace</emph>
— describing the <a href="https://github.com/DominicPM/supervisionary">Supervisionary</a> proof-checking
system for HOL — has been accepted in the post-proceedings of <emph>TYPES 2022</emph>.
</p>
</div>
<div class="news-item">
<span class="news-title">Conference paper announcement</span>
<span class="news-date">2024-02-27</span>
<p>I am delighted to announce that the paper <emph>A verification methodology for the Arm Confidential Computing
Architecture</emph> co-written with Anthony Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Nathan Chong, and
Gustavo Petri has now been accepted for publication at <emph>OOPSLA/SPLASH 2023</emph>.
</p>
</div>
<div class="news-item">
<span class="news-title">New job announcement</span>
<span class="news-date">2022-07-01</span>
<p>I have now left Arm Research and have taken up a position as a <emph>Principal Applied Scientist</emph> within the
<emph>Automated Reasoning Group</emph> at Amazon Web Services in Cambridge.</emph>.
</p>
</div>
<div class="news-item">
<span class="news-title">Position paper announcement</span>
<span class="news-date">2022-06-27</span>
<p>I am delighted to announce the recent publication of the <emph>Arm Trustworthy AI position paper</emph>, a
documented which I contributed to.
</p>
</div>
<div class="news-item">
<span class="news-title">Technical report announcement</span>
<span class="news-date">2022-05-25</span>
<p>I am delighted to announce the recent release of an Arm Research technical report on the <emph>IceCap</emph> and
<emph>Veracruz</emph> confidential-computing projects.
</p>
<p>The report, <emph>Private delegated computations using strong isolation</emph>, 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.
</p>
</div>
<div class="news-item">
<span class="news-title">Workshop abstract announcement</span>
<span class="news-date">2022-05-25</span>
<p>I am delighted to announce that the abstract, <emph>Scalable assurance via verifiable hardware-software contracts
</emph>, has been accepted for presentation at the <emph>Workshop on Open-source Computer Architecture Research
(OSCAR 2022)</emph>, co-located with <emph>ISCA</emph>.
<p>This paper was co-written with Yao Hsiao, Gustavo Petri, Nikos Nikoleris, and Caroline Trippel, with Yao presenting
this work at the workshop.
</p>
</div>
<div class="news-item">
<span class="news-title">Site announcement</span>
<span class="news-date">2021-12-12</span>
<p>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 <a href="./publications.html">publications</a> page.
</p>
</div>
<div class="news-item">
<span class="news-title">Workshop paper announcement</span>
<span class="news-date">2021-11-26</span>
<p>I am delighted to announce that <emph>The Supervisionary proof-checking kernel, or: a work-in-progress towards
proof-generating code</emph> — which I co-authored with Nick Spinale — has been accepted for
presentation at the workshop on <emph>Principles of Secure Compilation (PriSC 2022)</emph>, co-located with <emph>
POPL</emph>.
</p>
</div>
<div class="news-item">
<span class="news-title">Programme committee announcement</span>
<span class="news-date">2021-11-26</span>
<p>I am honoured to have been invited to serve on the <emph>Open Confidential Computing Conference (OC3 2021)</emph>
programme committee.</p>
<p>Please, consider submitting a talk proposal! Derek Miller, from the Veracruz project, presented
a talk at <a href="https://www.youtube.com/playlist?list=PLEhAl3D5WVvSKTp9jD6lV67zuFR8lUZVa">last year’s OC3</a>
event which had a great mix of interesting talks and was very well attended.
</p>
</div>
<div class="news-item">
<span class="news-title">Journal paper announcement</span>
<span class="news-date">2021-10-04</span>
<p>I am pleased to announce that the paper <emph>A highly-available move operation for replicated trees</emph> has now
been accepted for publication in <emph>IEEE Transactions on Parallel and Distributed Systems (TPDS)</emph>. This is
joint work with Martin Kleppmann, Victor Gomes, and Alastair Beresford.
</p>
</div>
<div class="news-item">
<span class="news-title">Invited talk announcement</span>
<span class="news-date">2021-09-15</span>
<p>I would like to thank <a href="https://cise.ufl.edu/~butler">Prof. Kevin Butler</a> for inviting me to give a
keynote talk at the Technical Demo Conference
within the <a href="https://fics.institute.ufl.edu/">Florida Institute for Cybersecurity Research (FICS)</a> at the
University of Florida.
</p>
</div>
<div class="news-item">
<span class="news-title">Conference paper announcement</span>
<span class="news-date">2021-09-07</span>
<p>I am delighted to announce that the paper <emph>Synthesizing formal models of hardware from RTL for efficient
verification of memory model implementations</emph> has been accepted for publication at the <emph>IEEE/ACM
International Symposium on Microarchitecture (MICRO) 2021</emph>.</p>
<p>This is a paper co-written with Yao Hsiao (Stanford), Gustavo Petri (Arm Research), Nikos Nikoleris (Arm Research),
and Caroline Trippel (Stanford).</p>
</div>
<div class="news-item">
<span class="news-title">Invited conference paper announcement</span>
<span class="news-date">2021-09-07</span>
<p>I am delighted to announce the invited paper <emph>Confidential Computing—a brave new
world</emph> has been accepted by the <emph> IEEE International Symposium on Secure and Private Execution
Environment Design (SEED 2021)</emph>.</p>
<p>This was written with some of my colleagues at Arm: Gustavo Petri, Nick Spinale, Gareth Stockwell, and Hugo
Vincent.</p>
</div>
<div class="news-item">
<span class="news-title">Post announcement</span>
<span class="news-date">2021-04-27</span>
<p>I have written a technical post explaining the motivation, and some of the design choices, behind the Vercruz
confidential computing project.</p>
</div>
<div class="news-item">
<span class="news-title">Site announcement</span>
<span class="news-date">2020-08-05</span>
<p>I have now moved my bibliography over from my old website. The list can be found <a
href="./publications.html">here</a>.</p>
</div>
<div class="news-item">
<span class="news-title">Site announcement</span>
<span class="news-date">2020-07-02</span>
<p>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.</p>
</div>
</html>