Personal information

Verified email addresses

Verified email domains

Switzerland, Australia

Activities

Employment (2)

ETH Zurich: Zurich, CH

2015 to present | Senior Researcher (D-INFK)
Employment
Source: Self-asserted source
David Cock

National ICT Australia: Sydney, NSW, AU

2006 to 2015 | Research Engineer (Trustworthy Systems)
Employment
Source: Self-asserted source
David Cock

Education and qualifications (2)

UNSW Sydney: Sydney, New South Wales, AU

2009-07 to 2014-08 | Ph.D. (Computer Science and Engineering)
Education
Source: Self-asserted source
David Cock

UNSW Sydney: Sydney, New South Wales, AU

2000-01 to 2005-05 | Bachelor of Science (Advanced Science, Mathematics and Computer Science) (Computer Science and Engineering)
Education
Source: Self-asserted source
David Cock

Professional activities (7)

Association for Computing Machinery: New York, US

2023 to 2023 | Program Committee (Eurosys)
Service
Source: Self-asserted source
David Cock

Association for Computing Machinery: New York, US

2023 to 2023 | Program Committee (PLOS)
Service
Source: Self-asserted source
David Cock

USENIX Association: Berkeley, CA, US

2021 to 2023 | Program Committee (ATC)
Service
Source: Self-asserted source
David Cock

Association for Computing Machinery: New York, US

2022 | Software System Award
Distinction
Source: Self-asserted source
David Cock

Association for Computing Machinery: New York, NY, US

2019 to 2021 | Program Committee (EMSOFT)
Service
Source: Self-asserted source
David Cock

IEEE: New York, NY, US

2020 | Program Committee (RTAS 2020)
Service
Source: Self-asserted source
David Cock

USENIX Association: Berkeley, CA, US

2019 | Program Committee (ATC 2019)
Service
Source: Self-asserted source
David Cock

Works (28)

Verified Fault Handling for Modern Board Management Controllers

2024 | Book chapter
Contributors: Ben Fiedler; Zikai Liu; David Cock; Timothy Roscoe
Source: check_circle
Crossref

Putting out the hardware dumpster fire

2023-06-22 | Conference paper
Contributors: Ben Fiedler; Daniel Schwyn; Constantin Gierczak-Galle; David Cock; Timothy Roscoe
Source: check_circle
Crossref

Enzian: An Open, General, CPU/FPGA Platform for Systems Software Research

International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
2022 | Conference paper
EID:

2-s2.0-85126391855

Contributors: Cock, D.; Ramdas, A.; Schwyn, D.; Giardino, M.; Turowski, A.; He, Z.; Hossle, N.; Korolija, D.; Licciardello, M.; Martsenko, K. et al.
Source: Self-asserted source
David Cock via Scopus - Elsevier

A Model-Checked I2C Specification

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2021 | Book
EID:

2-s2.0-85113716801

Part of ISSN: 16113349 03029743
Contributors: David Cock
Source: Self-asserted source
David Cock
grade
Preferred source (of 2)‎

Declarative Power Sequencing

ACM Transactions on Embedded Computing Systems
2021 | Journal article
EID:

2-s2.0-85115836256

Part of ISSN: 15583465 15399087
Contributors: Schult, J.; Schwyn, D.; Giardino, M.; Cock, D.; Achermann, R.; Roscoe, T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Generating correct initial page tables from formal hardware descriptions

PLOS 2021 - Proceedings of the 2021 11th Workshop on Programming Languages and Operating Systems
2021 | Conference paper
EID:

2-s2.0-85119090214

Contributors: Achermann, R.; Cock, D.; Haecki, R.; Hossle, N.; Humbel, L.; Roscoe, T.; Schwyn, D.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Mmapx: Uniform memory protection in a heterogeneous world

HotOS 2021 - Proceedings of the 2021 Workshop on Hot Topics in Operating Systems
2021 | Conference paper
EID:

2-s2.0-85107859266

Contributors: Achermann, R.; Cock, D.; Haecki, R.; Hossle, N.; Humbel, L.; Roscoe, T.; Schwyn, D.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Secure Memory Management on Modern Hardware

arXiv
2020 | Other
EID:

2-s2.0-85098389173

Part of ISSN: 23318422
Contributors: Achermann, R.; Hossle, N.; Humbel, L.; Schwyn, D.; Cock, D.; Roscoe, T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

A least-privilege memory protection model for modern hardware

arXiv
2019 | Other
EID:

2-s2.0-85094225511

Part of ISSN: 23318422
Contributors: Achermann, R.; Hossle, N.; Humbel, L.; Schwyn, D.; Cock, D.; Roscoe, T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

CleanQ: A lightweight, uniform, formally specified interface for intra-machine data transfer

arXiv
2019 | Other
EID:

2-s2.0-85093150821

