Trustworthy Systems

Robert Sison
Senior Research Associate

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

More contact information is available at the Contact page.

Photo of Robert Sison

Publication List

Rob is a Senior Research Associate who contributes to the seL4 Core Platform 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.




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.


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.

Program Committees and Editorial Boards

Recognition and Awards


Trustworthy Systems Group Papers


PDF 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
Abstract PDF 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


Abstract PDF Robert Sison and Toby Murray
Verified secure compilation for mixed-sensitivity concurrent programs
Journal of Functional Programming, Volume 31, pp. e18, 2021


PDF Robert Sison
Proving confidentiality and its preservation under compilation for mixed-sensitivity concurrent programs
PhD Thesis, UNSW, Sydney, Australia, October, 2020


PDF 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


Abstract PDF 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, United Kingdom, April, 2018
PDF Robert Sison
Per-thread compositional compilation for confidentiality-preserving concurrent programs
2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018


Abstract PDF Toby Murray, Robert Sison, Ed 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