-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
229 lines (194 loc) · 15.8 KB
/
index.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
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
218
219
220
221
222
223
224
225
226
227
228
229
<!DOCTYPE html>
<html lang="en">
<head>
<title>Dr Rob Sison</title>
<style>
body {
max-width:1024px;
margin:auto;
padding:8px
}
</style>
</head>
<body>
<h1>Dr Rob Sison</h1>
<p>
🔗
<a href="https://trustworthy.systems/people/?cn=Rob+Sison">Senior Research Associate</a>
<br>
School of Computer Science and Engineering (CSE)<br>
UNSW Engineering
</p>
<p>
🔗
<a href="https://findanexpert.unimelb.edu.au/profile/877887-rob-sison">Honorary (Fellow)</a>
<br>
School of Computing and Information Systems (CIS)<br>
University of Melbourne
</p>
<p>
<img src="RSison_ECAN_2024_final_181x256.jpeg" alt="Professional photo of Dr Rob Sison">
</p>
<div>✉ <a href="mailto:r.sison_AT_unsw.edu.au">r.sison AT unsw.edu.au</a></div>
<div style="padding-top:3px;padding-bottom:3px" itemscope itemtype="https://schema.org/Person"><a itemprop="sameAs" content="https://orcid.org/0000-0003-0313-9764" href="https://orcid.org/0000-0003-0313-9764" target="orcid.widget" rel="me noopener noreferrer" style="vertical-align:top;"><img src="https://orcid.org/sites/default/files/images/orcid_16x16.png" style="width:1em;margin-right:.5em;" alt="ORCID iD icon">https://orcid.org/0000-0003-0313-9764</a></div>
<div style="padding-top:3px">
📣
<a rel="me" href="https://aus.social/@robs">Fediverse (Mastodon)</a> |
<a href="https://github.com/robs-cse">GitHub</a> |
<a href="https://www.linkedin.com/in/robs-cse">LinkedIn</a>
</div>
<h3>Summary</h3>
<p>
I research and develop formal methods, primarily for proving
absences of information flow in systems for high-assurance use cases.
In the past, my focus was on complications arising from concurrency and
refinement to enable secure compilation;
more recently, it has been on how to prove an OS enforces absences of information leaks through the microarchitecture.
More broadly, I am interested in
all applications of
interactive theorem proving, as well as
anything to do with the design and construction of software systems with
formally proved functional-correctness and security properties at scale.
</p>
<h3>About me</h3>
<p>
I am an Australian computer engineer who pivoted to formal methods research
after a 5-year early career stint (2008-2014) as an OS-level software
developer with NICTA spin-out Open Kernel Labs, Inc.
(including following its <a href="https://www.prnewswire.com/news-releases/general-dynamics-acquires-open-kernel-labs-inc-169231176.html">acquisition</a>
by General Dynamics C4 Systems).
</p>
<p>
My long-term objective since 2014 has been to gain the skills, experience, and
qualifications necessary to assist, conduct, and eventually lead groundbreaking
research and development aimed at improving the trustworthiness and reliability
of system-critical software.
</p>
<p>
To this end, in 2016 I completed a master's degree by coursework focused on
computer security and formal methods. In 2020, I attained my doctorate
for <a href="https://doi.org/10.26190/5fab5c0a76454">my dissertation</a> on the
application of <i>interactive theorem proving</i> to make feasible the
verification of both
<i>information-flow security and its preservation by a compiler</i> for
concurrent programs that share memory both (1) between threads and
(2) between security domains.
</p>
<p>
From 2020 to 2023 I was proud to work
as a postdoctoral Research Fellow for
the <a href="https://brokenassumptions.org/">CS Security Research group</a> of
The University of Melbourne's
<a href="https://cis.unimelb.edu.au/">School of Computing and Information Systems (CIS)</a>,
in close collaboration with
the <a href="https://trustworthy.systems/">Trustworthy Systems research group</a> of UNSW Sydney's <a href="https://www.cse.unsw.edu.au">School of Computer Science and Engineering (CSE)</a>, my alma mater,
aimed at the <a href="https://findanexpert.unimelb.edu.au/project/104542-provable-elimination-of-information-leakage-through-timing-channels"><i>provable elimination of information leakage through timing channels</i></a> (ARC DP190103743).
</p>
<p>
Since 2023 I have held the position of Senior Research Associate working <a href="https://trustworthy.systems/people/?cn=Rob+Sison">with the Trustworthy Systems research group</a> at UNSW Sydney's School of CSE and an Honorary (Fellow) position with the University of Melbourne's School of CIS.
</p>
<p>
I am a trans nonbinary person and in professional contexts prefer Rob and they/them but otherwise don't care what pronouns you use for me.
</p>
<h3>Research supervision</h3>
<p>
I am happy to co-supervise anybody who is interested in a pursuing a Higher Degree Research candidature on any of the topics in my area of research.
</p>
<p>
Please contact me by email at my <a href="mailto:r.sison_AT_unsw.edu.au">institutional</a> email address to discuss our research interests and your circumstances.
</p>
<p>
If you have a <i>professional</i> online presence, especially <i>hosted or verified by</i> any institutional websites (e.g. employer or university), public code repositories (e.g. GitHub) or publication databases (e.g. DBLP), please include any links to those.
</p>
<h3>Other contact</h3>
<p>
On other professional matters, feel free to email me at either of my <a href="mailto:r.sison_AT_unsw.edu.au">institutional</a> or <a href="mailto:robs.cse_AT_fastmail.com">personal</a> email address - <b>no unsolicited attachments</b> please.
</p>
<h3>Institutional pages</h3>
<ul>
<li><a href="https://trustworthy.systems/people/?cn=Rob+Sison">Trustworthy Systems group @ UNSW Sydney</a></li>
<li><a href="https://research.unsw.edu.au/people/dr-rob-sison">UNSW Sydney Researcher Profile</a></li>
<li><a href="https://www.unsw.edu.au/staff/robert-sison">UNSW Sydney (Staff page)</a></li>
<li><a href="https://findanexpert.unimelb.edu.au/profile/877887-rob-sison">The University of Melbourne (Find an Expert)</a></li>
</ul>
<h3>Teaching - UNSW Sydney</h3>
<ul>
<li><a href="https://www.cse.unsw.edu.au/~cs3161/">COMP3161/9164</a> Concepts of Programming Languages (T3 2024), co-lecturer</li>
<li><a href="https://www.cse.unsw.edu.au/~cs4161/">COMP4161</a> Advanced Topics in Software Verification (T3 2023, 2024), co-lecturer</li>
</ul>
<h3>Current research students</h3>
<ul>
<li><a href="https://www.linkedin.com/in/pengbo-yan-7b48471b2/">Pengbo Yan</a>, PhD student (with <a href="https://people.eng.unimelb.edu.au/tobym/">Toby Murray</a> and <a href="https://findanexpert.unimelb.edu.au/profile/143325-olya-ohrimenko">Olya Ohrimenko</a>), The University of Melbourne</li>
<li><a href="https://trustworthy.systems/people/?cn=Kevin+Tran">Kevin Tran</a>, PhD student (with <a href="https://trustworthy.systems/people/?cn=Johannes+%C3%85man+Pohjola">Johannes Åman Pohjola</a> and <a href="https://trustworthy.systems/people/?cn=Gerwin+Klein">Gerwin Klein</a>), UNSW Sydney</li>
<li><a href="https://trustworthy.systems/people/?cn=Junming+Zhao">Junming Zhao</a>, PhD student (with <a href="https://trustworthy.systems/people/?cn=Thomas+Sewell">Thomas Sewell</a> and <a href="https://trustworthy.systems/people/?cn=Gernot+Heiser">Gernot Heiser</a>), UNSW Sydney</li>
<li><a href="https://trustworthy.systems/people/?cn=Kurt+Wu">Kurt Wu</a>, Master's research project student, UNSW Sydney</li>
</ul>
<h3>Completed research students</h3>
<ul>
<li><a href="https://trustworthy.systems/people/?cn=Mathieu+Paturel">Mathieu Paturel</a>, Honours thesis student, UNSW Sydney</li>
</ul>
<h3>Selected peer-reviewed publications</h3>
<ul>
<li><b>Latest lead-authored:</b>
R. Sison, S. Buckley, T. Murray, G. Klein and G. Heiser, "<a href="publications/FM23_accepted.pdf">Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems</a>," <i>25th International Symposium on Formal Methods (FM)</i>, pp. 103-121, 2023. doi: <a href="https://doi.org/10.1007/978-3-031-27481-7_8">10.1007/978-3-031-27481-7_8</a>.</li>
<li><b>Journal article on PhD work:</b>
R. Sison and T. Murray, "<a href="publications/JFPSC_accepted_plus_appendices.pdf">Verified secure compilation for mixed-sensitivity concurrent programs</a>," <i>Journal of Functional Programming</i>, vol. 31, p. e18, 2021. doi: <a href="https://doi.org/10.1017/s0956796821000162">10.1017/S0956796821000162</a>.</li>
<li><b>Doctoral dissertation:</b>
R. Sison, "<a href="http://hdl.handle.net/1959.4/70452">Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs</a>," PhD thesis, University of New South Wales, Sydney, 2020. doi: <a href="https://doi.org/10.26190/5fab5c0a76454">10.26190/5fab5c0a76454</a>.</li>
<li><b>Most cited:</b>
T. Murray, R. Sison, E. Pierzchalski and C. Rizkallah, "<a href="https://doi.org/10.1109/csf.2016.36">Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference</a>," <i>IEEE 29th Computer Security Foundations Symposium (CSF)</i>, pp. 417-431, 2016. doi: <a href="https://doi.org/10.1109/csf.2016.36">10.1109/CSF.2016.36</a>.</li>
</ul>
<h3>Proof artifacts and contributions</h3>
<ul>
<li><a href="https://doi.org/10.5281/zenodo.7340166">An Isabelle/HOL Formalisation of Microarchitectural Timing Channel Prevention by Operating Systems</a> (for <a href="https://trustworthy.systems/publications/papers/Sison_BMKH_23.abstract"><i>Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems</i></a>, 2023)</li>
<li><a href="https://github.com/seL4/l4v/commit/98c2889f1b66d82bfa8633d8c4d2d32df5c43fa7">A tutorial for seL4/l4v's EquivValid library</a></li>
<li><a href="https://covern.org/">COVERN-RG logic and compiler</a>
<ul>
<li><a href="https://covern.org/jfpsc.html">JFP artifact</a> (for <a href="https://doi.org/10.1017/s0956796821000162"><i>Verified secure compilation for mixed-sensitivity concurrent programs</i></a>, 2021)</li>
<li><a href="http://handle.unsw.edu.au/1959.4/unsworks_72923">Dissertation artifact</a> (for <a href="https://doi.org/10.26190/5fab5c0a76454"><i>Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs</i></a>, 2020)</li>
<li><a href="https://bitbucket.org/covern/covern/">Public repository incl. EuroS&P'18 artifact</a> (for <a href="https://doi.org/10.1109/eurosp.2018.00010"><i>COVERN: A Logic for Compositional Verification of Information Flow Control</i></a>, 2018)</li>
</ul></li>
<li><a href="https://www.isa-afp.org/entries/Dependent_SIFUM_Type_Systems.html">Dependent_SIFUM_Type_Systems</a> and <a href="https://www.isa-afp.org/entries/Dependent_SIFUM_Refinement.html">Dependent_SIFUM_Refinement</a> (for <a href="https://doi.org/10.1109/csf.2016.36"><i>Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference</i></a>, 2016)</li>
</ul>
<h3>Other publications listings</h3>
<ul>
<li><a href="https://orcid.org/0000-0003-0313-9764">ORCID</a></li>
<li><a href="https://dblp.org/pid/182/4864.html">dblp</a></li>
<li><a href="https://www.webofscience.com/wos/author/record/KHY-1932-2024">Web of Science</a></li>
<li><a href="https://www.scopus.com/authid/detail.uri?authorId=57191043310">Scopus</a></li>
<li><a href="https://scholar.google.com/citations?user=-BwpreQAAAAJ">Google Scholar</a></li>
</ul>
<h3>Awards and recognition</h3>
<ul>
<li><a href="https://2023.splashcon.org/track/splash-2023-Artifacts#distinguished-artifact-reviewers">Distinguished Artifact Reviewer</a>, OOPSLA External Review / Artifact Evaluation Committee (SPLASH 2023)</li>
<li><a href="https://2021.splashcon.org/track/splash-2021-Artifacts#distinguished-artifact-reviewers">Distinguished Artifact Reviewer</a>, OOPSLA Artifact Evaluation Committee (SPLASH 2021)</li>
<li><a href="https://australian.museum/get-involved/eureka-prizes/2021-eureka-prizes-winners/#safeguarding">2021 Australian Museum Eureka Prize for Outstanding Science in Safeguarding Australia</a> (with co-entrants <a href="https://pursuit.unimelb.edu.au/articles/using-maths-to-prove-computer-security">Toby Murray</a> and <a href="https://www.dst.defence.gov.au/news/2021/10/06/innovative-computing-device-wins-eureka-prize">Mark Beaumont</a>) for research contributions to the <a href="https://trustworthy.systems/projects/TS/cddc">Cross Domain Desktop Compositor</a></li>
<li>CSIRO Data61 Research Project Award (<a href="https://www.csiro.au/en/careers/Scholarships-student-opportunities/Postgraduate-programs-and-Scholarships/Data61-scholarships">PhD top-up scholarship</a>, 2016-2020)</li>
</ul>
<h3>Community participation</h3>
<ul>
<li>PLDI Review Committee (PLDI 2025), <a href="https://pldi25.sigplan.org/committee/pldi-2025-papers-pldi-review-committee">committee member</a></li>
<li>ACM Transactions on Privacy and Security (TOPS 2024), reviewer</li>
<li>seL4 Summit 2024, <a href="https://sel4summit2024.sched.com/event/1em2G">presenter</a> (<a href="https://static.sched.com/hosted_files/sel4summit2024/fd/VerifStatus-TimeProt-OSServices_RSison.pdf">slides</a>)</li>
<li>PLAS Program Committee (PLAS 2024), <a href="https://plas24.github.io/">committee member</a></li>
<li>Future Communications Workshop @ Macquarie University (2024), <a href="https://sites.google.com/view/futurecommunicationsworkshop/schedule">presenter</a></li>
<li>Workshop on Formal Methods in Australia/New Zealand (FM-Oz/NZ 2024), presenter (<a href="slides/2024-FMOZNZ_RSison-delivered.pdf">slides</a>)</li>
<li>ECOOP Artifact Evaluation + Extended Review Committees (ECOOP 2024), committee member (<a href="https://2024.ecoop.org/committee/ecoop-2024-artifact-evaluation-artifact-evaluation-committee">AEC</a>, <a href="https://2024.ecoop.org/committee/ecoop-2024-papers-extended-review-committee-and-external-reviewers">ERC</a>)</li>
<li>2024 Australasian Computer Science Week (ACSW) EnCore Talks, <a href="https://acsw.core.edu.au/program">presenter</a></li>
<li>PLDI Review Committee (PLDI 2024), <a href="https://pldi24.sigplan.org/committee/pldi-2024-papers-pldi-review-committee">committee member</a></li>
<li>Workshop on Formal Methods in Australia/New Zealand (FM-Oz/NZ 2023), presenter (<a href="slides/2023-FM-OZNZ.pdf">slides</a>)</li>
<li>25th International Symposium on Formal Methods (FM 2023), <a href="https://trustworthy.systems/publications/papers/Sison_BMKH_23.abstract">presenter</a> (<a href="https://trustworthy.systems/publications/papers/Sison_BMKH_23.slides.pdf">slides</a>)</li>
<li>Southern Summer School on Systems and Software Security (SSS<sup>2</sup> 2023), <a href="https://cs.adelaide.edu.au/~yval/SSS2/program.html">presenter</a> (<a href="https://trustworthy.systems/publications/papers/Sison%3Aphd.slides.pdf">slides</a>)</li>
<li>OOPSLA External Review / Artifact Evaluation Committee (SPLASH 2023), <a href="https://2023.splashcon.org/committee/splash-2023-oopsla-external-review---artifact-evaluation-committee">committee member</a></li>
<li>Trustworthy Systems group Monday talks @ UNSW Sydney (2022), schedule organiser</li>
<li>OOPSLA Artifact Evaluation Committee (SPLASH 2021), <a href="https://2021.splashcon.org/committee/splash-2021-Artifacts-artifact-evaluation-committee">committee member</a></li>
<li>CIS research seminar program @ University of Melbourne (2021), <a href="https://youtu.be/AD7fGEZqid8">presenter</a></li>
<li>10th International Conference on Interactive Theorem Proving (ITP 2019), <a href="https://trustworthy.systems/publications/csiroabstracts/Sison_Murray_19.abstract">presenter</a></li>
<li>Marktoberdorf Summer School 2018 (Engineering Secure and Dependable Software Systems), <a href="https://sites.google.com/site/marktoberdorf2018/">attendee</a></li>
<li>2nd DeepSpec Summer School on Verified Systems (DSSS 2018), <a href="https://deepspec.org/event/dsss18/">attendee</a></li>
<li>Programming Languages Mentoring Workshop (PLMW @ POPL 2018), <a href="https://popl18.sigplan.org/track/PLMW-POPL-2018">attendee</a></li>
<li>2nd Workshop on Principles of Secure Compilation (PriSC @ POPL 2018), <a href="https://popl18.sigplan.org/details/prisc-2018/2/Per-Thread-Compositional-Compilation-for-Confidentiality-Preserving-Concurrent-Progra">presenter</a></li>
</ul>
<a href="https://github.com/robs-cse/robs-cse.github.io/commits/main">Change history</a>
</body>
</html>