David A. Cock

33 papers A* 3A 3B 4C 1Journal 10Unranked 11
YearRankTypeTitle / Venue / Authors
2024 J jnl
Rethinking Programmed I/O for Fast Devices, Cheap Cores, and Coherent Interconnects.
CoRR
Anastasiia Ruzhanskaia, Pengcheng Xu, David A. Cock, Timothy Roscoe
2024 B conf
Semi-Open-State Testing for in-Silicon Coherent Interconnects.
FMCAD
Jasmin Schult, Ben Fiedler, David A. Cock, Timothy Roscoe
2024 — conf
Verified Fault Handling for Modern Board Management Controllers.
FACS
Ben Fiedler, Zikai Liu, David A. Cock, Timothy Roscoe
2023 A conf
Putting out the hardware dumpster fire.
HotOS
Ben Fiedler, Daniel Schwyn, Constantin Gierczak-Galle, David A. Cock, Timothy Roscoe
2022 J jnl
ECI: a Customizable Cache Coherency Stack for Hybrid FPGA-CPU Architectures.
CoRR
Abishek Ramdas, Michael Giardino, Runbin Shi, Adam Turowski, David A. Cock, Gustavo Alonso, Timothy Roscoe
2022 A* conf
Enzian: an open, general, CPU/FPGA platform for systems software research.
ASPLOS
David A. 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
2021 — conf
A Model-Checked I
SPIN
Lukas Humbel, Daniel David Schwyn, Nora Hossle, Roni Haecki, Melissa Licciardello, Jan Schaer, David A. Cock, Michael Giardino, Timothy Roscoe
2021 J jnl
Declarative Power Sequencing.
ACM Trans. Embed. Comput. Syst.
Jasmin Schult, Daniel David Schwyn, Michael Giardino, David A. Cock, Reto Achermann, Timothy Roscoe
2021 — conf
Generating correct initial page tables from formal hardware descriptions.
PLOS@SOSP
Reto Achermann, David A. Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel David Schwyn
2021 A conf
mmapx: uniform memory protection in a heterogeneous world.
HotOS
Reto Achermann, David A. Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, Daniel David Schwyn
2020 J jnl
Secure Memory Management on Modern Hardware.
CoRR
Reto Achermann, Nora Hossle, Lukas Humbel, Daniel David Schwyn, David A. Cock, Timothy Roscoe
2020 A conf
Tackling Hardware/Software co-design from a database perspective.
CIDR
Gustavo Alonso, Timothy Roscoe, David A. Cock, Mohsen Ewaida, Kaan Kara, Dario Korolija, David Sidler, Zeke Wang
2019 J jnl
A Least-Privilege Memory Protection Model for Modern Hardware.
CoRR
Reto Achermann, Nora Hossle, Lukas Humbel, Daniel David Schwyn, David A. Cock, Timothy Roscoe
2019 J jnl
CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer.
CoRR
Roni Haecki, Lukas Humbel, Reto Achermann, David A. Cock, Daniel David Schwyn, Timothy Roscoe
2018 J jnl
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware.
J. Cryptogr. Eng.
Qian Ge, Yuval Yarom, David A. Cock, Gernot Heiser
2018 B conf
Physical Addressing on Real Hardware in Isabelle/HOL.
ITP
Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe
2017 — conf
Formalizing Memory Accesses and Interrupts.
MARS
Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe
2017 — conf
Towards Correct-by-Construction Interrupt Routing on Real Hardware.
PLOS@SOSP
Lukas Humbel, Reto Achermann, David A. Cock, Timothy Roscoe
2016 J jnl
A Survey of Microarchitectural Timing Attacks and Countermeasures on Contemporary Hardware.
IACR Cryptol. ePrint Arch.
Qian Ge, Yuval Yarom, David A. Cock, Gernot Heiser
2014 B conf
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle.
ITP
David A. Cock
2014 — —
Leakage in Trustworthy Systems.
David A. Cock
2014 A* conf
The Last Mile: An Empirical Study of Timing Channels on seL4.
CCS
David A. Cock, Qian Ge, Toby C. Murray, Gernot Heiser
2014 J jnl
pGCL for Isabelle.
Arch. Formal Proofs
David A. Cock
2013 B conf
Practical Probability: Applying pGCL to Lattice Scheduling.
ITP
David A. Cock
2012 — conf
Verifying Probabilistic Correctness in Isabelle with pGCL
SSV
David A. Cock
2011 — conf
Exploitation as an inference problem.
AISec
David A. Cock
2010 — conf
Lyrebird - Assigning Meanings to Machines.
SSV
David A. Cock
2010 J jnl
seL4: formal verification of an operating-system kernel.
Commun. ACM
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
2009 — conf
Mind the Gap.
TPHOLs
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish
2009 A* conf
seL4: formal verification of an OS kernel.
SOSP
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
2008 — conf
Bitfields and Tagged Unions in C: Verification through Automatic Generation.
VERIFY
David A. Cock
2008 — conf
Secure Microkernels, State Monads and Scalable Refinement.
TPHOLs
David A. Cock, Gerwin Klein, Thomas Sewell
2006 C conf
Running the manual: an approach to high-assurance microkernel development.
Haskell
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty