Select Publications
By Dr Rob Sison
Book Chapters
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, '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
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
,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
,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
,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
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
2020, Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs, http://dx.doi.org/10.26190/5fab5c0a76454
,Preprints
2024, Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version), http://arxiv.org/abs/2407.00514v1
,2023, Proving the Absence of Microarchitectural Timing Channels, http://arxiv.org/abs/2310.17046v1
,2020, Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs, http://dx.doi.org/10.48550/arxiv.2010.14032
,2019, Verifying that a compiler preserves concurrent value-dependent information-flow security, http://dx.doi.org/10.48550/arxiv.1907.00713
,