Back to
Dr Rob Sison

Dr Rob Sison

Senior Research Associate
  • Doctor of Philosophy: Computer Science and Engineering (UNSW Sydney, November 2020)
  • Master of Information Technology, with Excellence (UNSW Sydney, August 2016)
  • Bachelor of Engineering: Computer Engineering, with Honours Class 1 (UNSW Sydney, May 2010)
Engineering
Computer Science and Engineering

I am an Australian formal methods researcher who pivoted to academia after a 5-year early career stint (2008-2014) as an OS-level software engineer with NICTA spin-out Open Kernel Labs, Inc. 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.

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 my dissertation on the application of interactive theorem proving to make feasible the verification of both information-flow security and its preservation by a compiler for concurrent programs that share memory both (1) between threads and (2) between security domains. From 2020 to 2023 I worked for the CS Security Research group of The University of Melbourne's School of CIS, collaborating with the Trustworthy Systems research group of UNSW's School of CSE, my alma mater, aimed at the provable elimination of information leakage through timing channels.

Since 2023 I have held the position of Senior Research Associate working with the Trustworthy Systems research group at UNSW Sydney's School of CSE.

I am a trans nonbinary person and in professional contexts would appreciate being referred to with they/them pronouns.
E-mail
r.sison@unsw.edu.au
  • Book Chapters | 2026
    Tran K; Pohjola JÅ; Sison R; Klein G, 2026, 'A Rely-Guarantee-Based Simulation for Cooperative Semantics', in , pp. 87 - 105, http://dx.doi.org/10.1007/978-3-032-11176-0_7
    Book Chapters | 2025
    Yan P; Murray T; Ohrimenko O; Pham VT; Sison R, 2025, 'Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms', in , pp. 188 - 205, http://dx.doi.org/10.1007/978-3-031-71162-6_10
  • Journal articles | 2021
    Sison R; Murray T, 2021, 'Verified secure compilation for mixed-sensitivity concurrent programs', Journal of Functional Programming, 31, pp. e18 - e18, http://dx.doi.org/10.1017/S0956796821000162
  • Preprints | 2025
    Zhao J; Tanaka M; Pohjola JÅ; Legnani A; Ung TT; Truong H; Sau TW; Sewell T; Sison R; Syeda H; Myreen M; Norrish M; Heiser G, 2025, Verifying Device Drivers with Pancake, http://arxiv.org/abs/2501.08249v2
    Preprints | 2024
    Yan P; Murray T; Ohrimenko O; Pham V-T; Sison R, 2024, Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version), http://arxiv.org/abs/2407.00514v1
    Preprints | 2023
    Buckley S; Sison R; Wistoff N; Millar C; Murray T; Klein G; Heiser G, 2023, Proving the Absence of Microarchitectural Timing Channels, http://arxiv.org/abs/2310.17046v1
    Conference Papers | 2023
    Sison R; Buckley S; Murray T; Klein G; Heiser G, 2023, 'Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems', in Katoen JP; Chechik M; Leucker M (eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, Lübeck, Germany, pp. 103 - 121, presented at Formal Methods (FM 2023), Lübeck, Germany, 06 March 2023 - 10 March 2023, http://dx.doi.org/10.1007/978-3-031-27481-7_8
    Software / Code | 2020
    Sison R; Murray T; Pierzchalski E; Engelhardt K; Rizkallah C, 2020, COVERN-RG release of Isabelle/HOL theories for Robert Sison's PhD thesis, Published: 2020, Software / Code, http://dx.doi.org/10.26190/unsworks/27878
    Preprints | 2020
    Sison R; Murray T, 2020, Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs, http://dx.doi.org/10.1017/S0956796821000162
    Theses / Dissertations | 2020
    Sison R, 2020, Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs, http://dx.doi.org/10.26190/5fab5c0a76454
    Conference Papers | 2019
    Sison R; Murray T, 2019, 'Verifying that a compiler preserves concurrent value-dependent information-flow security', in Harrison J; O'Leary J; Tolmach A (eds.), Leibniz International Proceedings in Informatics Lipics, SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS, OR, Portland, presented at 10th International Conference on Interactive Theorem Proving-ITP, OR, Portland, 09 September 2019 - 12 September 2019, http://dx.doi.org/10.4230/LIPIcs.ITP.2019.27
    Preprints | 2019
    Sison R; Murray T, 2019, Verifying that a compiler preserves concurrent value-dependent information-flow security, http://dx.doi.org/10.4230/LIPIcs.ITP.2019.27
    Conference Papers | 2018
    Murray T; Sison R; Engelhardt K, 2018, 'COVERN: A Logic for Compositional Verification of Information Flow Control', in Piessens F; Smith M (ed.), IEEE, London, presented at 3rd IEEE European Symposium on Security and Privacy, London, 24 April 2018 - 26 April 2018, http://dx.doi.org/10.1109/EuroSP.2018.00010
    Conference Papers | 2016
    Murray T; Sison R; Pierzchalski E; Rizkallah C, 2016, 'Compositional verification and refinement of concurrent value-dependent noninterference', in Proceedings - IEEE Computer Security Foundations Symposium, IEEE, Lisbon, PORTUGAL, presented at IEEE 29th Computer Security Foundations Symposium (CSF), Lisbon, PORTUGAL, 27 June 2016 - 01 July 2016, http://dx.doi.org/10.1109/CSF.2016.36

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.

My Research Supervision

  • Kevin Tran, PhD student (UNSW): A framework for reasoning about the multi-core seL4 code.
  • Junming Zhao, PhD student (UNSW): Compositional formal verification of network services in the seL4 Device Driver Framework.
  • Kurt Wu, PhD student (UNSW): Verifying inter-component communications in LionsOS.

My Teaching

I have co-lectured:

  • COMP3161/9164 Concepts of Programming Languages in T3 2024 and 2025.
  • COMP4161 Advanced Topics in Software Verification in T3 2023, 2024 and 2025.