-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathabout.html
135 lines (110 loc) · 7.11 KB
/
about.html
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
<!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>About me</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>About me</h1>
<p>Click <a href="./index.html">here</a> to go back.</p>
<h2>Employment history</h2>
<div class="employment">
<span class="employer">Automated Reasoning Group, Amazon Web Services</span>
<span class="employment-period">2022–present</span>
<p>I am a <emph>Principal Applied Scientist</emph> within the <emph>Automated Reasoning Group</emph> at <emph>Amazon
Web Services</emph>, Cambridge. I work on the verification of correctness and security properties of ultra
low-level code.</p>
</div>
<div class="employment">
<span class="employer">Systems Research Group, Arm Research</span>
<span class="employment-period">2017–2022</span>
<p>I was (eventually promoted to become a) <emph>Principal Research Engineer</emph> within the <emph>Systems Group
</emph> at <emph>Arm Research</emph>, Cambridge.
My research at Arm focussed on privacy-preserving computation, as evidenced
by the <a href="https://confidentialcomputing.io">Confidential Computing Consortium</a>-adopted <a
href="https://github.com/veracruz-project/veracruz">Veracruz</a> project, a project which I initiated and
thereafter acted as technical lead on.
</p>
<p>I also helped develop software verification flows which provided strong evidence for the
correctness for low-level, security-critical firmware, central to the <a
href="https://www.arm.com/architecture/security-features/arm-confidential-compute-architecture">Arm
Confidential Computing Architecture</a>, or Arm CCA. This is a Confidential Computing technology that will be
deployed as a point-release for the Armv9-A architecture and will eventually be found in hundreds of millions
of devices worldwide.</p>
</div>
<div class="employment">
<span class="employer">Computer Laboratory, University of Cambridge</span>
<span class="employment-period">2012–2017</span>
<p>I was a <emph>Postdoctoral Research Scientist</emph> at the <a href="https://www.cst.cam.ac.uk">Computer
Laboratory</a> at the <a href="https://www.cam.ac.uk">University of
Cambridge</a>. Here, I worked on <a href="https://www.cl.cam.ac.uk/~pes20/">Prof. Peter Sewell’s</a> <a
href="https://www.cl.cam.ac.uk/~pes20/people-new/index.html">Rigorous Engineering for Mainstream Systems</a>
project, or <emph>REMS</emph>.
</p>
<p>At Cambridge I helped design and develop the <a href="https://github.com/rems-project/lem">Lem</a>
specification language, and thereafter used Lem to formally specify the semantics of ELF static linking. I also
developed a side interest in the correctness of a class of distributed datastructure, called <emph>Conflict-free
Replicated Datatypes</emph>, or CRDTs.</p>
</div>
<div class="employment">
<span class="employer">Dipartimento di Scienze dell'Informazione, University of Bologna, Italy</span>
<span class="employment-period">2010–2012</span>
<p>I was a <emph>Postdoctoral Research Scientist</emph> at the <a href="https://disi.unibo.it/it">Dipartimento di
Scienze dell’Informazione</a> at the <a href="https://www.unibo.it/it/">Alma Mater Studiorum, Università di
Bologna</a>. I worked with <a href="https://www.cs.unibo.it/~sacerdot/">Dr. Claudio Sacerdoti Coen</a> on
the EU-funded <a
href="https://www.unibo.it/en/research/projects-and-initiatives/Unibo-Projects-under-7th-Framework-Programme/cooperation-1/information-and-communication-technology-ict-1/cerco">Certified
Complexity</a> project, or CerCo.</p>
<p>CerCo aimed to produce a certified compiler, for a large fragment of C, capable of
automatically lifting precise and reliable concrete complexity bounds from machine code to the original input
source code. I worked on the implementation and verification of the CerCo C compiler backend, using the now
sadly defunct <a href="http://matita.cs.unibo.it">Matita</a> proof assistant.
</p>
</div>
<h2>Education</h2>
<div class="employment">
<span class="employer">Heriot-Watt University, Edinburgh</span>
<span class="employment-period">2007–2010</span>
<p>I obtained my PhD in <emph>theoretical computer science</emph> from the <a
href="https://www.hw.ac.uk/uk/schools/mathematical-computer-sciences.htm">Department of Mathematics and Computer
Science</a> at <a href="https://www.hw.ac.uk">Heriot-Watt University</a>, Edinburgh. I studied various topics at
the intersection of nominal techniques, unification, and type-theory and lambda-calculi. My supervisors were <a
href="https://gabbay.org.uk">Dr. Murdoch “Jamie” Gabbay</a>
and <a href="https://www.dcs.gla.ac.uk/~trinder/">Prof. Phil Trinder</a>.</p>
<p>Whilst a PhD student I used to play rugby union — starting in the backs, before ending up playing as a
loosehead prop in the front row — for <a href="https://www.pitchero.com/clubs/lismore/">Lismore
RUFC</a>. In summer, I also played cricket for <a
href="https://www.pitchero.com/clubs/woodcutterscc/">Woodcutters Cricket Club</a>.</p>
</div>
<div class="employment">
<span class="employer">University of Edinburgh</span>
<span class="employment-period">2003–2007</span>
<p>I graduated with a first-class honours degree in <emph>Artificial Intelligence and Computer Science
</emph> from the <a href="https://informatics.ed.ac.uk">Department of Informatics</a> at the <a
href="https://ed.ac.uk">University of Edinburgh</a>.
</p>
</div>
<h2>Miscellaneous</h2>
<p>My <a href="https://en.wikipedia.org/wiki/Erdős_number">Erdős number</a> is <emph>at most</emph> four: me ⇒ Dowek ⇒
Dershowitz ⇒ Blass ⇒ Erdős.</p>
I am one of the three originators of the <a href="https://srepls.github.io">South of England Regional Programming
Languages</a>, or S-REPLS, seminar series in the South East of England, alongside <a
href="https://www.cl.cam.ac.uk/~jdy22/">Jeremy Yallop</a> and <a href="https://denotational.co.uk">Ohad Kammar</a>.
</body>