David Cock

ORCID

Publication Activity (10 Years)

Years Active: 2006-2022
Publications (10 Years): 15

Top Venues

CoRR

ITP

PLOS@SOSP

ACM Trans. Embed. Comput. Syst.

University of New South Wales, Sydney, Australia (PHD)

Education History

University of New South Wales, Sydney, Australia

PHD

Publications

Abishek Ramdas, Michael Giardino, Runbin Shi, Adam Turowski, David Cock, Gustavo Alonso, Timothy Roscoe
ECI: a Customizable Cache Coherency Stack for Hybrid FPGA-CPU Architectures. CoRR (2022)
David Cock, Abishek Ramdas, Daniel Schwyn, Michael Giardino, Adam Turowski, Zhenhao He, Nora Hossle, Dario Korolija, Melissa Licciardello, Kristina Martsenko, Reto Achermann, Gustavo Alonso, Timothy Roscoe
Enzian: an open, general, CPU/FPGA platform for systems software research. ASPLOS (2022)
Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel David Schwyn
mmapx: uniform memory protection in a heterogeneous world. HotOS (2021)
Lukas Humbel, Daniel David Schwyn, Nora Hossle, Roni Haecki, Melissa Licciardello, Jan Schaer, David Cock, Michael Giardino, Timothy Roscoe
C Specification. SPIN (2021)
Jasmin Schult, Daniel David Schwyn, Michael Giardino, David Cock, Reto Achermann, Timothy Roscoe
Declarative Power Sequencing. ACM Trans. Embed. Comput. Syst. 20 (5s) (2021)
Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel David Schwyn
Generating correct initial page tables from formal hardware descriptions. PLOS@SOSP (2021)
Gustavo Alonso, Timothy Roscoe, David Cock, Mohsen Ewaida, Kaan Kara, Dario Korolija, David Sidler, Zeke Wang
Tackling Hardware/Software co-design from a database perspective. CIDR (2020)
Reto Achermann, Nora Hossle, Lukas Humbel, Daniel David Schwyn, David Cock, Timothy Roscoe
Secure Memory Management on Modern Hardware. CoRR (2020)
Reto Achermann, Nora Hossle, Lukas Humbel, Daniel David Schwyn, David Cock, Timothy Roscoe
A Least-Privilege Memory Protection Model for Modern Hardware. CoRR (2019)
Roni Haecki, Lukas Humbel, Reto Achermann, David Cock, Daniel David Schwyn, Timothy Roscoe
CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer. CoRR (2019)
Qian Ge, Yuval Yarom, David Cock, Gernot Heiser
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. J. Cryptogr. Eng. 8 (1) (2018)
Reto Achermann, Lukas Humbel, David Cock, Timothy Roscoe
Physical Addressing on Real Hardware in Isabelle/HOL. ITP (2018)
Reto Achermann, Lukas Humbel, David Cock, Timothy Roscoe
Formalizing Memory Accesses and Interrupts. MARS@ETAPS (2017)
Lukas Humbel, Reto Achermann, David Cock, Timothy Roscoe
Towards Correct-by-Construction Interrupt Routing on Real Hardware. PLOS@SOSP (2017)
Qian Ge, Yuval Yarom, David Cock, Gernot Heiser
A Survey of Microarchitectural Timing Attacks and Countermeasures on Contemporary Hardware. IACR Cryptol. ePrint Arch. 2016 (2016)
David Cock, Qian Ge, Toby C. Murray, Gernot Heiser
The Last Mile: An Empirical Study of Timing Channels on seL4. CCS (2014)
David Cock
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle. ITP (2014)
David Cock
pGCL for Isabelle. Arch. Formal Proofs 2014 (2014)
David Cock
Practical Probability: Applying pGCL to Lattice Scheduling. ITP (2013)
David Cock
Verifying Probabilistic Correctness in Isabelle with pGCL SSV (2012)
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
seL4: formal verification of an operating-system kernel. Commun. ACM 53 (6) (2010)
David Cock
Lyrebird - Assigning Meanings to Machines. SSV (2010)
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish
Mind the Gap. TPHOLs (2009)
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
seL4: formal verification of an OS kernel. SOSP (2009)
David Cock, Gerwin Klein, Thomas Sewell
Secure Microkernels, State Monads and Scalable Refinement. TPHOLs (2008)
David Cock
Bitfields and Tagged Unions in C: Verification through Automatic Generation. VERIFY (2008)
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, Manuel M. T. Chakravarty
Running the manual: an approach to high-assurance microkernel development. Haskell (2006)

David Cock.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

David Cock