{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:11:34Z","timestamp":1755839494309,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031274800"},{"type":"electronic","value":"9783031274817"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-27481-7_8","type":"book-chapter","created":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T14:03:10Z","timestamp":1677765790000},"page":"103-121","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalising the\u00a0Prevention of\u00a0Microarchitectural Timing Channels by\u00a0Operating Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0313-9764","authenticated-orcid":false,"given":"Robert","family":"Sison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8810-9323","authenticated-orcid":false,"given":"Scott","family":"Buckley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8271-0289","authenticated-orcid":false,"given":"Toby","family":"Murray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8883-0559","authenticated-orcid":false,"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7069-0831","authenticated-orcid":false,"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,3,3]]},"reference":[{"key":"8_CR1","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: USENIX Security Symposium, pp. 53\u201370 (2016)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-21437-0_19","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Formally verifying isolation and availability in an idealized model of virtualization. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 231\u2013245. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_19"},{"key":"8_CR3","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: Proceedings of the 25th IEEE Computer Security Foundations Symposium, pp. 186\u2013197. IEEE (2012)","DOI":"10.1109\/CSF.2012.17"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.D., Pichardie, D.: System-level non-interference for constant-time cryptography. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, 3\u20137 November 2014, pp. 1267\u20131279. ACM (2014). https:\/\/doi.org\/10.1145\/2660267.2660283","DOI":"10.1145\/2660267.2660283"},{"key":"8_CR5","unstructured":"Buckley, S., Sison, R., Klein, G.: An Isabelle\/HOL formalisation of microarchitectural timing channel prevention by operating systems - VM artifact and proof release (2022). https:\/\/zenodo.org\/record\/7340166"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Cauligi, S., et al.: Constant-time foundations for the new spectre era. In: Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15\u201320 June 2020, pp. 913\u2013926. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385970","DOI":"10.1145\/3385412.3385970"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Chen, H., Shapiro, J.S.: Using build-integrated static checking to preserve correctness invariants. In: Proceedings of the 11th ACM Conference on Computer and Communications Security, CCS 2004, Washington, DC, USA, 25\u201329 October 2004, pp. 288\u2013297. ACM (2004). https:\/\/doi.org\/10.1145\/1030083.1030122","DOI":"10.1145\/1030083.1030122"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Costanzo, D., Shao, Z., Gu, R.: End-to-end verification of information-flow security for C and assembly programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 648\u2013664 (2016)","DOI":"10.1145\/2980983.2908100"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Daum, M., Billing, N., Klein, G.: Concerned with the unprivileged: user programs in kernel refinement. Formal Aspects Comput. 26(6), 1205\u20131229 (2014). https:\/\/trustworthy.systems\/publications\/nicta_full_text\/7114.pdf","DOI":"10.1007\/s00165-014-0296-9"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/365230.365252","volume":"9","author":"JB Dennis","year":"1966","unstructured":"Dennis, J.B., Van Horn, E.C.: Programming semantics for multiprogrammed computations. Commun. ACM 9, 143\u2013155 (1966)","journal-title":"Commun. ACM"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Ge, Q., Yarom, Y., Chothia, T., Heiser, G.: Time protection: the missing OS abstraction. In: EuroSys Conference. ACM, Dresden (2019). https:\/\/trustworthy.systems\/publications\/full_text\/Ge_YCH_19.pdf","DOI":"10.1145\/3302424.3303976"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Ge, Q., Yarom, Y., Cock, D., Heiser, G.: A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. J. Cryptogr. Eng. 8, 1\u201327 (2018). https:\/\/trustworthy.systems\/publications\/full_text\/Ge_YCH_18.pdf","DOI":"10.1007\/s13389-016-0141-6"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Ge, Q., Yarom, Y., Heiser, G.: No security without time protection: we need a new hardware-software contract. In: Asia-Pacific Workshop on Systems (APSys). ACM SIGOPS, Korea (2018). https:\/\/trustworthy.systems\/publications\/full_text\/Ge_YH_18.pdf","DOI":"10.1145\/3265723.3265724"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Gullasch, D., Bangerter, E., Krenn, S.: Cache games - bringing access-based cache attacks on AES to practice. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 490\u2013505. IEEE, Oakland (2011)","DOI":"10.1109\/SP.2011.22"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Heiser, G., Klein, G., Murray, T.: Can we prove time protection? In: Workshop on Hot Topics in Operating Systems (HotOS), pp. 23\u201329. ACM, Bertinoro (2019). https:\/\/trustworthy.systems\/publications\/full_text\/Heiser_KM_19.pdf","DOI":"10.1145\/3317550.3321431"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Heiser, G., Murray, T., Klein, G.: Towards provable timing-channel prevention. ACM Oper. Syst. Rev. 54, 1\u20137 (2020). https:\/\/trustworthy.systems\/publications\/full_text\/Heiser_MK_20.pdf","DOI":"10.1145\/3421473.3421475"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/138873.138876","volume":"10","author":"RE Kessler","year":"1992","unstructured":"Kessler, R.E., Hill, M.D.: Page placement algorithms for large real-indexed caches. ACM Trans. Comput. Syst. 10, 338\u2013359 (1992)","journal-title":"ACM Trans. Comput. Syst."},{"key":"8_CR18","unstructured":"Kim, T., Peinado, M., Mainar-Ruiz, G.: StealthMem: system-level protection against cache-based side channel attacks in the cloud. In: Proceedings of the 21st USENIX Security Symposium, pp. 189\u2013204. USENIX, Bellevue (2012)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: Formal verification of an OS kernel. In: ACM Symposium on Operating Systems Principles, pp. 207\u2013220. ACM, Big Sky (2009). https:\/\/trustworthy.systems\/publications\/nicta_full_text\/1852.pdf","DOI":"10.1145\/1629575.1629596"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/3399742","volume":"63","author":"P Kocher","year":"2020","unstructured":"Kocher, P., et al.: Spectre attacks: exploiting speculative execution [abridged version]. Commun. ACM 63, 93\u2013101 (2020)","journal-title":"Commun. ACM"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Li, S.W., Li, X., Gu, R., Nieh, J., Hui, J.Z.: A secure and formally verified Linux KVM hypervisor. In: IEEE Security and Privacy (2021)","DOI":"10.1109\/SP40001.2021.00049"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Liedtke, J., H\u00e4rtig, H., Hohmuth, M.: OS-controlled cache predictability for real-time systems. In: IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 213\u2013223. IEEE, Montreal (1997)","DOI":"10.1109\/RTTAS.1997.601360"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Liu, M., et al.: Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. Proc. ACM Program. Lang. 4(POPL), 1\u201331 (2019)","DOI":"10.1145\/3371088"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Murray, T., et al.: seL4: from general purpose to a proof of information flow enforcement. In: IEEE Symposium on Security and Privacy, pp. 415\u2013429. IEEE, San Francisco (2013). https:\/\/trustworthy.systems\/publications\/nicta_full_text\/6464.pdf","DOI":"10.1109\/SP.2013.35"},{"key":"8_CR25","doi-asserted-by":"publisher","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. 7679, pp. 126\u2013142. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_12, https:\/\/trustworthy.systems\/publications\/nicta_full_text\/6004.pdf","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11605805_1","volume-title":"Topics in Cryptology \u2013 CT-RSA 2006","author":"DA Osvik","year":"2006","unstructured":"Osvik, D.A., Shamir, A., Tromer, E.: Cache attacks and countermeasures: the case of AES. In: Pointcheval, D. (ed.) CT-RSA 2006. LNCS, vol. 3860, pp. 1\u201320. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11605805_1"},{"key":"8_CR28","unstructured":"Percival, C.: Cache missing for fun and profit. In: BSDCan 2005, Ottawa, CA (2005). http:\/\/css.csail.mit.edu\/6.858\/2014\/readings\/ht-cache.pdf"},{"key":"8_CR29","unstructured":"seL4 microkernel code and proofs. https:\/\/github.com\/seL4\/"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Sewell, T., Kam, F., Heiser, G.: Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis. In: IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria (2016). https:\/\/trustworthy.systems\/publications\/nicta_full_text\/9118.pdf","DOI":"10.1109\/RTAS.2016.7461326"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Sewell, T., Kam, F., Heiser, G.: High-assurance timing analysis for a high-assurance real-time OS. Real-Time Syst. 53, 812\u2013853 (2017). https:\/\/trustworthy.systems\/publications\/full_text\/Sewell_KH_17.pdf","DOI":"10.1007\/s11241-017-9286-3"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 enforces integrity. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 325\u2013340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_24, https:\/\/trustworthy.systems\/publications\/nicta_full_text\/4709.pdf","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"8_CR33","doi-asserted-by":"publisher","first-page":"16395","DOI":"10.1109\/ACCESS.2018.2815766","volume":"6","author":"J Sun","year":"2018","unstructured":"Sun, J., Long, X., Zhao, Y.: A verified capability-based model for information flow security with dynamic policies. IEEE Access 6, 16395\u201316407 (2018)","journal-title":"IEEE Access"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Wistoff, N., Schneider, M., G\u00fcrkaynak, F., Benini, L., Heiser, G.: Microarchitectural timing channels and their prevention on an open-source 64-bit RISC-V core. In: Design, Automation and Test in Europe (DATE). IEEE, Virtual (2021). https:\/\/trustworthy.systems\/publications\/full_text\/Wistoff_SGBH_21.pdf","DOI":"10.23919\/DATE51398.2021.9474214"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Wistoff, N., Schneider, M., G\u00fcrkaynak, F., Heiser, G., Benini, L.: Systematic prevention of on-core timing channels by full temporal partitioning. IEEE Trans. Comput. (2023, to appear). https:\/\/trustworthy.systems\/publications\/papers\/Wistoff_SGHB_23.pdf","DOI":"10.1109\/TC.2022.3212636"},{"key":"8_CR36","unstructured":"Yarom, Y., Falkner, K.: Flush+Reload: a high resolution, low noise, L3 cache side-channel attack. In: Proceedings of the 23rd USENIX Security Symposium, pp. 719\u2013732. USENIX, San Diego (2014)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-27481-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,15]],"date-time":"2024-10-15T16:21:53Z","timestamp":1729009313000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-27481-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031274800","9783031274817"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-27481-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 March 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"L\u00fcbeck","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 March 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 March 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fm2023.isp.uni-luebeck.de\/wordpress\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"95","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also include 7 short industry papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}