Rob Sison
Senior Research Associate
(pronouns: they/them)
Research Interests
Rob is a postdoctoral researcher who is broadly interested in discovering how best to design and construct software systems with formally proved functional-correctness and security properties at scale.
Contact Details
| Email: | r.sison@unsw.edu.au |
|---|---|
| Web: | https:/ |
More contact information is available at the Contact page.
Rob is a Senior Research Associate who contributes to the seL4 Microkit and Time Protection verification projects.
For their machine-checked Isabelle/HOL formalisation of a compiler and proof that it preserves concurrent value-dependent noninterference, please see the COVERN project.
Projects
Current |
Past |
Career Summary
From 2020-2023, Rob held the position of Research Fellow in Verified Operating System Security with the School of Computing and Information Systems at the University of Melbourne.
From 2016-2020, Rob's PhD with Trustworthy Systems and UNSW Sydney was supervised by Carroll Morgan, Toby Murray, and Kai Engelhardt.
Previously at NICTA and Data61, Rob was a research engineer developing software for the eChronos/SMACCM project, during which time they ported eChronos to the PowerPC e500. Subsequently as a research engineer they developed proofs for the Information Flow project.
Prior to that, they were a software engineer at Open Kernel Labs, Inc. and General Dynamics C4 Systems, where they spent most of their time developing device-driver paravirtualisation stacks for use by Android and Linux kernel instances on a dual-personality smartphone.
Qualifications
Rob holds the degrees of Doctor of Philosophy (Computer Science and Engineering), Master of Information Technology with Excellence, and Bachelor of Engineering (Computer Engineering) with First Class Honours, all from the University of New South Wales.
Affiliations
- Honorary (Fellow), School of Computing and Information Systems (CIS), University of Melbourne
Program Committees and Editorial Boards
Recognition and Awards
- Distinguished Artifact Reviewer, OOPSLA External Review / Artifact Evaluation Committee (SPLASH 2023)
- Distinguished Artifact Reviewer, OOPSLA Artifact Evaluation Committee (SPLASH 2021)
- 2021 Australian Museum Eureka Prize for Outstanding Science in Safeguarding Australia (with co-entrants Toby Murray and Mark Beaumont) for research contributions to the Cross Domain Desktop Compositor
- CSIRO Data61 Research Project Award (PhD top-up scholarship, 2016-2020)
Publications
Trustworthy Systems Group Papers
2026
|
 |
Kevin Tran, Johannes Åman Pohjola, Rob Sison and Gerwin Klein A rely-guarantee-based simulation for cooperative semantics International Colloquium on Theoretical Aspects of Computing, pp. 87–105, 2026 |
2025
|
|
|
Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser Verifying device drivers with Pancake arXiv preprint, January, 2025 |
2024
|
|
 
|
Rob Sison Verification status of time protection and Microkit-based OS services Talk at the 6th seL4 Summit, October, 2024 |
|
|
|
Trudy Weibel, Zoltan A. Kocsis, Mathieu Paturel, Robert Sison, Isitha Subasinghe and Gernot Heiser Verifying the seL4 Microkit https://trustworthy.systems/publications/papers/Weibel_KPSSH_24.pdf, June, 2024 |
2023
|
|
|
Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser Formalising the prevention of microarchitectural timing channels by operating systems International Symposium on Formal Methods (FM), Lübeck, DE, March, 2023 |
|
|
|
Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein and Gernot Heiser Proving the absence of microarchitectural timing channels arXiv preprint arXiv:2310.17046, 2023 |
2021
|
|
|
Robert Sison and Toby Murray Verified secure compilation for mixed-sensitivity concurrent programs Journal of Functional Programming, Volume 31, pp. e18, 2021 |
2020
|
|
|
Robert Sison Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs PhD Thesis, UNSW, Sydney, Australia, October, 2020 |
2019
|
|
|
Robert Sison and Toby Murray Verifying that a compiler preserves concurrent value-dependent information-flow security International Conference on Interactive Theorem Proving, pp. 27:1–27:19, Portland, USA, September, 2019 |
2018
|
|
|
Toby Murray, Robert Sison and Kai Engelhardt COVERN: A logic for compositional verification of information flow control European Conference on Security and Privacy (EuroS&P), London, UK, April, 2018 |
|
|
|
Robert Sison Per-thread compositional compilation for confidentiality-preserving concurrent programs 2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018 |
2016
|
|
|
Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah Compositional verification and refinement of concurrent value-dependent noninterference IEEE Computer Security Foundations Symposium, pp. 417–431, Lisbon, Portugal, June, 2016 |