By Dr Rob Sison

Book Chapters

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

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

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

Conference Papers

Sison R; Buckley S; Murray T; Klein G; Heiser G, 2023, 'Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 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

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

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

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

Software / Code

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

Theses / Dissertations

Sison R, 2020, Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs, http://dx.doi.org/10.26190/5fab5c0a76454

Preprints

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://dx.doi.org/10.48550/arxiv.2501.08249

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://dx.doi.org/10.48550/arxiv.2407.00514

Buckley S; Sison R; Wistoff N; Millar C; Murray T; Klein G; Heiser G, 2023, Proving the Absence of Microarchitectural Timing Channels, http://dx.doi.org/10.48550/arxiv.2310.17046

Sison R; Murray T, 2022, Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs, http://dx.doi.org/10.48550/arxiv.2010.14032

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

Back to profile page