{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:50:39Z","timestamp":1725742239367},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_23","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"311-327","source":"Crossref","is-referenced-by-count":2,"title":["Practical Probability: Applying pGCL to Lattice Scheduling"],"prefix":"10.1007","author":[{"given":"David","family":"Cock","sequence":"first","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Cache-leakage resilient os isolation in an idealized model of virtualization. In: 25th Comp. Security Foundations WS, pp. 186\u2013197 (2012)","key":"23_CR1","DOI":"10.1109\/CSF.2012.17"},{"unstructured":"Bernstein, D.J.: Cache-timing attacks on AES (2004)","key":"23_CR2"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/1255329.1255335","volume-title":"Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS 2007","author":"H. Chen","year":"2007","unstructured":"Chen, H., Malacaria, P.: Quantitative analysis of leakage for multi-threaded programs. In: Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS 2007, pp. 31\u201340. ACM, New York (2007)"},{"doi-asserted-by":"crossref","unstructured":"Cock, D.: Verifying probabilistic correctness in isabelle with pGCL. In: Systems Software Verification, Sydney, Australia, p. 10 (November 2012)","key":"23_CR5","DOI":"10.4204\/EPTCS.102.15"},{"key":"23_CR6","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D.E. Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. CACM\u00a019, 236\u2013242 (1976)","journal-title":"CACM"},{"issue":"8","key":"23_CR7","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. CACM\u00a018(8), 453\u2013457 (1975)","journal-title":"CACM"},{"unstructured":"US Department of Defence. Trusted Computer System Evaluation Criteria, DoD 5200.28-STD (1986)","key":"23_CR8"},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s001650300006","volume":"14","author":"C. Fidge","year":"2003","unstructured":"Fidge, C., Shankland, C.: But what if i don\u2019t want to wait forever? Formal Aspects of Computing\u00a014, 281\u2013294 (2003)","journal-title":"Formal Aspects of Computing"},{"doi-asserted-by":"crossref","unstructured":"Gong, X., Kiyavash, N., Venkitasubramaniam, P.: Information theoretic analysis of side channel information leakage in FCFS schedulers. In: 2011 IEEE International Symposium on Information Theory Proceedings (ISIT), pp. 1255\u20131259 (August 2011)","key":"23_CR10","DOI":"10.1109\/ISIT.2011.6033737"},{"issue":"1","key":"23_CR11","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science\u00a0346(1), 96\u2013112 (2005)","journal-title":"Theoretical Computer Science"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-31762-0_12","volume-title":"Formal Verification of Object-Oriented Software","author":"M. Huisman","year":"2012","unstructured":"Huisman, M., Ngo, T.M.: Scheduler-specific confidentiality for multi-threaded programs and its logic-based verification. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 178\u2013195. Springer, Heidelberg (2012)"},{"unstructured":"Hu, W.M.: Lattice scheduling and covert channels. In: IEEE Symp. Security & Privacy, pp. 52\u201361 (1992)","key":"23_CR13"},{"doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, pp. 207\u2013220. ACM (2009)","key":"23_CR14","DOI":"10.1145\/1629575.1629596"},{"issue":"11","key":"23_CR15","doi-asserted-by":"publisher","first-page":"1147","DOI":"10.1109\/32.106971","volume":"17","author":"P.A. Karger","year":"1991","unstructured":"Karger, P.A., Zurko, M.E., Bonin, D.W., Mason, A.H., Kahn, C.E.: A retrospective on the VAX VMM security kernel. Trans. Softw. Engin.\u00a017(11), 1147\u20131165 (1991)","journal-title":"Trans. Softw. Engin."},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1093\/jigpal\/7.6.779","volume":"7","author":"C. Morgan","year":"1999","unstructured":"Morgan, C., Mciver, A.K.: An expectation-based model for probabilistic temporal logic. Logic Journal of the IGPL\u00a07, 779\u2013804 (1999)","journal-title":"Logic Journal of the IGPL"},{"unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2004)","key":"23_CR17"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-33826-7_23","volume-title":"Software Engineering and Formal Methods","author":"D. Matichuk","year":"2012","unstructured":"Matichuk, D., Murray, T.: Extensible specifications for automatic re-use of specifications and proofs. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 333\u2013341. Springer, Heidelberg (2012)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-35308-6_12","volume-title":"Certified Programs and Proofs","author":"T. Murray","year":"2012","unstructured":"Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 126\u2013142. Springer, Heidelberg (2012)"},{"unstructured":"Percival, C.: Cache missing for fun and profit. In: BSDCan 2005 (2005)","key":"23_CR20"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-30108-0_14","volume-title":"Computer Security \u2013 ESORICS 2004","author":"D. Oheimb von","year":"2004","unstructured":"von Oheimb, D.: Information flow control revisited: Noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol.\u00a03193, pp. 225\u2013243. Springer, Heidelberg (2004)"},{"unstructured":"Waldspurger, C.A., Weihl, W.E.: Lottery scheduling: Flexible proportional-share resource management. In: 1st OSDI, Monterey, CA, USA, pp. 1\u201311 (November 1994)","key":"23_CR22"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T02:18:13Z","timestamp":1557973093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}