{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:13Z","timestamp":1773193513791,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T00:00:00Z","timestamp":1725408000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1846230, 1953932"],"award-info":[{"award-number":["1846230, 1953932"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,4]]},"DOI":"10.1145\/3678015.3680486","type":"proceedings-article","created":{"date-parts":[[2024,8,29]],"date-time":"2024-08-29T12:19:32Z","timestamp":1724933972000},"page":"115-121","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Hora: High Assurance Periodic Availability Guarantee for Life-Critical Applications on Smartphones"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-5255-5286","authenticated-orcid":false,"given":"Dylan","family":"Zueck","sequence":"first","affiliation":[{"name":"University of California, Irvine, Irvine, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0453-6490","authenticated-orcid":false,"given":"Nathaniel","family":"Atallah","sequence":"additional","affiliation":[{"name":"University of California, Irvine, Irvine, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7948-3304","authenticated-orcid":false,"given":"Ian","family":"Do","sequence":"additional","affiliation":[{"name":"University of California, Irvine, Irvine, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9842-0713","authenticated-orcid":false,"given":"Zhihao","family":"Yao","sequence":"additional","affiliation":[{"name":"New Jersey Institute of Technology, Newark, New Jersey, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0130-587X","authenticated-orcid":false,"given":"Ardalan Amiri","family":"Sani","sequence":"additional","affiliation":[{"name":"University of California, Irvine, Irvine, California, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,9,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2022. AndroidAPS app documentation. http:\/\/wiki.aaps.app\/en\/latest\/."},{"key":"e_1_3_2_1_2_1","unstructured":"2022. Source code for the split-trust hardware and its OS OctopOS. https:\/\/github.com\/trusslab\/octopos_hardware https:\/\/github.com\/trusslab\/octopos."},{"key":"e_1_3_2_1_3_1","unstructured":"2024. Google \u00bb Android (Operating system): Product Details Threats and Statistics. https:\/\/www.cvedetails.com\/product\/19997\/Google-Android.html."},{"key":"e_1_3_2_1_4_1","unstructured":"2024. Simplicity Starts With Omnipod DASH\u00ae. https:\/\/www.omnipod.com\/what-is-omnipod\/omnipod-dash."},{"key":"e_1_3_2_1_5_1","unstructured":"2024. Simplify Life\u00ae With Omnipod\u00ae 5 Tubeless Automated Insulin Delivery. https:\/\/www.omnipod.com\/what-is-omnipod\/omnipod-5."},{"key":"e_1_3_2_1_6_1","unstructured":"2024. The Coq Proof Assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_7_1","unstructured":"2024. The Kani Rust Verifier. https:\/\/model-checking.github.io\/kani\/."},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. ACM CCS. 1357--1372","author":"Alder F.","unstructured":"F. Alder, J. Van Bulck, F. Piessens, and Jan T. M\u00fchlberg. 2021. Aion: Enabling open systems through strong availability guarantees for enclaves. In Proc. ACM CCS. 1357--1372."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICESC.2014.15"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"G. Klein K. Elphinstone G. Heiser J. Andronick D. Cock P. Derrin D. Elkaduwe K. Engelhardt R. Kolanski M. Norrish et al. 2009. seL4: Formal Verification of an OS Kernel. In SOSP. 207--220.","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. USENIX OSDI. 465--484","author":"Li X.","unstructured":"X. Li, X. Li, C. Dall, R. Gu, J. Nieh, Y. Sait, and G. Stockwell. 2022. Design and verification of the Arm Confidential Compute Architecture. In Proc. USENIX OSDI. 465--484."},{"key":"e_1_3_2_1_12_1","volume-title":"General-Purpose Microkernel. In Workshop on Mixed Criticality Systems. 9--14","author":"Lyons A.","unstructured":"A. Lyons and G. Heiser. 2014. Mixed-Criticality Support in a High-Assurance, General-Purpose Microkernel. In Workshop on Mixed Criticality Systems. 9--14."},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. ACM ACSAC. 61--70","author":"Masti Ramya J.","unstructured":"Ramya J. Masti, C. Marforio, A. Ranganathan, A. Francillon, and S. Capkun. 2012. Enabling Trusted Scheduling in Embedded Systems. In Proc. ACM ACSAC. 61--70."},{"key":"e_1_3_2_1_14_1","volume-title":"Paulson","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow, M. Wenzel, and Lawrence C. Paulson. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"P. Puschner and C. Koza. 1989. Calculating the Maximum Execution Time of Real-Time Programs. Real-time systems 1 2 (1989) 159--176.","DOI":"10.1007\/BF00571421"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2019.07.004"},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. USENIX OSDI. 1--16","author":"Sigurbjarnarson H.","unstructured":"H. Sigurbjarnarson, J. Bornholt, E. Torlak, and X. Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proc. USENIX OSDI. 1--16."},{"key":"e_1_3_2_1_18_1","volume-title":"NEWS: OmniPod Tubeless Insulin Pump to Offer Smartphone Control Soon. https:\/\/www.healthline.com\/diabetesmine\/omnipod-smartphone-control-diabetes.","author":"Team DiabetesMine","year":"2019","unstructured":"DiabetesMine Team. 2019. NEWS: OmniPod Tubeless Insulin Pump to Offer Smartphone Control Soon. https:\/\/www.healthline.com\/diabetesmine\/omnipod-smartphone-control-diabetes."},{"key":"e_1_3_2_1_19_1","volume-title":"Statically-Partitioned Hardware. In Proc. ACM MobiSys.","author":"Yao Z.","unstructured":"Z. Yao, S. M. Seyed Talebi, M. Chen, A. Amiri Sani, and T. Anderson. 2023. Minimizing a Smartphone's TCB for Security-Critical Programs with Exclusively-Used, Physically-Isolated, Statically-Partitioned Hardware. In Proc. ACM MobiSys."}],"event":{"name":"APSys '24: 15th ACM SIGOPS Asia-Pacific Workshop on Systems","location":"Kyoto Japan","acronym":"APSys '24","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the 15th ACM SIGOPS Asia-Pacific Workshop on Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678015.3680486","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3678015.3680486","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T02:13:44Z","timestamp":1755915224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678015.3680486"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,4]]},"references-count":19,"alternative-id":["10.1145\/3678015.3680486","10.1145\/3678015"],"URL":"https:\/\/doi.org\/10.1145\/3678015.3680486","relation":{},"subject":[],"published":{"date-parts":[[2024,9,4]]},"assertion":[{"value":"2024-09-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}