{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T10:23:28Z","timestamp":1779099808799,"version":"3.51.4"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2026,1,31]]},"abstract":"<jats:p>Industrial Internet of Things (IIoT) systems require robust mechanisms for secure firmware updates. Existing approaches are often inadequate due to vendor fragmentation, network limitations, and the safety-critical nature of many IIoT applications. In this article, we address these challenges by extending the IETF SUIT (Software Updates for Internet of Things) framework to enhance the security and assurance of firmware updates. Our contributions include the integration of Software Bill of Materials (SBOM) mechanisms and a Behavioral Certification Manifest into the SUIT architecture to increase transparency and provide formal guarantees about the content of the update. The approach is validated by a prototype implementation that demonstrates its feasibility and scalability using real-world benchmarks.<\/jats:p>","DOI":"10.1145\/3754455","type":"journal-article","created":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T15:45:28Z","timestamp":1753717528000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Firmware Secure Updates Meet Formal Verification"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9748-3293","authenticated-orcid":false,"given":"Alberto","family":"Tacchella","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Trento, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-0317-0725","authenticated-orcid":false,"given":"Emanuele","family":"Beozzo","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Trento, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1252-8465","authenticated-orcid":false,"given":"Bruno","family":"Crispo","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Trento, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9483-3940","authenticated-orcid":false,"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Trento, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,21]]},"reference":[{"key":"e_1_3_4_2_2","unstructured":"Xz: Malicious Code in Distributed Source. 2024. Retrieved November 14 2024 from https:\/\/www.cve.org\/CVERecord?id=CVE-2024-3094"},{"key":"e_1_3_4_3_2","first-page":"743","volume-title":"CCC \u201916","author":"Abera Tigist","year":"2016","unstructured":"Tigist Abera, N. Asokan, Lucas Davi, Jan-Erik Ekberg, Thomas Nyman, Andrew Paverd, Ahmad-Reza Sadeghi, and Gene Tsudik. 2016. C-flat: Control-flow attestation for embedded systems software. In CCC \u201916. ACM, New York, NY, 743\u2013754."},{"key":"e_1_3_4_4_2","unstructured":"Ron Amadeo. 2022. Samsung\u2019s App-Signing Key Leaked to Sign Malware. Retrieved from https:\/\/arstechnica.com\/gadgets\/2022\/12\/samsungs-android-app-signing-key-has-leaked-is-being-used-to-sign-malware\/"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2858422"},{"key":"e_1_3_4_6_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"TACAS (1)","author":"Barbosa Haniel","year":"2022","unstructured":"Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, et al. 2022. cvc5: A versatile and industrial-strength SMT solver. In TACAS (1). Dana Fisman and Grigore Rosu (Eds.), Lecture Notes in Computer Science, Vol. 13243, Springer, 415\u2013442."},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3587692"},{"key":"e_1_3_4_8_2","first-page":"1267","volume-title":"Handbook of Satisfiability","author":"Barrett Clark W.","year":"2021","unstructured":"Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2021. Satisfiability modulo theories. In Handbook of Satisfiability. Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh (Eds.), IOS Press, 1267\u20131329."},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2220336.2220346"},{"key":"e_1_3_4_10_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/978-3-031-30122-3_25","volume-title":"Foundations and Practice of Security","author":"Bradley Conner","year":"2023","unstructured":"Conner Bradley and David Barrera. 2023. Towards characterizing IoT software update practices. In Foundations and Practice of Security. Guy-Vincent Jourdan, Laurent Mounier, Carlisle Adams, Florence S\u00e8des, and Joaquin Garcia-Alfaro (Eds.), Vol. 13877, Lecture Notes in Computer Science, Cham, 406\u2013422."},{"key":"e_1_3_4_11_2","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1109\/APCC.2016.7581459","volume-title":"2016 22nd Asia-Pacific Conference on Communications (APCC)","author":"Chandra Hans","year":"2016","unstructured":"Hans Chandra, Erwin Anggadjaja, Pranata Setya Wijaya, and Edy Gunawan. 2016. Internet of things: Over-the-air (OTA) firmware update in lightweight mesh network protocol for smart urban development. In 2016 22nd Asia-Pacific Conference on Communications (APCC), 115\u2013118."},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_4_13_2","unstructured":"Gareth Corfield. 2022. Leaked stolen Nvidia key can sign Windows malware. Retrieved from https:\/\/www.theregister.com\/2022\/03\/05\/nvidia_stolen_certificate\/"},{"key":"e_1_3_4_14_2","first-page":"238","volume-title":"Conference Record of the 4th ACM Symposium on Principles of Programming Languages","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages. ACM, 238\u2013252."},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3579856.3590329"},{"key":"e_1_3_4_16_2","first-page":"223","volume-title":"Proceedings of the 13th IFIP WG 11.2 International Conference on Information Security Theory and Practice (WISTP \u201919)","volume":"12024","author":"Dejon Nicolas","year":"2019","unstructured":"Nicolas Dejon, Davide Caputo, Luca Verderame, Alessandro Armando, and Alessio Merlo. 2019. Automated security analysis of IoT software updates. In Proceedings of the 13th IFIP WG 11.2 International Conference on Information Security Theory and Practice (WISTP \u201919). Maryline Laurent and Thanassis Giannetsos (Eds.), Lecture Notes in Computer Science, Vol. 12024, Springer, 223\u2013239."},{"key":"e_1_3_4_17_2","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1109\/LCN.Workshops.2017.78","volume-title":"2017 IEEE 42nd Conference on Local Computer Networks Workshops (LCN Workshops)","author":"Doddapaneni Krishna","year":"2017","unstructured":"Krishna Doddapaneni, Ravi Lakkundi, Suhas Rao, Sujay Gururaj Kulkarni, and Bhargav Bhat. 2017. Secure FoTA object for IoT. In 2017 IEEE 42nd Conference on Local Computer Networks Workshops (LCN Workshops), 154\u2013159."},{"issue":"7","key":"e_1_3_4_18_2","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","article-title":"A survey of automated techniques for formal software verification","volume":"27","author":"D'Silva Vijay","unstructured":"Vijay D'Silva, Daniel Kroening, and Georg Weissenbacher. A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 27, 7 (Jul. 2008), 1165\u20131178.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2022.3163969"},{"key":"e_1_3_4_20_2","doi-asserted-by":"crossref","first-page":"100508","DOI":"10.1016\/j.iot.2022.100508","article-title":"Secure firmware over-the-air updates for IoT: Survey, challenges, and discussions","volume":"18","author":"Jaouhari S. El","year":"2022","unstructured":"S. El Jaouhari and E. Bouvet. 2022. Secure firmware over-the-air updates for IoT: Survey, challenges, and discussions. Internet of Things 18 (2022), 100508.","journal-title":"Internet of Things"},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3480462"},{"key":"e_1_3_4_22_2","unstructured":"Dan Goodin. 2023. Leak of MSI UEFI signing keys stokes fears of \u201cdoomsday\u201d supply chain attack. Retrieved from http:\/\/arstechnica.com\/information-technology\/2023\/05\/leak-of-msi-uefi-signing-keys-stokes-concerns-of-doomsday-supply-chain-attack\/"},{"key":"e_1_3_4_23_2","unstructured":"U.S. Federal Government. 2021. Improving the Nation\u2019s Cybersecurity. Retrieved November 14 2024 from https:\/\/www.federalregister.gov\/documents\/2021\/05\/17\/2021-10460\/improving-the-nations-cybersecurity"},{"issue":"3","key":"e_1_3_4_24_2","article-title":"Flashadow: A flash-based shadow stack for low-end embedded systems","volume":"5","author":"Grisafi Michele","year":"2024","unstructured":"Michele Grisafi, Mahmoud Ammar, Marco Roveri, and Bruno Crispo. 2024. Flashadow: A flash-based shadow stack for low-end embedded systems. ACM Transactions on Internet of Things 5, 3 (Aug. 2024), 19:1\u201319:29.","journal-title":"ACM Transactions on Internet of Things"},{"key":"e_1_3_4_25_2","first-page":"20","volume-title":"F-IDE@FM","author":"Healy Andrew","year":"2016","unstructured":"Andrew Healy, Rosemary Monahan, and James F. Power. 2016. Predicting SMT solver performance for software verification. In F-IDE@FM, 20\u201337."},{"key":"e_1_3_4_26_2","first-page":"1","volume-title":"International Conference on Embedded Security in Car","author":"Karthik Trishank","year":"2016","unstructured":"Trishank Karthik, Akan Brown, Sebastien Awwad, Damon McCoy, Russ Bielawski, Cameron Mott, Sam Lauzon, Andr\u00e9 Weimerskirch, and Justin Cappos. 2016. Uptane: Securing software updates for automobiles. In International Conference on Embedded Security in Car, 1\u201311."},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_4_28_2","doi-asserted-by":"crossref","first-page":"2101","DOI":"10.1109\/ICDCS.2019.00207","volume-title":"2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS)","author":"Langiu Antonio","year":"2019","unstructured":"Antonio Langiu, Carlo Alberto Boano, Markus Schu\u00df, and Kay R\u00f6mer. 2019. UpKit: An open-source, portable, and lightweight update framework for constrained IoT devices. In 2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS), 2101\u20132112."},{"key":"e_1_3_4_29_2","first-page":"1","volume-title":"Workshop on Next Generation Real-Time Embedded Systems (NG-RES \u201920)","author":"Martins Jos\u00e9","year":"2020","unstructured":"Jos\u00e9 Martins, Adriano Tavares, Marco Solieri, Marko Bertogna, and Sandro Pinto. 2020. Bao: A lightweight static partitioning hypervisor for modern multi-core embedded systems. In Workshop on Next Generation Real-Time Embedded Systems (NG-RES \u201920), 1\u201314."},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3297280.3297299"},{"key":"e_1_3_4_31_2","article-title":"A manifest information model for firmware updates in internet of things (IoT) devices","volume":"9124","author":"Moran Brendan","year":"2022","unstructured":"Brendan Moran, Hannes Tschofenig, and Henk Birkholz. 2022. A manifest information model for firmware updates in internet of things (IoT) devices. RFC 9124.","journal-title":"RFC"},{"key":"e_1_3_4_32_2","article-title":"A concise binary object representation (CBOR)-based serialization format for the software updates for internet of things (SUIT) manifest","author":"Moran Brendan","unstructured":"Brendan Moran, Hannes Tschofenig, Henk Birkholz, Koen Zandberg, and \u00d8yvind R\u00f8nningstad. 2024. A concise binary object representation (CBOR)-based serialization format for the software updates for internet of things (SUIT) manifest. Internet-Draft Draft-Ietf-Suit-Manifest-34, Internet Engineering Task Force. Retrieved from https:\/\/datatracker.ietf.org\/doc\/draft-ietf-suit-manifest\/","journal-title":"Internet-Draft Draft-Ietf-Suit-Manifest-34, Internet Engineering Task Force"},{"key":"e_1_3_4_33_2","article-title":"A firmware update architecture for internet of things","volume":"9019","author":"Moran Brendan","year":"2021","unstructured":"Brendan Moran, Hannes Tschofenig, David Brown, and Milosch Meriac. 2021. A firmware update architecture for internet of things. RFC 9019.","journal-title":"RFC"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_4_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/277652.277752"},{"key":"e_1_3_4_36_2","unstructured":"European Parliament. 2024. Cyber Resilience Act. Retrieved November 14 2024 from https:\/\/www.europarl.europa.eu\/doceo\/document\/TA-9-2024-0130_EN.html"},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_3_4_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.03.023"},{"key":"e_1_3_4_39_2","doi-asserted-by":"publisher","unstructured":"Rustam Sadykov Azat Abdullin and Marat Akhin. 2025. Cache-a-lot: Pushing the limits of unsatisfiable core reuse in SMT-based program analysis. DOI: 10.48550\/ARXIV.2504.07642","DOI":"10.48550\/ARXIV.2504.07642"},{"key":"e_1_3_4_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866315"},{"key":"e_1_3_4_41_2","first-page":"85","volume-title":"Proceedings of the 2006 ACM Workshop on Wireless Security","author":"Seshadri Arvind","year":"2006","unstructured":"Arvind Seshadri, Mark Luk, Adrian Perrig, Leendert van Doorn, and Pradeep K. Khosla. 2006. SCUBA: Secure code update by attestation in sensor networks. In Proceedings of the 2006 ACM Workshop on Wireless Security. ACM, 85\u201394."},{"key":"e_1_3_4_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2018.1700621"},{"key":"e_1_3_4_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2919760"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3754455","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T09:08:23Z","timestamp":1768986503000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3754455"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,21]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1,31]]}},"alternative-id":["10.1145\/3754455"],"URL":"https:\/\/doi.org\/10.1145\/3754455","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,21]]},"assertion":[{"value":"2024-11-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-07-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}