forked from Imagelibrary/seL4
ea8e57275c
- resolve mix of service mechanism, abstraction - update verification explanation + references - remove reference to ARM11 which is slated to be discontinued Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
275 lines
10 KiB
BibTeX
275 lines
10 KiB
BibTeX
THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT!
|
|
|
|
,-------------------.
|
|
| PREAMBLE |
|
|
`-------------------'
|
|
|
|
@preamble{ "\providecommand{\noopsort}[1]{}
|
|
\providecommand{\url}{\error{The bib files now require the
|
|
`url' package!}}"
|
|
}
|
|
|
|
,-------------------.
|
|
| BIBTEX ENTRIES |
|
|
`-------------------'
|
|
|
|
@inproceedings{Blackham_SCRH_11,
|
|
author = {Blackham, Bernard and Shi, Yao and Chattopadhyay, Sudipta and Roychoudhury, Abhik and Heiser, Gernot},
|
|
month = nov,
|
|
pages = {339-348},
|
|
year = {2011},
|
|
title = {Timing Analysis of a Protected Operating System Kernel},
|
|
booktitle = {IEEE Real-Time Systems Symposium},
|
|
address = {Vienna, Austria}
|
|
}
|
|
|
|
@inproceedings{Blackham_SH_12,
|
|
author = {Blackham, Bernard and Shi, Yao and Heiser, Gernot},
|
|
month = apr,
|
|
pages = {323-336},
|
|
year = {2012},
|
|
title = {Improving Interrupt Response Time in a Verifiable Protected Microkernel},
|
|
booktitle = {EuroSys},
|
|
address = {Bern, Switzerland}
|
|
}
|
|
|
|
@inproceedings{Boyton_09,
|
|
address = {Aachen, Germany},
|
|
author = {Andrew Boyton},
|
|
booktitle = {Proceedings of the 4th Workshop on Systems Software
|
|
Verification},
|
|
editor = {Gerwin Klein and Ralf Huuck and Bastian Schlich},
|
|
month = oct,
|
|
pages = {25--44},
|
|
publisher = {Elsevier},
|
|
series = {Electronic Notes in Computer Science},
|
|
title = {A Verified Shared Capability Model},
|
|
volume = {254},
|
|
year = {2009},
|
|
}
|
|
|
|
@inproceedings{Cock_KS_08,
|
|
address = {Montreal, Canada},
|
|
author = {David Cock and Gerwin Klein and Thomas Sewell},
|
|
booktitle = {Proceedings of the 21st International Conference on
|
|
Theorem Proving in Higher Order Logics},
|
|
editor = {Otmane Ait Mohamed and C\'{e}sar Mu{\~{n}}oz and
|
|
Sofi\`{e}ne Tahar},
|
|
month = aug,
|
|
pages = {167--182},
|
|
publisher = {Springer-Verlag},
|
|
series = {Lecture Notes in Computer Science},
|
|
title = {Secure Microkernels, State Monads and Scalable
|
|
Refinement},
|
|
volume = {5170},
|
|
year = {2008},
|
|
doi = {10.1007/978-3-540-71067-7\_16},
|
|
}
|
|
|
|
@inproceedings{Derrin_EKCC_06,
|
|
address = {Portland, OR, USA},
|
|
author = {Philip Derrin and Kevin Elphinstone and Gerwin Klein and
|
|
David Cock and Manuel M. T. Chakravarty},
|
|
booktitle = {Proceedings of the ACM SIGPLAN Haskell Workshop},
|
|
month = sep,
|
|
title = {Running the Manual: An Approach to High-Assurance
|
|
Microkernel Development},
|
|
year = {2006},
|
|
}
|
|
|
|
@inproceedings{Elkaduwe_KE_08,
|
|
address = {Toronto, Canada},
|
|
author = {Dhammika Elkaduwe and Gerwin Klein and
|
|
Kevin Elphinstone},
|
|
booktitle = {Proceedings of Verified Software: Theories, Tools and
|
|
Experiments 2008},
|
|
editor = {Jim Woodcock and Natarajan Shankar},
|
|
month = oct,
|
|
pages = {99--114},
|
|
publisher = {Springer-Verlag},
|
|
series = {Lecture Notes in Computer Science},
|
|
title = {Verified Protection Model of the {seL4} Microkernel},
|
|
volume = {5295},
|
|
year = {2008},
|
|
}
|
|
|
|
@inproceedings{Klein_EHACDEEKNSTW_09,
|
|
address = {Big Sky, MT, USA},
|
|
author = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and
|
|
June Andronick and David Cock and Philip Derrin and
|
|
Dhammika Elkaduwe and Kai Engelhardt and
|
|
Rafal Kolanski and Michael Norrish and Thomas Sewell and
|
|
Harvey Tuch and Simon Winwood},
|
|
booktitle = {Proceedings of the 22nd ACM Symposium on Operating
|
|
Systems Principles},
|
|
month = oct,
|
|
pages = {207--220},
|
|
publisher = {ACM},
|
|
title = {{seL4}: Formal Verification of an {OS} Kernel},
|
|
year = {2009},
|
|
doi = {10.1145/1629575.1629596},
|
|
}
|
|
|
|
@inproceedings{Murray_MBGBSLGK_13,
|
|
author = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Bourke, Timothy and
|
|
Seefried, Sean and Lewis, Corey and Gao, Xin and Klein, Gerwin},
|
|
month = may,
|
|
pages = {415-429},
|
|
year = {2013},
|
|
title = {{seL4}: from General Purpose to a Proof of Information Flow Enforcement},
|
|
booktitle = {IEEE Symposium on Security \& Privacy},
|
|
address = {San Francisco, CA}
|
|
}
|
|
|
|
@inproceedings{Sewell_WGMAK_11,
|
|
author = {Sewell, Thomas and Winwood, Simon and Gammie, Peter and Murray, Toby and Andronick, June and Klein,
|
|
Gerwin},
|
|
pages = {325-340},
|
|
month = aug,
|
|
editor = {{Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk}},
|
|
year = {2011},
|
|
title = {{seL4} Enforces Integrity},
|
|
booktitle = {Interactive Theorem Proving (ITP)},
|
|
address = {Nijmegen, The Netherlands}
|
|
}
|
|
|
|
@inproceedings{Tuch_KN_07,
|
|
address = {Nice, France},
|
|
author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
|
|
booktitle = {Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium
|
|
on Principles of Programming Languages},
|
|
editor = {Martin Hofmann and Matthias Felleisen},
|
|
month = jan,
|
|
pages = {97--108},
|
|
publisher = {ACM},
|
|
title = {Types, Bytes, and Separation Logic},
|
|
year = {2007},
|
|
}
|
|
|
|
@inproceedings{Winwood_KSACN_09,
|
|
address = {Munich, Germany},
|
|
author = {Simon Winwood and Gerwin Klein and Thomas Sewell and
|
|
June Andronick and David Cock and Michael Norrish},
|
|
booktitle = {Proceedings of the 22nd International Conference on
|
|
Theorem Proving in Higher Order Logics},
|
|
editor = {Stefan Berghofer and Tobias Nipkow and
|
|
Christian Urban and Makarius Wenzel},
|
|
month = aug,
|
|
pages = {500--515},
|
|
publisher = {Springer-Verlag},
|
|
series = {Lecture Notes in Computer Science},
|
|
title = {Mind the Gap: A Verification Framework for Low-Level
|
|
{C}},
|
|
volume = {5674},
|
|
year = {2009},
|
|
}
|
|
|
|
@manual{extra:vtd,
|
|
author = {{Intel Corporation}},
|
|
month = feb,
|
|
note =
|
|
{\url{http://download.intel.com/technology/computing/vptech/Intel(r)_VT_for_Direct_IO.pdf}},
|
|
title = {Intel Virtualization Technology for Directed I/O ---
|
|
Architecture Specification},
|
|
year = {2011},
|
|
}
|
|
|
|
@book{Shanley:PCISA,
|
|
author = {Tom Shanley and Don Anderson},
|
|
publisher = {Mindshare, Inc.},
|
|
title = {PCI System Architecture},
|
|
year = {1999},
|
|
}
|
|
|
|
@mastersthesis{Palande:M,
|
|
address = {Amsterdam},
|
|
author = {Ameya Palande},
|
|
month = jan,
|
|
school = {Vrije Universiteit},
|
|
type = {Masters Thesis},
|
|
title = {Capability-based Secure {DMA} in {seL4}},
|
|
year = {2009},
|
|
}
|
|
|
|
@inproceedings{Baumann_BDHIPRSS_09,
|
|
address = {Big Sky, MT, USA},
|
|
author = {Andrew Baumann and Paul Barham and
|
|
Pierre-Evariste Dagand and Tim Harris and
|
|
Rebecca Isaacs and Simon Peter and Timothy Roscoe and
|
|
Adrian Sch{\"u}pbach and Akhilesh Singhania},
|
|
booktitle = {Proceedings of the 22nd ACM Symposium on Operating
|
|
Systems Principles},
|
|
month = oct,
|
|
publisher = {ACM},
|
|
title = {The multikernel: A new {OS} architecture for scalable
|
|
multicore systems},
|
|
year = {2009},
|
|
}
|
|
|
|
@inproceedings{vonTessin_10,
|
|
address = {Edinburgh, UK},
|
|
author = {von Tessin, Michael},
|
|
booktitle = {Proceedings of the 6th International Verification
|
|
Workshop},
|
|
editor = {Markus Aderhold and Serge Autexier and Heiko Mantel},
|
|
month = jul,
|
|
pages = {110--125},
|
|
publisher = {EasyChair},
|
|
series = {EasyChair Proceedings in Computing},
|
|
title = {Towards High-Assurance Multiprocessor Virtualisation},
|
|
volume = {3},
|
|
year = {2010},
|
|
issn = {2040-557X},
|
|
}
|
|
|
|
@inproceedings{vonTessin_12,
|
|
address = {Bern, Switzerland},
|
|
author = {von Tessin, Michael},
|
|
booktitle = {Proceedings of the 2nd Workshop on Systems for Future
|
|
Multi-core Architectures},
|
|
month = apr,
|
|
title = {The Clustered Multikernel: An Approach to Formal
|
|
Verification of Multiprocessor {OS} Kernels},
|
|
year = {2012},
|
|
}
|
|
|
|
@article{Klein_AEMSKH_14,
|
|
author = {Klein, Gerwin and Andronick, June and
|
|
Elphinstone, Kevin and Murray, Toby and
|
|
Sewell, Thomas and Kolanski, Rafal and
|
|
Heiser, Gernot},
|
|
journal = {ACM Transactions on Computer Systems},
|
|
month = feb,
|
|
number = {1},
|
|
pages = {2:1-2:70},
|
|
title = {Comprehensive Formal Verification of an {OS}
|
|
Microkernel},
|
|
volume = {32},
|
|
year = {2014},
|
|
doi = {10.1145/2560537},
|
|
}
|
|
|
|
@misc{seL4_spec,
|
|
author = {{seL4 Authors}},
|
|
month = sep,
|
|
title = {Abstract formal specification of the {seL4} {API}},
|
|
year = {2021},
|
|
url = {https://github.com/seL4/l4v/tree/master/spec/abstract},
|
|
}
|
|
|
|
@misc{whitepaper,
|
|
author = {Gernot Heiser},
|
|
month = jun,
|
|
title = {The {seL4} Microkernel, An Introduction},
|
|
year = {2020},
|
|
url = {https://sel4.systems/About/seL4-whitepaper.pdf},
|
|
}
|
|
|
|
@misc{doc_site_proofs,
|
|
author = {{seL4 Authors}},
|
|
month = sep,
|
|
title = {The {seL4} documentation site},
|
|
year = {2021},
|
|
url = {https://docs.sel4.systems/projects/sel4/verified-configurations.html},
|
|
}
|