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 acquisition by General Dynamics). 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 was proud to work as a postdoctoral Research Fellow for the CS Security Research group of the University of Melbourne's School of Computing and Information Systems (CIS), in close collaboration with the Trustworthy Systems research group of UNSW Sydney's School of Computer Science and Engineering (CSE), my alma mater, aimed at the provable elimination of information leakage through timing channels (ARC DP190103743).

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 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, 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; Legnani A; Ung TT; Truong H; Sau TW; Tanaka M; Pohjola JÅ; Sewell T; Sison R; Syeda H; Myreen M; Norrish M; Heiser G, 2025, Verifying Device Drivers with Pancake, http://arxiv.org/abs/2501.08249v1
    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.48550/arxiv.2010.14032
    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 Leibniz International Proceedings in Informatics, LIPIcs, 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.48550/arxiv.1907.00713
    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

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

My Teaching

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