91色情片
Back to
Dr Rob Sison

Dr Rob Sison

Senior Research Associate
  • Doctor of Philosophy: Computer Science and Engineering (91色情片 Sydney, November 2020)
  • Master of Information Technology, with Excellence (91色情片 Sydney, August 2016)
  • Bachelor of Engineering: Computer Engineering, with Honours Class 1 (91色情片 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 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 of The University of Melbourne's , collaborating with the of 91色情片's , my alma mater, aimed at the .

Since 2023 I have held the position of Senior Research Associate working at 91色情片 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,
    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 | 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,
    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 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,
    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

  • , PhD student (91色情片): A framework for reasoning about the multi-core seL4 code.
  • , PhD student (91色情片):聽Compositional formal verification of network services in the seL4 Device Driver Framework.
  • , PhD student (91色情片):聽Verifying inter-component communications in LionsOS.

My Teaching

I have co-lectured:

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