@misc{Verbeek2013,
  author = {Freek Verbeek and Julien Schmaltz and Sergey Tverdyshev and Holger Blasum and Oto Havle},
  title = {A New Theory of Intransitive Noninterference for Separation Kernels with Control (manuscript)},
  year = {2013},
  class = {},
  filename = {post14_submission_37.pdf},
  timestamp = {1381923125},
}

@inproceedings{Liedtke1995,
  author = {Jochen Liedtke},
  title = {On $\mu$-Kernel Construction},
  booktitle = {Proceedings of the 15th ACM Symposium on Operating Systems Principles},
  year = {1995},
  isbn = {0-89791-715-4},
  pages = {237--250},
  location = {Copper Mountain, Colorado, United States},
  doi = {http://doi.acm.org/10.1145/224056.224075},
  publisher = {ACM Press},
}

@TECHREPORT{Rushby1992noninterference,
    AUTHOR = {John Rushby},
    TITLE = {Noninterference, Transitivity, and Channel-Control Security Policies},
    YEAR = {1992},
    MONTH = {dec},
    URL = {http://www.csl.sri.com/papers/csl-92-2/},
    BOOKTITLE = {Technical Report {CSL-92-02}}
}

@TECHREPORT{rushby92,
    AUTHOR = {John Rushby},
    TITLE = {Noninterference, Transitivity, and Channel-Control Security Policies},
    YEAR = {1992},
    MONTH = {dec},
    URL = {http://www.csl.sri.com/papers/csl-92-2/},
    BOOKTITLE = {Technical Report {CSL-92-02}}
}


@inproceedings{kaiser07,
  author = {R. Kaiser and S. Wagner},
  title = {{E}volution of the {P}ike{OS} microkernel},
  booktitle = {In: FirstInternational Workshop on Microkernels for Embedded Systems},
  year = {2007}
}


@article{rushby81,
  author = {John Rushby},
  title = {Design and verification of secure systems},
  journal = {ACM SIGOPS Operating Systems Review},
  volume = {15}, 
  publisher = {ACM},
  year = {1981},
  pages = {12--21}
}

@TECHREPORT{brygier09,
    AUTHOR = {J. Brygier and R. Fuchsen and H. Blasum},
    TITLE = {PikeOS: Safe and secure virtualization in a separation microkernel},
    YEAR = {2009},
    BOOKTITLE = {Technical Report SYSGO (2009)}
}


@inproceedings{nipkow12,
   author = {Tobias Nipkow and Larry C. Paulson and Markus Wenzel}, 
   title = {Isabelle/HOL: a proof assistant for higher- order logic},
   year = {2012},
   editor= {Springer-Verlag}
}

@inproceedings{Murray_MBGK_12,
    publisher        = {Springer},
    isbn             = {978-3-642-35307-9},
    author           = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Klein, Gerwin},
    month            = {dec},
    editor           = {{Chris Hawblitzel and Dale Miller}},
    year             = {2012},
    title            = {Noninterference for Operating System Kernels},
    booktitle        = {The Second International Conference on Certified Programs and Proofs},
    pages            = {126-142},
    address          = {Kyoto}
}




@Article{SKIPaper6,
  author = 	 { A. Sabelfeld and A. C. Myers},
  title = 	 {Language-based information-flow security,},
  journal = 	 {Selected Areas in Communications, IEEE Journal on,},
  year = 	 2003,
  volume = 	 21,
  number = 	 1,
  pages = 	 {5--19}
}

@InProceedings{SKIPaper7,
  author = 	 {D. Greve and M. Wilding and W. M. Vanfleet},
  title = 	 {A separation kernel formal security policy},
  booktitle = {Fourth International Workshop on the ACL2 Prover and Its  Applications (ACL2-2003)},
  year = 	 {2003}
}



@inproceedings{Heitmeyer:2006:FSV:1180405.1180448,
 author = {Heitmeyer, Constance L. and Archer, Myla and Leonard, Elizabeth I. and McLean, John},
 title = {Formal Specification and Verification of Data Separation in a Separation Kernel for an Embedded System},
 booktitle = {Proceedings of the 13th ACM Conference on Computer and Communications Security},
 series = {CCS '06},
 year = {2006},
 isbn = {1-59593-518-5},
 location = {Alexandria, Virginia, USA},
 pages = {346--355},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1180405.1180448},
 doi = {10.1145/1180405.1180448},
 acmid = {1180448},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {code verification, formal model, formal specification, separation kernel, theorem proving},
} 

@inproceedings{Martin:2000:FCM:786768.786973,
 author = {Martin, W. and White, P. and Taylor, F. S. and Goldberg, A.},
 title = {Formal Construction of the Mathematically Analyzed Separation Kernel},
 booktitle = {Proceedings of the 15th IEEE International Conference on Automated Software Engineering},
 series = {ASE '00},
 year = {2000},
 isbn = {0-7695-0710-7},
 pages = {133--},
 url = {http://dl.acm.org/citation.cfm?id=786768.786973},
 acmid = {786973},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
} 

@inproceedings{Shapiro:2000:VEC:882494.884422,
 author = {Shapiro, Jonathan S. and Weber, Sam},
 title = {Verifying the EROS Confinement Mechanism},
 booktitle = {Proceedings of the 2000 IEEE Symposium on Security and Privacy},
 series = {SP '00},
 year = {2000},
 isbn = {0-7695-0665-8},
 pages = {166--},
 url = {http://dl.acm.org/citation.cfm?id=882494.884422},
 acmid = {884422},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {operating systems, capability systems, proof of correctness, confinement, verification, formal specification},
} 

@article{SKIPaper11,
 year={2009},
 issn={0256-2499},
 journal={Sadhana},
 volume={34},
 number={1},
 doi={10.1007/s12046-009-0002-4},
 title={Operating system verification---An overview},
 url={https://doi.org/10.1007/s12046-009-0002-4},
 publisher={Springer-Verlag},
 keywords={Formal software verification; operating systems; theorem proving},
 author={Klein, Gerwin},
 pages={27-69},
 language={English}
}

@article{SKIPaper12,
title = "A comparison of semantic models for noninterference ",
journal = "Theoretical Computer Science ",
volume = "411",
number = "47",
pages = "4123 - 4147",
year = "2010",
note = "",
issn = "0304-3975",
doi = "https://doi.org/10.1016/j.tcs.2010.08.013",
url = "http://www.sciencedirect.com/science/article/pii/S0304397510004482",
author = "Ron van der Meyden and Chenyi Zhang",
keywords = "Computer security",
keywords = "Noninterference",
keywords = "Information flow",
keywords = "Comparison ",
abstract = "The literature on definitions of security based on causality-like notions such as noninterference has used several distinct semantic models for systems. Early work was based on state machine and trace-set definitions; more recent work has dealt with definitions of security in two distinct process algebraic settings. Comparisons between the definitions has been carried out mainly within semantic frameworks. This paper studies the relationship between semantic frameworks, by defining mappings between a number of semantic models and studying the relationship between notions of noninterference under these mappings. "
}

@inproceedings{SKIPaper13,
  author    = {Joseph A. Goguen and
               Jos{\'e} Meseguer},
  title     = {Security policies and security models},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {1984},
  pages     = {11-20}
}

@inproceedings{SKIPaper14,
  author    = {Joseph A. Goguen and
               Jos{\'e} Meseguer},
  title     = {Unwinding and Inference Control},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {1984},
  pages     = {75-87}
}

@inproceedings{SKIPaper25,
  author    = {Rebekah Leslie},
  title     = {Dynamic intransitive noninterference},
  booktitle = {IEEE International Symposium on Secure Software Engineering},
  year      = {2006},
  pages     = {75-87}
}

@inproceedings{Klein:2009:SFV:1629575.1629596,
 author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, 
          June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, 
          Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
 title = {seL4: Formal Verification of an OS Kernel},
 booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
 series = {SOSP '09},
 year = {2009},
 isbn = {978-1-60558-752-3},
 location = {Big Sky, Montana, USA},
 pages = {207--220},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/1629575.1629596},
 doi = {10.1145/1629575.1629596},
 acmid = {1629596},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {isabelle/hol, l4, microkernel, sel4},
} 

@inproceedings{SKIPaper30,
  author = "Toby Murray and Daniel Matichuk and Matthew Brassil and Peter Gammie and Timothy Bourke and Sean Seefried and Corey Lewis and Xin Gao and Gerwin Klein",
  isbn = "10.1109/SP.2013.35",
  month = "May",
  booktitle = "IEEE Symposium on Security and Privacy",
  year = "2013",
  pages = "415--429",
  title = "seL4: from General Purpose to a Proof of Information Flow Enforcement",
  abstract = "In contrast to testing, mathematical reasoning and formal verification
can show the absence of whole classes of security vulnerabilities. We
present the, to our knowledge, first complete, formal, machine-checked
verification of information flow security for the implementation of a
general-purpose microkernel; namely seL4. Unlike previous proofs of
information flow security for operating system kernels, ours applies
to the actual 8,830 lines of C code that implement seL4, and
so rules out the possibility of invalidation by implementation errors
in this code. We assume correctness of compiler, assembly code,
hardware, and boot code. We prove everything else. This proof is
strong evidence of seL4's utility as a separation kernel, and
describes precisely how the general purpose kernel should be
configured to enforce isolation and mandatory information flow
control. We describe the information flow security statement we proved
(a variant of intransitive noninterference), including the assumptions
on which it rests, as well as the modifications that had to be made to
seL4 to ensure it was enforced. We discuss the practical limitations
and implications of this result, including covert channels not covered
by the formal proof.
",
  address = "San Francisco, CA"
}

@incollection{SKIPaper31,
year={2013},
isbn={978-3-642-40312-5},
booktitle={Mathematical Foundations of Computer Science 2013},
volume={8087},
series={Lecture Notes in Computer Science},
editor={Chatterjee, Krishnendu and Sgall, Jirí},
doi={10.1007/978-3-642-40313-2_31},
title={Noninterference with Local Policies},
url={https://doi.org/10.1007/978-3-642-40313-2_31},
publisher={Springer Berlin Heidelberg},
author={Eggert, Sebastian and Schnoor, Henning and Wilke, Thomas},
pages={337-348},
language={English}
}

@article{SKIPaper32,
	title = {Extending the Non-Interference Version of MLS for SAT},
	journal = {IEEE Transactions on Software Engineering},
	volume = {13},
	year = {1987},
	month = {1987},
	pages = {141-150},
	author = {J.Thomas Haigh and W.D. Young}
}


@inproceedings{Elphinstone:2007:TPV:1361397.1361417,
 author = {Elphinstone, Kevin and Klein, Gerwin and Derrin, Philip and Roscoe, Timothy and Heiser, Gernot},
 title = {Towards a Practical, Verified Kernel},
 booktitle = {Proceedings of the 11th USENIX Workshop on Hot Topics in Operating Systems},
 series = {HOTOS'07},
 year = {2007},
 location = {San Diego, CA},
 pages = {20:1--20:6},
 articleno = {20},
 numpages = {6},
 url = {http://dl.acm.org/citation.cfm?id=1361397.1361417},
 acmid = {1361417},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 

@article{DBLP:journals/jar/AlkassarHLSST09,
  author    = {Eyad Alkassar and
               Mark A. Hillebrand and
               Dirk Leinenbach and
               Norbert Schirmer and
               Artem Starostin and
               Alexandra Tsyban},
  title     = {Balancing the Load},
  journal   = {J. Autom. Reasoning},
  volume    = {42},
  number    = {2-4},
  year      = {2009},
  pages     = {389-454},
  ee        = {https://doi.org/10.1007/s10817-009-9123-z},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jar/DaumDW09,
  author    = {Matthias Daum and
               Jan D{\"o}rrenb{\"a}cher and
               Burkhart Wolff},
  title     = {Proving Fairness and Implementation Correctness of a Microkernel
               Scheduler},
  journal   = {J. Autom. Reasoning},
  volume    = {42},
  number    = {2-4},
  year      = {2009},
  pages     = {349-388},
  ee        = {https://doi.org/10.1007/s10817-009-9119-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{SKIPaper15,
year={2001},
isbn={978-3-540-41791-0},
booktitle={FME 2001: Formal Methods for Increasing Software Productivity},
volume={2021},
series={Lecture Notes in Computer Science},
editor={Oliveira, JoséNuno and Zave, Pamela},
doi={10.1007/3-540-45251-6_9},
title={Information Flow Control and Applications --- Bridging a Gap ---},
url={https://doi.org/10.1007/3-540-45251-6_9},
publisher={Springer Berlin Heidelberg},
author={Mantel, Heiko},
pages={153-172},
language={English}
}

@incollection{SKIPaper16,
year={2000},
isbn={978-3-540-41031-7},
booktitle={Computer Security - ESORICS 2000},
volume={1895},
series={Lecture Notes in Computer Science},
editor={Cuppens, Frédéric and Deswarte, Yves and Gollmann, Dieter and Waidner, Michael},
doi={10.1007/10722599_2},
title={Verification of a Formal Security Model for Multiapplicative Smart Cards},
url={https://doi.org/10.1007/10722599_2},
publisher={Springer Berlin Heidelberg},
author={Schellhorn, Gerhard and Reif, Wolfgang and Schairer, Axel and Karger, Paul and Austel, Vernon and Toll, David},
pages={17-36},
language={English}
}

@INPROCEEDINGS{SKIPaper18,
    author = {A. W. Roscoe},
    title = {What is intransitive noninterference},
    booktitle = {In Proc. of the 12th IEEE Computer Security Foundations Workshop},
    year = {1999},
    pages = {228--238}
}


@inproceedings{VanDerMeyden:2007:IIN:2393847.2393869,
 author = {Van Der Meyden, Ron},
 title = {What, Indeed, is Intransitive Noninterference?},
 booktitle = {Proceedings of the 12th European Conference on Research in Computer Security},
 series = {ESORICS'07},
 year = {2007},
 isbn = {3-540-74834-2, 978-3-540-74834-2},
 location = {Dresden, Germany},
 pages = {235--250},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=2393847.2393869},
 acmid = {2393869},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}


@inproceedings{SKIPaper20,
  author    = {Sebastian Eggert and
               Ron van der Meyden and
               Henning Schnoor and
               Thomas Wilke},
  title     = {The Complexity of Intransitive Noninterference},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {2011},
  pages     = {196-211},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/SP.2011.30},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{SKIPaper21,
year={2010},
isbn={978-1-4419-1538-2},
booktitle={Design and Verification of Microprocessor Systems for High-Assurance Applications},
editor={Hardin, David S.},
doi={10.1007/978-1-4419-1539-9_13},
title={Model Checking Information Flow},
url={https://doi.org/10.1007/978-1-4419-1539-9_13},
publisher={Springer US},
author={Whalen, MichaelW. and Greve, DavidA. and Wagner, LucasG.},
pages={381-428},
language={English}
}