Part of ISSN: 23318422
Contributors: Haecki, R.; Humbel, L.; Achermann, R.; Cock, D.; Schwyn, D.; Roscoe, T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Physical Addressing on Real Hardware in Isabelle/HOL

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2018 | Book
EID:

2-s2.0-85049882391

Part of ISSN: 16113349 03029743
Contributors: Achermann, R.; Humbel, L.; Cock, D.; Roscoe, T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Formalizing Memory Accesses and Interrupts

2017 | Journal article
Contributors: Reto Achermann; Lukas Humbel; David Cock; Timothy Roscoe
Source: Self-asserted source
David Cock via BASE - Bielefeld Academic Search Engine
grade
Preferred source (of 2)‎

Towards correct-by-construction interrupt routing on real hardware

Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS 2017
2017 | Conference paper
EID:

2-s2.0-85037173197

Contributors: Humbel, L.; Achermann, R.; Cock, D.; Roscoe, T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

A survey of microarchitectural timing attacks and countermeasures on contemporary hardware

Journal of cryptographic engineering
2016-12-26 | Journal article
Contributors: Qian Ge; Yuval Yarom; David Cock; Gernot Heiser
Source: Self-asserted source
David Cock via Deutsche Nationalbibliothek (DNB)
grade
Preferred source (of 2)‎

From operational models to information theory; side channels in pGCL with Isabelle

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2014 | Book
EID:

2-s2.0-84904800091

Part of ISSN: 16113349 03029743
Contributors: Cock, D.
Source: Self-asserted source
David Cock via Scopus - Elsevier

The last mile: An empirical study of timing channels on seL4

Proceedings of the ACM Conference on Computer and Communications Security
2014 | Conference paper
EID:

2-s2.0-84910669114

Part of ISSN: 15437221
Contributors: Cock, D.; Ge, Q.; Murray, T.; Heiser, G.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Leakage in Trustworthy Systems

2014-08 | Dissertation or Thesis
Contributors: David Cock
Source: Self-asserted source
David Cock

Practical probability: Applying pGCL to lattice scheduling

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2013 | Book
EID:

2-s2.0-84882742694

Part of ISSN: 03029743 16113349
Contributors: Cock, D.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Verifying Probabilistic Correctness in Isabelle with pGCL

Source: Self-asserted source
David Cock via BASE - Bielefeld Academic Search Engine

Exploitation as an inference problem

Proceedings of the ACM Conference on Computer and Communications Security
2011 | Conference paper
EID:

2-s2.0-80955143555

Part of ISSN: 15437221
Contributors: Cock, D.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Lyrebird: assigning meanings to machines

2010 | Conference paper
Contributors: David Cock
Source: Self-asserted source
David Cock
grade
Preferred source (of 2)‎

SeL4: Formal verification of an operating-system kernel

Communications of the ACM
2010 | Journal article
EID:

2-s2.0-77953210383

Part of ISSN: 00010782 15577317
Contributors: Klein, G.; Andronick, J.; Elphinstone, K.; Heiser, G.; Cock, D.; Derrin, P.; Elkaduwe, D.; Engelhardt, K.; Kolanski, R.; Norrish, M. et al.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Mind the gap: A verification framework for low-level C

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2009 | Book
EID:

2-s2.0-70350303809

Part of ISSN: 03029743 16113349
Contributors: Winwood, S.; Klein, G.; Sewell, T.; Andronick, J.; Cock, D.; Norrish, M.
Source: Self-asserted source
David Cock via Scopus - Elsevier

SeL4: Formal verification of an OS kernel

SOSP'09 - Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles
2009 | Conference paper
EID:

2-s2.0-72249120603

Contributors: Klein, G.; Elphinstone, K.; Heiser, G.; Andronick, J.; Cock, D.; Derrin, P.; Elkaduwe, D.; Engelhardt, K.; Kolanski, R.; Norrish, M. et al.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Bitfields and tagged unions in C - Verification through automatic generation

CEUR Workshop Proceedings
2008 | Conference paper
EID:

2-s2.0-84885230563

Part of ISSN: 16130073
Contributors: Cock, D.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Secure microkernels, state monads and scalable refinement

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2008 | Book
EID:

2-s2.0-57049118010

Part of ISSN: 16113349 03029743
Contributors: Cock, D.; Klein, G.; Sewell, T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

Running the manual: An approach to high-assurance microkernel development

Haskell'06 - Proceedings of the ACM SIGPLAN 2006 Haskell Workshop
2006 | Conference paper
EID:

2-s2.0-33750992489

Contributors: Derrin, P.; Elphinstone, K.; Klein, G.; Cock, D.; Chakravarty, M.M.T.
Source: Self-asserted source
David Cock via Scopus - Elsevier

The Weyl Algebras

Source: Self-asserted source
David Cock
grade
Preferred source (of 2)‎