David Cock
David Cock
Graduate Researcher, NICTA and University of New South Wales
Verified email at cse.unsw.edu.au - Homepage
Title
Cited by
Cited by
Year
seL4: Formal verification of an OS kernel
G Klein, K Elphinstone, G Heiser, J Andronick, D Cock, P Derrin, ...
Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles …, 2009
20622009
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware
Q Ge, Y Yarom, D Cock, G Heiser
Journal of Cryptographic Engineering 8 (1), 1-27, 2018
2532018
Secure microkernels, state monads and scalable refinement
D Cock, G Klein, T Sewell
International Conference on Theorem Proving in Higher Order Logics, 167-182, 2008
892008
The last mile: An empirical study of timing channels on seL4
D Cock, Q Ge, T Murray, G Heiser
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications …, 2014
812014
Running the manual: An approach to high-assurance microkernel development
P Derrin, K Elphinstone, G Klein, D Cock, MMT Chakravarty
Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, 60-71, 2006
542006
Mind the gap
S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish
International Conference on Theorem Proving in Higher Order Logics, 500-515, 2009
502009
Verifying probabilistic correctness in Isabelle with pGCL
D Cock
arXiv preprint arXiv:1211.6197, 2012
222012
Bitfields and Tagged Unions in C: Verification through Automatic Generation.
D Cock
VERIFY 8, 44-55, 2008
142008
Practical probability: Applying pGCL to lattice scheduling
D Cock
International Conference on Interactive Theorem Proving, 311-327, 2013
122013
Formalizing memory accesses and interrupts
R Achermann, L Humbel, D Cock, T Roscoe
arXiv preprint arXiv:1703.06571, 2017
112017
Physical addressing on real hardware in Isabelle/HOL
R Achermann, L Humbel, D Cock, T Roscoe
International Conference on Interactive Theorem Proving, 1-19, 2018
82018
Towards correct-by-construction interrupt routing on real hardware
L Humbel, R Achermann, D Cock, T Roscoe
Proceedings of the 9th Workshop on Programming Languages and Operating …, 2017
62017
pGCL for Isabelle
D Cock
Archive of Formal Proofs, 2014
62014
Leakage in Trustworthy Systems.
D Cock
University of New South Wales, Sydney, Australia, 2014
42014
Lyrebird-Assigning Meanings to Machines.
D Cock
SSV, 2010
32010
The Weyl algebras
D Cock
School of Mathematics, The University of New South Wales, 2004
32004
Tackling Hardware/Software co-design from a database perspective.
G Alonso, T Roscoe, D Cock, M Ewaida, K Kara, D Korolija, D Sidler, ...
CIDR, 2020
22020
A Least-Privilege Memory Protection Model for Modern Hardware
R Achermann, N Hossle, L Humbel, D Schwyn, D Cock, T Roscoe
arXiv preprint arXiv:1908.08707, 2019
22019
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle
D Cock
International Conference on Interactive Theorem Proving, 177-192, 2014
22014
Exploitation as an inference problem
DA Cock
Proceedings of the 4th ACM workshop on Security and artificial intelligence …, 2011
22011
The system can't perform the operation now. Try again later.
Articles 1–20