Select Publications
Conference Papers
2023, 'AutoCC: Automatic Discovery of Covert Channels in Time-Shared Hardware', in Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023, pp. 871 - 885, http://dx.doi.org/10.1145/3613424.3614254
,2023, 'Pancake: Verified Systems Programming Made Sweeter', in PLOS 2023 - Proceedings of the 12th Workshop on Programming Languages and Operating Systems, Part of: SOSP 2023, pp. 1 - 9, http://dx.doi.org/10.1145/3623759.3624544
,2023, 'First steps in verifying the seL4 Core Platform', in APSys 2023 - Proceedings of the 14th ACM SIGOPS Asia-Pacific Workshop on Systems, pp. 9 - 15, http://dx.doi.org/10.1145/3609510.3609821
,2023, 'Tutorial: Using the seL4 Microkernel', in 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S), IEEE, pp. 4 - 4, presented at 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S), 27 June 2023 - 30 June 2023, http://dx.doi.org/10.1109/dsn-s58398.2023.00016
,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
,2023, 'Verified Value Chains, Innovation and Competition', in Proceedings of the 2023 IEEE International Conference on Cyber Security and Resilience, CSR 2023, pp. 470 - 476, http://dx.doi.org/10.1109/CSR57506.2023.10224911
,2023, 'Pancake: Verified Systems Programming Made Sweeter.', in PLOS@SOSP, ACM, pp. 1 - 9, https://doi.org/10.1145/3623759
,2022, 'Property-Based Testing: Climbing the Stairway to Verification', in SLE 2022 - Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, co-located with SPLASH 2022, pp. 84 - 97, http://dx.doi.org/10.1145/3567512.3567520
,2022, 'Can We Put the 'S' Into IoT?', in 2022 IEEE 8th World Forum on Internet of Things, WF-IoT 2022, http://dx.doi.org/10.1109/WF-IoT54382.2022.10152198
,2021, 'Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core', in Proceedings -Design, Automation and Test in Europe, DATE, pp. 627 - 632, http://dx.doi.org/10.23919/DATE51398.2021.9474214
,2019, 'Fault Tolerance Through Redundant Execution on COTS Multicores: Exploring Trade-Offs', in Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2019, pp. 188 - 200, http://dx.doi.org/10.1109/DSN.2019.00031
,2019, 'SoK: Benchmarking flaws in systems security', in Proceedings - 4th IEEE European Symposium on Security and Privacy, EURO S and P 2019, pp. 310 - 325, http://dx.doi.org/10.1109/EuroSP.2019.00031
,2019, 'Can We Prove Time Protection?', in Proceedings of the Workshop on Hot Topics in Operating Systems, HotOS 2019, pp. 23 - 29, http://dx.doi.org/10.1145/3317550.3321431
,2019, 'Time protection: The missing OS abstraction', in Proceedings of the 14th EuroSys Conference 2019, http://dx.doi.org/10.1145/3302424.3303976
,2019, 'Message from the 2012 USENIX annual technical conference program co-chairs', in Proceedings of the 2012 USENIX Annual Technical Conference, USENIX ATC 2012, pp. VII
,2019, 'VNUMA: A virtual shared-memory multiprocessor', in Proceedings of the 2009 USENIX Annual Technical Conference, pp. 15 - 28
,2018, 'No security without time protection: We need a new hardware-software contract', in Proceedings of the 9th Asia-Pacific Workshop on Systems, APSys 2018, http://dx.doi.org/10.1145/3265723.3265724
,2018, 'The Jury is in: Monolithic OS design is flawed: Microkernel-based designs improve security', in Proceedings of the 9th Asia-Pacific Workshop on Systems, APSys 2018, http://dx.doi.org/10.1145/3265723.3265733
,2018, 'Scheduling-Context Capabilities: A Principled, Light-Weight Operating-System Mechanism for Managing Time', in EuroSys '18: Thirteenth EuroSys Conference 2018, April 23--26, 2018, Porto, Portugal, Portugal, presented at Thirteenth EuroSys Conference 2018, Portugal, 23 April 2018 - 26 March 2018, http://dx.doi.org/10.1145/3190508.3190539
,2017, 'The COGENT case for property-based testing', in Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS 2017, Shanghai, China, pp. 1 - 7, presented at 9th Workshop on Programming Languages and Operating Systems, Shanghai, China, 28 October 2017 - 28 October 2017, http://dx.doi.org/10.1145/3144555.3144556
,2017, 'A performance evaluation of rump kernels as a multi-server OS building block on seL4', in Proceedings of the 8th Asia-Pacific Workshop on Systems, APSys 2017, Mumbai, India, presented at APSys '17 Proceedings of the 8th Asia-Pacific Workshop on Systems, Mumbai, India, 02 September 2017 - 02 September 2017, http://dx.doi.org/10.1145/3124680.3124727
,2016, 'Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis', in 2016 IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016 - Proceedings, Vienna, AUSTRIA, presented at 22nd IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, AUSTRIA, 11 April 2016 - 14 April 2016, http://dx.doi.org/10.1109/RTAS.2016.7461326
,2016, 'COGENT: Verifying high-assurance file system implementations', in International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS, Association for Computing Machinery (ACM), Atlanta, GA, USA, pp. 175 - 188, presented at 21st International Conference on Architectural Support for Programming Languages and Operating Systems, Atlanta, GA, USA, 02 April 2016 - 06 April 2016, http://dx.doi.org/10.1145/2872362.2872404
,2016, 'CATalyst: Defeating last-level cache side channel attacks in cloud computing', in Proceedings - International Symposium on High-Performance Computer Architecture, Barcelona, SPAIN, pp. 406 - 418, presented at 22nd IEEE International Symposium on High-Performance Computer Architecture (HPCA), Barcelona, SPAIN, 12 March 2016 - 16 March 2016, http://dx.doi.org/10.1109/HPCA.2016.7446082
,2015, 'For a Microkernel, a Big Lock Is Fine', in APSys '15 Proceedings of the 6th Asia-Pacific Workshop on Systems, ACM, Tokyo, Japan, presented at ACM Asia-Pacific Workshop on Systems (APSys), Tokyo, Japan, 27 July 2015 - 28 July 2015, http://dx.doi.org/10.1145/2797022.2797042
,2015, 'Report on the Asia-Pacific Systems Workshop 2015 (APSys'15)', in OPERATING SYSTEMS REVIEW, ASSOC COMPUTING MACHINERY, JAPAN, Tokyo, pp. 1 - 2, presented at 6th Asia-Pacific Systems Workshop (APSys), JAPAN, Tokyo, 27 July 2015 - 28 July 2015, http://dx.doi.org/10.1145/2903267.2903269
,2015, 'Last-level cache side-channel attacks are practical', in Proceedings - IEEE Symposium on Security and Privacy, Institute of Electrical and Electronics Engineers (IEEE), CA, San Jose, pp. 605 - 622, presented at 2015 IEEE Symposium on Security and Privacy, CA, San Jose, 18 May 2015 - 20 May 2015, http://dx.doi.org/10.1109/SP.2015.43
,2014, 'Mixed-Criticality Support in a High-Assurance, General-Purpose Microkernel', in Davis R; Cucu-Grosjean L (ed.), 2nd International Workshop on Mixed Criticality Systems, Rome, Italy, pp. 9 - 14, presented at 2nd Workshop on Mixed Criticality Systems, Rome, Italy, 01 December 2014 - 01 December 2014, http://www.nicta.com.au/pub?doc=8354
,2014, 'The last mile: An empirical study of timing channels on seL4', in Proceedings of the ACM Conference on Computer and Communications Security, pp. 570 - 581, http://dx.doi.org/10.1145/2660267.2660294
,2014, 'File systems deserve verification too!', in Operating Systems Review (ACM), pp. 58 - 64, http://dx.doi.org/10.1145/2626401.2626414
,2014, 'Mobile multicores: Use them or waste them', in Operating Systems Review (ACM), pp. 44 - 48, http://dx.doi.org/10.1145/2626401.2626411
,2014, 'Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets', in Real-Time and Embedded Technology and Applications Symposium - Proceedings, Berlin, presented at Real-Time and Embedded Technology and Applications Symposium, Berlin, 15 April 2014 - 17 April 2014
,2014, 'Unifying DVFS and offlining in mobile multicores', in Real-Time and Embedded Technology and Applications - Proceedings, Berlin, presented at Real-Time and Embedded Technology and Applications, Berlin, 15 April 2014 - 17 April 2014
,2013, 'From L3 to seL4: What have we learnt in 20 years of L4 microkernels?', in SOSP 2013 - Proceedings of the 24th ACM Symposium on Operating Systems Principles, pp. 133 - 150, http://dx.doi.org/10.1145/2517349.2522720
,2013, 'Mobile Multicores: Use Them or Waste Them', in Proceedings of the 5th Workshop on Power-Aware Computing and Systems, ACM, Farmington, PA, USA, presented at 5th Workshop on Power-Aware Computing and Systems, Farmington, PA, USA, 03 November 2013 - 03 November 2013
,2013, 'A scalable lock manager for multicores', in Proceedings of the ACM SIGMOD International Conference on Management of Data, pp. 73 - 84, http://dx.doi.org/10.1145/2463676.2465271
,2013, 'The Systems Hacker's Guide to the Galaxy: Energy Usage in a Modern Smartphone', in Proceedings of the 4th Asia-Pacific Workshop on Systems, ACM, New York, NY, presented at APSys'13 Asia-Pacific Workshop on Systems, Singapore, 29 July 2013 - 30 July 2013, http://www.nicta.com.au/pub?id=7044
,2013, 'Correct, fast, maintainable - choose any three!', in Proceedings of the 4th Asia-Pacific Workshop on Systems, ACM, New York, NY, presented at APSys'13 Asia-Pacific Workshop on Systems, Singapore, 29 July 2013 - 30 July 2013, http://dx.doi.org/10.1145/2349896.2349909
,2013, 'Preempt or Not Preempt - That is the Question', in Proceedings of the 4th Asia-Pacific Workshop on Systems, ACM, New York, NY, presented at APSys'13 Asia-Pacific Workshop on Systems, Singapore, 29 July 2013 - 30 July 2013, http://dx.doi.org/10.1145/2349896.2349904
,2013, 'The von Neumann architecture is due for retirement', USENIX, Santa Ana Pueblo, New Mexico, presented at 14th Workshop on Hot Topics in Operating Systems (HotOS XIV), Santa Ana Pueblo, New Mexico, 13 May 2013 - 15 May 2013
,2013, 'RapiLog: Reducing system complexity through verification', in Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013, ACM, Prague; Czech Republic, pp. 323 - 336, presented at 8th ACM European Conference on Computer Systems, EuroSys 2013, Prague; Czech Republic, 15 April 2013 - 17 April 2013, http://dx.doi.org/10.1145/2465351.2465383
,2013, 'Sequoll: A framework for model checking binaries', in Proceedings of the 19th IEEE Real-Time and Embedded Technology and Applications Symposium, IEEE, Philadelphia, USA, presented at 19th IEEE Real-Time and Embedded Technology and Applications Symposium, Philadelphia, USA, 09 April 2013 - 11 April 2013
,2013, 'Code optimizations using formally verified properties', in ACM SIGPLAN Notices, pp. 427 - 441, http://dx.doi.org/10.1145/2544173.2509513
,2013, 'File Systems Deserve Verification Too!', in Programming Languages and Operating Systems (PLOS), pp. 1 - 7
,2012, 'Message from the 2012 USENIX annual technical conference program co-chairs', in Proceedings of the 2012 USENIX Annual Technical Conference, USENIX ATC 2012, Boston, MA, pp. VII - VII, presented at USENIX ATC, Boston, MA, 12 June 2012 - 15 June 2012
,2012, 'Improving Interrupt Response Time in a Verifiable Protected Microkernel', in Proceedings of the 7th ACM European Conference on Computer Systems, ACM, New York, NY, USA, pp. 323 - 336, presented at 7th ACM European Conference on Computer Systems, EuroSys'12, Bern, Switzerland, 10 April 2012 - 13 April 2012, http://dx.doi.org/10.1145/2168836.2168869
,2011, 'Timing Analysis of a Protected Operating System Kernel', in Proceedings of the 32nd Real Time Systems Symposium, IEEE Computer Society, Los Alamitos, USA, pp. 339 - 348, presented at 2011 32nd IEEE Real-Time Systems Symposium, RTSS 2011, Vienna, Austria, 29 November 2011 - 02 December 2011, http://dx.doi.org/10.1109/RTSS.2011.38
,2011, 'Low-Overhead Vlrtualization of Mobile Platforms', in PROCEEDINGS OF THE PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON COMPILERS, ARCHITECTURES AND SYNTHESIS FOR EMBEDDED SYSTEMS (CASES '11), ASSOC COMPUTING MACHINERY, TAIWAN, Taipei, pp. 3 - 3, presented at 14th Confernece on Compilers, Architectures and Synthesis for Embedded Systems (CASES), TAIWAN, Taipei, 09 October 2011 - 14 October 2011, https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000397432700002&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1
,2011, 'Hardware-Supported Virtualization on ARM', in Proceedings of the Second Asia-Pacific Workshop on Systems (APSys'11), ACM, New York, NY, USA, pp. 1 - 5, presented at APSys'11: 2nd ACM SIGOPS Asia-Pacific Workshop on Systems, Shanghai, China, 11 July 2011 - 12 July 2011, http://dx.doi.org/10.1145/2103799.2103813
,2011, 'Protected Hard Real-time: The Next Frontier', in Proceedings of the Second Asia-Pacific Workshop on Systems (APSys'11), ACM, New York, NY, USA, pp. 1 - 5, presented at APSys'11: 2nd ACM SIGOPS Asia-Pacific Workshop on Systems, Shanghai, China, 11 July 2011 - 12 July 2011, http://dx.doi.org/10.1145/2103799.2103801
,