{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T08:55:49Z","timestamp":1767084949424,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T00:00:00Z","timestamp":1737504000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000005","name":"Department of Defense","doi-asserted-by":"crossref","award":["FA8702-15-D-0002"],"award-info":[{"award-number":["FA8702-15-D-0002"]}],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Carnegie Mellon University for the operation of the Software Engineering Institute","award":["DM23-0365"],"award-info":[{"award-number":["DM23-0365"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2025,1,31]]},"abstract":"<jats:p>Verifying complex Cyber-physical Systems (CPSs) is increasingly important given the push to deploy safety-critical autonomous features. Unfortunately, traditional verification methods do not scale to the complexity of these systems and do not provide systematic methods to protect verified properties when not all the components can be verified. To address these challenges, this article proposes a real-time mixed-trust computing framework that combines verification and protection. The framework introduces a new task model, where an application task can have both an untrusted and a trusted part. The untrusted part allows complex computations supported by a full OS with a real-time scheduler running in a VM hosted by a trusted hypervisor. The trusted part is executed by another scheduler within the hypervisor and is thus protected from the untrusted part. If the untrusted part fails to finish by a specific time, the trusted part is activated to preserve safety (e.g., prevent a crash) including its timing guarantees. This framework is the first allowing the use of untrusted components for CPS critical functions while preserving logical and timing guarantees, even in the presence of malicious attackers. We present the framework, its schedulability analysis, and the coordination protocol between the trusted and untrusted parts. Our implementation on a Raspberry Pi\u00a03 is also discussed along with experiments showing the behavior of the system under failures of untrusted components and a drone application to demonstrate its practicality.<\/jats:p>","DOI":"10.1145\/3635162","type":"journal-article","created":{"date-parts":[[2023,12,2]],"date-time":"2023-12-02T11:54:19Z","timestamp":1701518059000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Mixed-trust Computing: Safe and Secure Real-time Systems"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5560-590X","authenticated-orcid":false,"given":"Dionisio","family":"de Niz","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4718-5722","authenticated-orcid":false,"given":"Bjorn","family":"Andersson","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5605-7995","authenticated-orcid":false,"given":"Mark","family":"Klein","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-5638-5279","authenticated-orcid":false,"given":"John","family":"Lehoczky","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8553-732X","authenticated-orcid":false,"given":"Hyoseung","family":"Kim","sequence":"additional","affiliation":[{"name":"University of California, Riverside, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4604-0839","authenticated-orcid":false,"given":"Gabriel","family":"Moreno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,22]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"Pixhawk. The Open Standard for Drone Hardware. https:\/\/pixhawk.org"},{"key":"e_1_3_2_3_2","unstructured":"Open Source Autopilot for Drone Developers. https:\/\/px4.io"},{"key":"e_1_3_2_4_2","unstructured":"Dronecode Foundation. https:\/\/dronecode.org"},{"key":"e_1_3_2_5_2","unstructured":"RTCA Special Committee 205. 2011. Formal Methods Supplement to DO-178C and DO-278A."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2018.00010"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3055004.3055012"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Bjorn Andersson Sagar Chaki and Dionisio de Niz. 2017. Combining symbolic runtime enforcers for cyber-physical systems. In International Conference in Runtime Verification.","DOI":"10.1007\/978-3-319-67531-2_5"},{"key":"e_1_3_2_9_2","unstructured":"E. Armbrust J. Song G. Bloom and G. Parmer. 2014. On spatial isolation for mixed criticality embedded systems. In Proceedings of the 2nd International Workshop on Mixed Criticality Systems (WMC\u201914)."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"S. Bak T. T. Johnson M. Caccamo and L. Sha. 2014. Real-time reachability for verified simplex design. IEEE Real-Time Systems Symposium. 138\u2013148. DOI:10.1109\/RTSS.2014.21","DOI":"10.1109\/RTSS.2014.21"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"S. K. Baruah. 2003. Dynamic- and static-priority scheduling of recurring real-time tasks. Real-Time Systems 24 93-128 (2003). 10.1023\/A:1021711220939","DOI":"10.1023\/A:1021711220939"},{"key":"e_1_3_2_12_2","article-title":"A safe, secure, and predictable software architecture for deep learning in safety-critical systems","author":"Biondi Alessandro","year":"2020","unstructured":"Alessandro Biondi, Federico Nesti, Giorgiomaria Cicero, Daniel Casini, and Giorgio Buttazzo. 2020. A safe, secure, and predictable software architecture for deep learning in safety-critical systems. IEEE Embedded Systems Letter (2020).","journal-title":"IEEE Embedded Systems Letter"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Sagar Chaki and Dionisio De Niz. 2017. Formal verification of a timing enforcer implementation. ACM Trans. Embed. Comput. Syst. 16 5s (2017) 19 pages. 10.1145\/3126517","DOI":"10.1145\/3126517"},{"key":"e_1_3_2_14_2","volume-title":"Congress of the International Council of the Aeronautical Sciences (ICAS \u201912)","author":"Consiglio M. C.","year":"2012","unstructured":"M. C. Consiglio, J. P. Chamberlain, C. A. Munoz, and K. D. Hoffler. 2012. Concepts of integration for UAS operations in the NAS. In Congress of the International Council of the Aeronautical Sciences (ICAS \u201912)."},{"key":"e_1_3_2_15_2","volume-title":"EDCC","author":"Correia M.","year":"2002","unstructured":"M. Correia, P. Verissimo, and N. F. Neves. 2002. The design of a COTS real-time distributed security kernel. In EDCC."},{"key":"e_1_3_2_16_2","volume-title":"EDCC","author":"Crespo A.","year":"2010","unstructured":"A. Crespo, I. Ripoll, and M. Masmano. 2010. Partitioned embedded architecture based on hypervisor: The XtratuM approach. In EDCC."},{"key":"e_1_3_2_17_2","volume-title":"Technical Report, University of York","author":"Davis R.","year":"2019","unstructured":"R. Davis and A. Burns. 2019. Mixed-criticality systems\u2014A review. Technical Report, University of York. https:\/\/www-users.cs.york.ac.uk\/burns\/review.pdf"},{"key":"e_1_3_2_18_2","article-title":"Controller area network (CAN) schedulability analysis: Refuted, revisited and revised","author":"Davis R. I.","year":"2007","unstructured":"R. I. Davis, A. Burns, R. J. Bril, and J. J. Lukkien. 2007. Controller area network (CAN) schedulability analysis: Refuted, revisited and revised. Real-time Systems (2007).","journal-title":"Real-time Systems"},{"key":"e_1_3_2_19_2","first-page":"1","volume-title":"The 25th IEEE International Conference on Embedded and Real-time Computing Systems and Applications","author":"Niz Dionisio de","year":"2019","unstructured":"Dionisio de Niz, Bj\u00f6rn Andersson, Mark H. Klein, John P. Lehoczky, Amit Vasudevan, Hyoseung Kim, and Gabriel A. Moreno. 2019. Mixed-trust computing for real-time systems. In The 25th IEEE International Conference on Embedded and Real-time Computing Systems and Applications. 1\u201311."},{"key":"e_1_3_2_20_2","volume-title":"Proceedings of SPIE","author":"Niz D. de","year":"2018","unstructured":"D. de Niz, B. Andersson, and G. Moreno. 2018. Safety enforcement for the verification of autonomous systems. In Proceedings of SPIE."},{"key":"e_1_3_2_21_2","volume-title":"RTSS","author":"Niz D. de","year":"2009","unstructured":"D. de Niz, K. Lakshmanan, and R. Rajkumar. 2009. On the scheduling of mixed-criticality real-time task sets. In RTSS."},{"key":"e_1_3_2_22_2","volume-title":"ECRTS","author":"Ding H.","year":"2006","unstructured":"H. Ding, L. Arber, L. Sha, and M. Caccamo. 2006. The dependency management framework: A case study of the ION CubeSat. In ECRTS."},{"key":"e_1_3_2_23_2","volume-title":"ISORC","author":"Easwaran A.","year":"2007","unstructured":"A. Easwaran, I. Lee, I. Shin, and O. Sokolsky. 2007. Compositional schedulability analysis of hierarchical real-time systems. In ISORC."},{"key":"e_1_3_2_24_2","volume-title":"OSDI","author":"Gu R.","year":"2016","unstructured":"R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim, V. Sj\u00f6berg, and D. Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In OSDI."},{"key":"e_1_3_2_25_2","volume-title":"RTAS","author":"Jiang Z.","year":"2018","unstructured":"Z. Jiang, N. C. Audsley, and P. Dong. 2018. BlueVisor: A scalable real-time hardware hypervisor for many-core embedded systems. In RTAS."},{"key":"e_1_3_2_26_2","volume-title":"1st International Workshop on Microkernels for Embedded Systems","author":"Kaiser R.","year":"2007","unstructured":"R. Kaiser and S. Wagner. 2007. Evolution of the PikeOS microkernel. In 1st International Workshop on Microkernels for Embedded Systems."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1990.128748"},{"key":"e_1_3_2_29_2","volume-title":"RTSS","author":"Li Y.","year":"2014","unstructured":"Y. Li, R. West, Z. Cheng, and E. Missimer. 2014. Predictable communication and migration in the Quest-V separation kernel. In RTSS."},{"key":"e_1_3_2_30_2","volume-title":"ECRTS","author":"Mohan S.","year":"2014","unstructured":"S. Mohan, M.-K. Yoon, R. Pellizzoni, and R. Bobba. 2014. Real-time systems security through scheduler constraints. In ECRTS."},{"key":"e_1_3_2_31_2","unstructured":"Special C. of RTCA. 2011. DO-178C Software Considerations in Airborne Systems and Equipment Certification."},{"key":"e_1_3_2_32_2","article-title":"Using simplicity to control complexity","author":"Sha L.","year":"2001","unstructured":"L. Sha. 2001. Using simplicity to control complexity. IEEE Software (2001).","journal-title":"IEEE Software"},{"key":"e_1_3_2_33_2","volume-title":"Eurosys","author":"Singaravelu L.","year":"2006","unstructured":"L. Singaravelu, C. Pu, H. H\u00e4rtig, and C. Helmuth. 2006. Reducing TCB complexity for security-sensitive applications: Three case studies. In Eurosys."},{"key":"e_1_3_2_34_2","volume-title":"IEEE Euro Symposium on Security and Privacy","author":"Vasudevan A.","year":"2018","unstructured":"A. Vasudevan and S. Chaki. 2018. Have your PI and eat it too: Practical security on a low-cost ubiquitous computing platform. In IEEE Euro Symposium on Security and Privacy."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.36"},{"key":"e_1_3_2_36_2","volume-title":"25th USENIX Security Symposium (USENIX Security \u201916)","author":"Vasudevan A.","year":"2016","unstructured":"A. Vasudevan, S. Chaki, P. Maniatis, L. Jia, and A. Datta. 2016. \u00fcberSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor. In 25th USENIX Security Symposium (USENIX Security \u201916)."},{"key":"e_1_3_2_37_2","volume-title":"EMSOFT","author":"Xia S.","year":"2011","unstructured":"S. Xia, J. Wilson, C. Lu, and C. D. Gill. 2011. RT-Xen: Towards real-time hypervisor scheduling in Xen. In EMSOFT."}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3635162","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3635162","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:06Z","timestamp":1750286946000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3635162"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,22]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,1,31]]}},"alternative-id":["10.1145\/3635162"],"URL":"https:\/\/doi.org\/10.1145\/3635162","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"type":"print","value":"2378-962X"},{"type":"electronic","value":"2378-9638"}],"subject":[],"published":{"date-parts":[[2025,1,22]]},"assertion":[{"value":"2023-04-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-20","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}