%15
@article{15,
	author = {<NAME> <NAME> and <NAME>},
	title = {End-to-End Verification of Information-Flow Security for C and Assembly Programs},
	year = {2016},
	issue_date = {June 2016},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {51},
	number = {6},
	issn = {0362-1340},
	url = {https://doi.org/10.1145/2980983.2908100},
	doi = {10.1145/2980983.2908100},
	journal = {SIGPLAN Not.},
	month = jun,
	pages = {648–664},
	numpages = {17},
	keywords = {Security-Preserving Simulation, Information Flow Control, Security Policy Specification, Certified OS Kernels, Program Verification}
}

%17
@inproceedings{17,
	title	= {Komodo: Using Verification to Disentangle Secure-enclave Hardware from Software},
	author	= {<NAME> and <NAME> and <NAME> and <NAME>},
	year	= {2017},
	URL	= {https://people.ece.cornell.edu/af433/pdf/ferraiuolo-sosp-17.pdf},
	booktitle	= {Proceedings of the 26th Symposium on Operating Systems Principles},
	pages	= {287--305}
}

%19
@INPROCEEDINGS{19,
	author={<NAME>. and <NAME>.},
	booktitle={1982 IEEE Symposium on Security and Privacy}, 
	title={Security Policies and Security Models}, 
	year={1982},
	volume={},
	number={},
	pages={11-11},
	doi={10.1109/SP.1982.10014}}

%20
@inproceedings {20,
	author = {<NAME> and <NAME> and <NAME> and <NAME> and <NAME> and <NAME> and <NAME>},
	title = {Ironclad Apps: End-to-End Security via Automated Full-System Verification},
	booktitle = {11th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 14)},
	year = {2014},
	isbn = { 978-1-931971-16-4},
	address = {Broomfield, CO},
	pages = {165--181},
	url = {https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel},
	publisher = {{USENIX} Association},
	month = oct,
}

%23
@article{23,
	author = {<NAME> <NAME>, <NAME> <NAME> Sewell, <NAME> Kolanski, <NAME> Heiser, Gernot},
	title = {Comprehensive Formal Verification of an OS Microkernel},
	year = {2014},
	issue_date = {February 2014},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {32},
	number = {1},
	issn = {0734-2071},
	url = {https://doi.org/10.1145/2560537},
	doi = {10.1145/2560537},
	journal = {ACM Trans. Comput. Syst.},
	month = feb,
	articleno = {2},
	numpages = {70},
	keywords = {operating systems, seL4, L4, microkernel, Isabelle/HOL}
}


%25
@ARTICLE{25,
	author = {<NAME>},
	title = {Proving Noninterference and Functional Correctness Using Traces},
	journal = {Journal of Computer Security},
	year = {1992},
	volume = {1},
	pages = {37--58}
}

%26
@INPROCEEDINGS{26,
	author={<NAME> and <NAME> and Brassil, Matthew and <NAME> and <NAME> and <NAME> and <NAME> and <NAME> and <NAME>},
	booktitle={2013 IEEE Symposium on Security and Privacy}, 
	title={seL4: From General Purpose to a Proof of Information Flow Enforcement}, 
	year={2013},
	volume={},
	number={},
	pages={415-429},
	doi={10.1109/SP.2013.35}}

%29
@InProceedings{29,
	author="Popescu, Andrei
	and H{\"o}lzl, Johannes
	and Nipkow, Tobias",
	editor="Hawblitzel, Chris
	and <NAME>",
	title="Proving Concurrent Noninterference",
	booktitle="Certified Programs and Proofs",
	year="2012",
	publisher="Springer Berlin Heidelberg",
	address="Berlin, Heidelberg",
	pages="109--125"
}

%30
@INPROCEEDINGS{30,
	author={<NAME>.},
	booktitle={Proceedings 1995 IEEE Symposium on Security and Privacy}, 
	title={CSP and determinism in security modelling}, 
	year={1995},
	volume={},
	number={},
	pages={114-127},
	doi={10.1109/SECPRI.1995.398927}}

%32
@InProceedings{32,
	author="<NAME>.",
	editor="Dezani-Ciancaglini, Mariangiola
	and Montanari, Ugo",
	title="Proof of separability A verification technique for a class of security kernels",
	booktitle="International Symposium on Programming",
	year="1982",
	publisher="Springer Berlin Heidelberg",
	address="Berlin, Heidelberg",
	pages="352--367",
	isbn="978-3-540-39184-5"
}

%SeLoc
@article{seloc,
	title={Compositional non-interference for fine-grained concurrent programs},
	author={<NAME> Krebbers, <NAME> <NAME>},
	journal={arXiv preprint arXiv:1910.00905},
	year={2019}
}

%IRIS
@article{iris, 
	title={Iris from the ground up: A modular foundation for higher-order concurrent separation logic}, 
	volume={28}, 
	DOI={10.1017/S0956796818000151}, 
	journal={Journal of Functional Programming}, 
	publisher={Cambridge University Press}, 
	author={<NAME> and <NAME> and <NAME> and BIZJAK, ALEŠ and BIRKEDAL, LARS and DREYER, DEREK}, year={2018}, pages={e20}}

%Sun
@INPROCEEDINGS{sun,
	author={<NAME> and <NAME> and <NAME>},
	booktitle={2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC)}, 
	title={Enforcing Generalized Refinement-Based Noninterference for Secure Interface Composition}, 
	year={2017},
	volume={1},
	number={},
	pages={586-595},
	doi={10.1109/COMPSAC.2017.118}}

%Baumann
@INPROCEEDINGS {baumann,
	author = {<NAME> and <NAME> and <NAME> and <NAME>},
	booktitle = {2021 2021 IEEE 34th Computer Security Foundations Symposium (CSF)},
	title = {On Compositional Information Flow Aware Refinement},
	year = {2021},
	volume = {},
	issn = {2374-8303},
	pages = {79-94},
	keywords = {security;confidentiality;noninterference;simulation;ignorance;knowledge;oram;unwinding;verification;specification;observation},
	doi = {10.1109/CSF51468.2021.00010},
	url = {https://doi.ieeecomputersociety.org/10.1109/CSF51468.2021.00010},
	publisher = {IEEE Computer Society},
	address = {Los Alamitos, CA, USA},
	month = {jun}
}

%Disksec
@inproceedings {disksec,
	author = {<NAME> and <NAME> and <NAME> and <NAME> and <NAME>},
	title = {Proving confidentiality in a file system using DiskSec},
	booktitle = {13th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 18)},
	year = {2018},
	isbn = {978-1-939133-08-3},
	address = {Carlsbad, CA},
	pages = {323--338},
	url = {https://www.usenix.org/conference/osdi18/presentation/ileri},
	publisher = {{USENIX} Association},
	month = oct,
}