91³ÉÈ˰涶Òô
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 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 ). 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 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 was proud to work as a postdoctoral Research Fellow for the of the University of Melbourne's School of , in close collaboration with the of UNSW Sydney's , my alma mater, aimed at the (ARC DP190103743).

Since 2023 I have held the position of Senior Research Associate working at UNSW Sydney's School of CSE and an Honorary (Fellow) position with the University of Melbourne's School of CIS.

I am a trans nonbinary person and prefer Rob informally and they/them but otherwise don't care what pronouns you use for me.
E-mail
r.sison@unsw.edu.au
  • 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,
  • Journal articles | 2021
    Sison R; Murray T, 2021, 'Verified secure compilation for mixed-sensitivity concurrent programs', Journal of Functional Programming, 31, pp. e18 - e18,
  • 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),
    Preprints | 2023
    Buckley S; Sison R; Wistoff N; Millar C; Murray T; Klein G; Heiser G, 2023, Proving the Absence of Microarchitectural Timing Channels,
    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,
    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,
    Preprints | 2020
    Sison R; Murray T, 2020, Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs, ,
    Theses / Dissertations | 2020
    Sison R, 2020, Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs,
    Conference Papers | 2019
    Sison R; Murray T, 2019, 'Verifying that a compiler preserves concurrent value-dependent information-flow security', in Leibniz International Proceedings in Informatics, LIPIcs,
    Preprints | 2019
    Sison R; Murray T, 2019, Verifying that a compiler preserves concurrent value-dependent information-flow security,
    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,
    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,

  • 2023: , OOPSLA External Review / Artifact Evaluation Committee (SPLASH 2023)
  • 2021: , OOPSLA Artifact Evaluation Committee (SPLASH 2021)
  • 2021: Co-recipient of the (for research contributions to the )
  • 2016-2020: CSIRO Data61 Research Project Award ()

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

  • Pengbo Yan, PhD student (University of Melbourne): Development of formal methods to verify the obliviousness of probabilistic algorithms.

My Teaching

I co-lectured Advanced Topics in Software Verification in T3 2023.