1THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT! 2 3,-------------------. 4| PREAMBLE | 5`-------------------' 6 7@preamble{ "\providecommand{\noopsort}[1]{} 8 \providecommand{\url}{\error{The bib files now require the 9 `url' package!}}" 10} 11 12,-------------------. 13| BIBTEX ENTRIES | 14`-------------------' 15 16 @inproceedings{Blackham_SCRH_11, 17 author = {Blackham, Bernard and Shi, Yao and Chattopadhyay, Sudipta and Roychoudhury, Abhik and Heiser, Gernot}, 18 month = nov, 19 pages = {339-348}, 20 year = {2011}, 21 title = {Timing Analysis of a Protected Operating System Kernel}, 22 booktitle = {IEEE Real-Time Systems Symposium}, 23 address = {Vienna, Austria} 24 } 25 26 @inproceedings{Blackham_SH_12, 27 author = {Blackham, Bernard and Shi, Yao and Heiser, Gernot}, 28 month = apr, 29 pages = {323-336}, 30 year = {2012}, 31 title = {Improving Interrupt Response Time in a Verifiable Protected Microkernel}, 32 booktitle = {EuroSys}, 33 address = {Bern, Switzerland} 34 } 35 36@inproceedings{Boyton_09, 37 address = {Aachen, Germany}, 38 author = {Andrew Boyton}, 39 booktitle = {Proceedings of the 4th Workshop on Systems Software 40 Verification}, 41 editor = {Gerwin Klein and Ralf Huuck and Bastian Schlich}, 42 month = oct, 43 pages = {25--44}, 44 publisher = {Elsevier}, 45 series = {Electronic Notes in Computer Science}, 46 title = {A Verified Shared Capability Model}, 47 volume = {254}, 48 year = {2009}, 49} 50 51@inproceedings{Cock_KS_08, 52 address = {Montreal, Canada}, 53 author = {David Cock and Gerwin Klein and Thomas Sewell}, 54 booktitle = {Proceedings of the 21st International Conference on 55 Theorem Proving in Higher Order Logics}, 56 editor = {Otmane Ait Mohamed and C\'{e}sar Mu{\~{n}}oz and 57 Sofi\`{e}ne Tahar}, 58 month = aug, 59 pages = {167--182}, 60 publisher = {Springer-Verlag}, 61 series = {Lecture Notes in Computer Science}, 62 title = {Secure Microkernels, State Monads and Scalable 63 Refinement}, 64 volume = {5170}, 65 year = {2008}, 66 doi = {10.1007/978-3-540-71067-7\_16}, 67} 68 69@inproceedings{Derrin_EKCC_06, 70 address = {Portland, OR, USA}, 71 author = {Philip Derrin and Kevin Elphinstone and Gerwin Klein and 72 David Cock and Manuel M. T. Chakravarty}, 73 booktitle = {Proceedings of the ACM SIGPLAN Haskell Workshop}, 74 month = sep, 75 title = {Running the Manual: An Approach to High-Assurance 76 Microkernel Development}, 77 year = {2006}, 78} 79 80@inproceedings{Elkaduwe_GE_08, 81 address = {Toronto, Canada}, 82 author = {Dhammika Elkaduwe and Gerwin Klein and 83 Kevin Elphinstone}, 84 booktitle = {Proceedings of Verified Software: Theories, Tools and 85 Experiments 2008}, 86 editor = {Jim Woodcock and Natarajan Shankar}, 87 month = oct, 88 pages = {99--114}, 89 publisher = {Springer-Verlag}, 90 series = {Lecture Notes in Computer Science}, 91 title = {Verified Protection Model of the {seL4} Microkernel}, 92 volume = {5295}, 93 year = {2008}, 94} 95 96@inproceedings{Klein_EHACDEEKNSTW_09, 97 address = {Big Sky, MT, USA}, 98 author = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and 99 June Andronick and David Cock and Philip Derrin and 100 Dhammika Elkaduwe and Kai Engelhardt and 101 Rafal Kolanski and Michael Norrish and Thomas Sewell and 102 Harvey Tuch and Simon Winwood}, 103 booktitle = {Proceedings of the 22nd ACM Symposium on Operating 104 Systems Principles}, 105 month = oct, 106 pages = {207--220}, 107 publisher = {ACM}, 108 title = {{seL4}: Formal Verification of an {OS} Kernel}, 109 year = {2009}, 110 doi = {10.1145/1629575.1629596}, 111} 112 113 @inproceedings{Murray_MBGBSLGK_13, 114 author = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Bourke, Timothy and 115 Seefried, Sean and Lewis, Corey and Gao, Xin and Klein, Gerwin}, 116 month = may, 117 pages = {415-429}, 118 year = {2013}, 119 title = {{seL4}: from General Purpose to a Proof of Information Flow Enforcement}, 120 booktitle = {IEEE Symposium on Security \& Privacy}, 121 address = {San Francisco, CA} 122 } 123 124 @inproceedings{Sewell_WGMAK_11, 125 author = {Sewell, Thomas and Winwood, Simon and Gammie, Peter and Murray, Toby and Andronick, June and Klein, 126 Gerwin}, 127 pages = {325-340}, 128 month = aug, 129 editor = {{Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk}}, 130 year = {2011}, 131 title = {{seL4} Enforces Integrity}, 132 booktitle = {Interactive Theorem Proving (ITP)}, 133 address = {Nijmegen, The Netherlands} 134 } 135 136@inproceedings{Tuch_KN_07, 137 address = {Nice, France}, 138 author = {Harvey Tuch and Gerwin Klein and Michael Norrish}, 139 booktitle = {Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium 140 on Principles of Programming Languages}, 141 editor = {Martin Hofmann and Matthias Felleisen}, 142 month = jan, 143 pages = {97--108}, 144 publisher = {ACM}, 145 title = {Types, Bytes, and Separation Logic}, 146 year = {2007}, 147} 148 149@inproceedings{Winwood_KSACN_09, 150 address = {Munich, Germany}, 151 author = {Simon Winwood and Gerwin Klein and Thomas Sewell and 152 June Andronick and David Cock and Michael Norrish}, 153 booktitle = {Proceedings of the 22nd International Conference on 154 Theorem Proving in Higher Order Logics}, 155 editor = {Stefan Berghofer and Tobias Nipkow and 156 Christian Urban and Makarius Wenzel}, 157 month = aug, 158 pages = {500--515}, 159 publisher = {Springer-Verlag}, 160 series = {Lecture Notes in Computer Science}, 161 title = {Mind the Gap: A Verification Framework for Low-Level 162 {C}}, 163 volume = {5674}, 164 year = {2009}, 165} 166 167@manual{extra:vtd, 168 author = {{Intel Corporation}}, 169 month = feb, 170 note = 171 {\url{http://download.intel.com/technology/computing/vptech/Intel(r)_VT_for_Direct_IO.pdf}}, 172 title = {Intel Virtualization Technology for Directed I/O --- 173 Architecture Specification}, 174 year = {2011}, 175} 176 177@book{Shanley:PCISA, 178 author = {Tom Shanley and Don Anderson}, 179 publisher = {Mindshare, Inc.}, 180 title = {PCI System Architecture}, 181 year = {1999}, 182} 183 184@mastersthesis{Palande:M, 185 address = {Amsterdam}, 186 author = {Ameya Palande}, 187 month = jan, 188 school = {Vrije Universiteit}, 189 type = {Masters Thesis}, 190 title = {Capability-based Secure {DMA} in {seL4}}, 191 year = {2009}, 192} 193 194@inproceedings{Baumann_BDHIPRSS_09, 195 address = {Big Sky, MT, USA}, 196 author = {Andrew Baumann and Paul Barham and 197 Pierre-Evariste Dagand and Tim Harris and 198 Rebecca Isaacs and Simon Peter and Timothy Roscoe and 199 Adrian Sch{\"u}pbach and Akhilesh Singhania}, 200 booktitle = {Proceedings of the 22nd ACM Symposium on Operating 201 Systems Principles}, 202 month = oct, 203 publisher = {ACM}, 204 title = {The multikernel: A new {OS} architecture for scalable 205 multicore systems}, 206 year = {2009}, 207} 208 209@inproceedings{vonTessin_10, 210 address = {Edinburgh, UK}, 211 author = {von Tessin, Michael}, 212 booktitle = {Proceedings of the 6th International Verification 213 Workshop}, 214 editor = {Markus Aderhold and Serge Autexier and Heiko Mantel}, 215 month = jul, 216 pages = {110--125}, 217 publisher = {EasyChair}, 218 series = {EasyChair Proceedings in Computing}, 219 title = {Towards High-Assurance Multiprocessor Virtualisation}, 220 volume = {3}, 221 year = {2010}, 222 issn = {2040-557X}, 223} 224 225@inproceedings{vonTessin_12, 226 address = {Bern, Switzerland}, 227 author = {von Tessin, Michael}, 228 booktitle = {Proceedings of the 2nd Workshop on Systems for Future 229 Multi-core Architectures}, 230 month = apr, 231 title = {The Clustered Multikernel: An Approach to Formal 232 Verification of Multiprocessor {OS} Kernels}, 233 year = {2012}, 234} 235 236