Thomas Bauereiss
I'm a research associate in the group of Peter Sewell, working on the formal modelling and verification of Instruction Set Architectures. Previously, I was working on techniques for verifying information flow security at DFKI Bremen in the DFG priority programme Reliably Secure Software Systems (RS3).
Publications
Please also see DBLP for a complete list.
-
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture.
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell
In ESOP 2022, pp. 174-203 [ doi | pdf | formal proofs ] -
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process.
Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell
In IEEE Symposium on Security and Privacy 2020, pp. 1003-1020 [ doi | pdf ] -
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS.
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
In POPL 2019, Article 71 [ doi | pdf | supplementary material ] -
CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees.
Thomas Bauereiss, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
In IEEE Symposium on Security and Privacy 2017, pp. 729-748 [ doi | formal proofs ] -
CoSMed: A Confidentiality-Verified Social Media Platform
Thomas Bauereiss, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
In J. Autom. Reason. 61(1-4): 113-139 (2018) [ doi | formal proofs ]
Contact
Mail: Thomas.Bauereiss@cl.cam.ac.uk
Office: FS17
Computer Laboratory
15 JJ Thomson Avenue
Cambridge, CB3 0FD, UK