{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:46:58Z","timestamp":1750308418968,"version":"3.41.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T00:00:00Z","timestamp":1598832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2020,8,31]]},"abstract":"<jats:p>We describe our ongoing research that aims to eliminate microarchitectural timing channels through time protection, which eliminates the root cause of these channels, competition for capacity-limited hardware resources. A proof-ofconcept implementation of time protection demonstrated the approach can be effective a nd l ow o verhead, b ut also that present hardware fails to support the approach in some aspects and that we need an improved hardXare-software contract to achieve real security. We have demonstrated that these mechanisms are not hard to provide, and are working on their inclusion in the RISC-V ISA. Assuming compliant hardware, we outline how we think we can then formally prove that timing channels are eliminated.<\/jats:p>","DOI":"10.1145\/3421473.3421475","type":"journal-article","created":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T13:31:19Z","timestamp":1598880679000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Towards Provable Timing-Channel Prevention"],"prefix":"10.1145","volume":"54","author":[{"given":"Gernot","family":"Heiser","sequence":"first","affiliation":[{"name":"UNSW Sydney, Sydney, Australia"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"University of Melbourne, Melbourne, Australia"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Sydney, Australia"}]}],"member":"320","published-online":{"date-parts":[[2020,8,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"ARINC 2012. Avionics Application Software Standard Interface. ARINC. ARINC Standard 653.  ARINC 2012. Avionics Application Software Standard Interface. ARINC. ARINC Standard 653."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2086696.2086714"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303976"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-016-0141-6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3265723.3265724"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CLOUD.2013.21"},{"volume-title":"Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures","author":"Guanciale Roberto","key":"e_1_2_1_9_1","unstructured":"Roberto Guanciale , Hamed Nemati , Christoph Baumann , and Mads Dam . 2016. Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures . San Jose, CA , US , 38--55. Roberto Guanciale, Hamed Nemati, Christoph Baumann, and Mads Dam. 2016. Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. San Jose, CA, US, 38--55."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3317550.3321431"},{"volume-title":"Deep Dive: Intel Analysis of L1 Terminal Fault. https:\/\/software.intel.com\/security-software-guidance\/insights\/deepdive- intel-analysis-l1-terminal-fault","year":"2018","key":"e_1_2_1_11_1","unstructured":"Intel. 2018 a. Deep Dive: Intel Analysis of L1 Terminal Fault. https:\/\/software.intel.com\/security-software-guidance\/insights\/deepdive- intel-analysis-l1-terminal-fault Intel. 2018a. Deep Dive: Intel Analysis of L1 Terminal Fault. https:\/\/software.intel.com\/security-software-guidance\/insights\/deepdive- intel-analysis-l1-terminal-fault"},{"key":"e_1_2_1_12_1","unstructured":"Intel. 2018b. Speculative Execution Side Channel Mitigations. https:\/\/software.intel.com\/sites\/default\/files\/managed\/c5\/63\/336996- Speculative-Execution-Side-Channel-Mitigations.pdf  Intel. 2018b. Speculative Execution Side Channel Mitigations. https:\/\/software.intel.com\/sites\/default\/files\/managed\/c5\/63\/336996- Speculative-Execution-Side-Channel-Mitigations.pdf"},{"volume-title":"Intel 64 and IA-32 Architecture Software Developer's Manual Volume 2: Instruction Set Reference","author":"Intel Corporation 2016.","key":"e_1_2_1_13_1","unstructured":"Intel Corporation 2016. Intel 64 and IA-32 Architecture Software Developer's Manual Volume 2: Instruction Set Reference , A-Z. Intel Corporation . http:\/\/www.intel.com.au\/content\/dam\/www\/public\/us\/en\/documents\/ manuals\/64-ia-32-architectures-software-developer-instruction-setreference- manual-325383.pdf. Intel Corporation 2016. Intel 64 and IA-32 Architecture Software Developer's Manual Volume 2: Instruction Set Reference, A-Z. Intel Corporation. http:\/\/www.intel.com.au\/content\/dam\/www\/public\/us\/en\/documents\/ manuals\/64-ia-32-architectures-software-developer-instruction-setreference- manual-325383.pdf."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/138873.138876"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1991596.1991634"},{"key":"e_1_2_1_17_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution. In IEEE Symposium on Security and Privacy. IEEE","author":"Kocher Paul","year":"2019","unstructured":"Paul Kocher , Jann Horn , Anders Fogh , Daniel Genkin , Daniel Gruss , Werner Haas , Mike Haburg , Moritz Lipp , Stefan Mangard , Thomas Prescher , Michael Schwartz , and Yuval Yarom . 2019 . Spectre Attacks: Exploiting Speculative Execution. In IEEE Symposium on Security and Privacy. IEEE , San Francisco, 19--37. https:\/\/ts.data61.csiro.au\/publications\/csiro_full_ text\/\/Kocher_HFGGHHLMPSY_19.pdf Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss,Werner Haas, Mike Haburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwartz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In IEEE Symposium on Security and Privacy. IEEE, San Francisco, 19--37. https:\/\/ts.data61.csiro.au\/publications\/csiro_full_ text\/\/Kocher_HFGGHHLMPSY_19.pdf"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/362375.362389"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/523983.828369"},{"key":"e_1_2_1_20_1","volume-title":"CATalyst: Defeating Last-Level Cache Side Channel Attacks in Cloud Computing. In IEEE Symposium on High- Performance Computer Architecture. IEEE","author":"Liu Fangfei","year":"2016","unstructured":"Fangfei Liu , Qian Ge , Yuval Yarom , Frank Mckeen , Carlos Rozas , Gernot Heiser , and Ruby B Lee . 2016 . CATalyst: Defeating Last-Level Cache Side Channel Attacks in Cloud Computing. In IEEE Symposium on High- Performance Computer Architecture. IEEE , Barcelona, Spain, 406--418. https:\/\/ts.data61.csiro.au\/publications\/nicta_full_text\/8984.pdf Fangfei Liu, Qian Ge, Yuval Yarom, Frank Mckeen, Carlos Rozas, Gernot Heiser, and Ruby B Lee. 2016. CATalyst: Defeating Last-Level Cache Side Channel Attacks in Cloud Computing. In IEEE Symposium on High- Performance Computer Architecture. IEEE, Barcelona, Spain, 406--418. https:\/\/ts.data61.csiro.au\/publications\/nicta_full_text\/8984.pdf"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/144965.145814"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3190508.3190539"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11605805_1"},{"key":"e_1_2_1_25_1","volume-title":"Program Verification in the Presence of Cached Address Translation. In International Conference on Interactive Theorem Proving","volume":"10895","author":"Syeda Hira","year":"2018","unstructured":"Hira Syeda and Gerwin Klein . 2018 . Program Verification in the Presence of Cached Address Translation. In International Conference on Interactive Theorem Proving , Vol. 10895 . Lecture Notes in Computer Science, Oxford, UK, 542--559. https:\/\/ts.data61.csiro.au\/publications\/csiro_full_ text\/\/Syeda_Klein_18.pdf 6 Hira Syeda and Gerwin Klein. 2018. Program Verification in the Presence of Cached Address Translation. In International Conference on Interactive Theorem Proving, Vol. 10895. Lecture Notes in Computer Science, Oxford, UK, 542--559. https:\/\/ts.data61.csiro.au\/publications\/csiro_full_ text\/\/Syeda_Klein_18.pdf 6"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1669112.1669174"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024723.2000087"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_26"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273440.1250723"},{"key":"e_1_2_1_30_1","volume-title":"Workshop on Computer Architecture Research with RISC-V (CARRV). ACM","author":"Wistoff Nils","year":"2020","unstructured":"Nils Wistoff , Moritz Schneider , Frank G\u00fcrkaynak , Luca Benini , and Gernot Heiser . 2020 . Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core . In Workshop on Computer Architecture Research with RISC-V (CARRV). ACM , Valencia, Spain, 7. https:\/\/ts.data61. csiro.au\/publications\/csiro_full_text\/\/Wistoff_SGBH_20.pdf Nils Wistoff, Moritz Schneider, Frank G\u00fcrkaynak, Luca Benini, and Gernot Heiser. 2020. Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core. In Workshop on Computer Architecture Research with RISC-V (CARRV). ACM, Valencia, Spain, 7. https:\/\/ts.data61. csiro.au\/publications\/csiro_full_text\/\/Wistoff_SGBH_20.pdf"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/RISP.1991.130767"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2013.6531079"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516741"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421475","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3421473.3421475","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:21Z","timestamp":1750268961000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421475"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,31]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,8,31]]}},"alternative-id":["10.1145\/3421473.3421475"],"URL":"https:\/\/doi.org\/10.1145\/3421473.3421475","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2020,8,31]]},"assertion":[{"value":"2020-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}