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
20132009
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
2342018
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
772014
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
492009
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
102017
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
72018
pGCL for Isabelle
D Cock
Archive of Formal Proofs, 2014
62014
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
52017
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
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 Weyl algebras
D Cock
School of Mathematics, The University of New South Wales, 2004
22004
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
12020
The system can't perform the operation now. Try again later.
Articles 1–20