{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T06:07:23Z","timestamp":1780466843747,"version":"3.54.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031928819","type":"print"},{"value":"9783031928826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-92882-6_11","type":"book-chapter","created":{"date-parts":[[2025,5,15]],"date-time":"2025-05-15T14:33:58Z","timestamp":1747319638000},"page":"151-165","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Certified Secure Updates for IoT Devices"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9748-3293","authenticated-orcid":false,"given":"Alberto","family":"Tacchella","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-0317-0725","authenticated-orcid":false,"given":"Emanuele","family":"Beozzo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1252-8465","authenticated-orcid":false,"given":"Bruno","family":"Crispo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9483-3940","authenticated-orcid":false,"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,16]]},"reference":[{"issue":"11","key":"11_CR1","doi-asserted-by":"publisher","first-page":"2290","DOI":"10.1109\/TCAD.2018.2858422","volume":"37","author":"N Asokan","year":"2018","unstructured":"Asokan, N., Nyman, T., Rattanavipanon, N., Sadeghi, A.R., Tsudik, G.: ASSURED: architecture for secure software update of realistic embedded devices. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11), 2290\u20132300 (2018). https:\/\/doi.org\/10.1109\/TCAD.2018.2858422","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: CVC5: a versatile and industrial-strength SMT solver. Presented at the (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"issue":"10","key":"11_CR3","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3587692","volume":"66","author":"H Barbosa","year":"2023","unstructured":"Barbosa, H., et al.: Generating and exploiting automated reasoning proof certificates. Commun. ACM 66(10), 86\u201395 (2023). https:\/\/doi.org\/10.1145\/3587692","journal-title":"Commun. ACM"},{"key":"11_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1267\u20131329. IOS Press (2021)","DOI":"10.3233\/FAIA201017"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Blech, J.O., P\u00e9rin, M.: Generating invariant-based certificates for embedded systems. ACM Trans. Embed. Comput. Syst. 11(2), 34:1\u201334:22 (2012). https:\/\/doi.org\/10.1145\/2220336.2220346","DOI":"10.1145\/2220336.2220346"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Bradley, C., Barrera, D.: Towards characterizing IoT software update practices. In: Jourdan, G.V., et.al (eds.) Foundations and Practice of Security, pp. 406\u2013422. LNCS, Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30122-3_25","DOI":"10.1007\/978-3-031-30122-3_25"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Chandra, H., Anggadjaja, E., Wijaya, P.S., Gunawan, E.: 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), pp. 115\u2013118 (August 2016). https:\/\/doi.org\/10.1109\/APCC.2016.7581459","DOI":"10.1109\/APCC.2016.7581459"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Dejon, N., Caputo, D., Verderame, L., Armando, A., Merlo, A.: Automated security analysis of IoT software updates. In: Laurent, M., Giannetsos, T. (eds.) Information Security Theory and Practice - 13th IFIP WG 11.2 International Conference, Paris, France. LNCS, vol. 12024, pp. 223\u2013239. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-41702-4_14","DOI":"10.1007\/978-3-030-41702-4_14"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Doddapaneni, K., Lakkundi, R., Rao, S., Kulkarni, S.G., Bhat, B.: Secure FoTA object for IoT. In: 2017 IEEE 42nd Conference on Local Computer Networks Workshops (LCN Workshops), pp. 154\u2013159 (October 2017). https:\/\/doi.org\/10.1109\/LCN.Workshops.2017.78","DOI":"10.1109\/LCN.Workshops.2017.78"},{"issue":"7","key":"11_CR11","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165\u20131178 (2008). https:\/\/doi.org\/10.1109\/TCAD.2008.923410","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"11_CR12","doi-asserted-by":"publisher","DOI":"10.1016\/j.iot.2022.100508","volume":"18","author":"S El Jaouhari","year":"2022","unstructured":"El Jaouhari, S., Bouvet, E.: Secure firmware over-the-air updates for IoT: survey, challenges, and discussions. Internet Things 18, 100508 (2022). https:\/\/doi.org\/10.1016\/j.iot.2022.100508","journal-title":"Internet Things"},{"issue":"19","key":"11_CR13","doi-asserted-by":"publisher","first-page":"4121","DOI":"10.3390\/S19194121","volume":"19","author":"A Giaretta","year":"2019","unstructured":"Giaretta, A., Dragoni, N., Massacci, F.: IoT security configurability with security-by-contract. Sensors 19(19), 4121 (2019). https:\/\/doi.org\/10.3390\/S19194121","journal-title":"Sensors"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Giaretta, A., Dragoni, N., Massacci, F.: S$$\\times $$C4IoT: a security-by-contract framework for dynamic evolving IoT devices. ACM Trans. Sens. Netw. 18(1), 12:1\u201312:51 (2022). https:\/\/doi.org\/10.1145\/3480462","DOI":"10.1145\/3480462"},{"issue":"2","key":"11_CR15","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/S10703-021-00369-1","volume":"57","author":"A Griggio","year":"2021","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for SAT-based model checking. Form. Methods Syst. Des. 57(2), 178\u2013210 (2021). https:\/\/doi.org\/10.1007\/S10703-021-00369-1","journal-title":"Form. Methods Syst. Des."},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Kolehmainen, A.: Secure firmware updates for IoT: a survey. In: IEEE International Conference on iThings and IEEE GreenCom and IEEE CPSCom and IEEE SmartData, Halifax, NS, Canada, pp. 112\u2013117. IEEE (2018). https:\/\/doi.org\/10.1109\/CYBERMATICS_2018.2018.00051","DOI":"10.1109\/CYBERMATICS_2018.2018.00051"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Langiu, A., Boano, C.A., Schu\u00df, M., R\u00f6mer, K.: UpKit: an open-source, portable, and lightweight update framework for constrained IoT devices. In: 2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS), pp. 2101\u20132112 (July 2019)","DOI":"10.1109\/ICDCS.2019.00207"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Moran, B., Tschofenig, H., Birkholz, H.: A Manifest Information Model for Firmware Updates in Internet of Things (IoT) Devices. RFC 9124 (January 2022)","DOI":"10.17487\/RFC9124"},{"key":"11_CR19","unstructured":"Moran, B., Tschofenig, H., Birkholz, H., Zandberg, K., R\u00f8nningstad, O.: 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-25, Internet Engineering Task Force (February 2024). https:\/\/datatracker.ietf.org\/doc\/draft-ietf-suit-manifest\/25\/, work in progress"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Moran, B., Tschofenig, H., Brown, D., Meriac, M.: A Firmware Update Architecture for Internet of Things. RFC 9019 (April 2021)","DOI":"10.17487\/RFC9019"},{"issue":"5","key":"11_CR21","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/277652.277752","volume":"33","author":"GC Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. SIGPLAN Not. 33(5), 333\u2013344 (1998). https:\/\/doi.org\/10.1145\/277652.277752","journal-title":"SIGPLAN Not."},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106\u2013119. POPL \u201997, Association for Computing Machinery, New York, NY, USA (January 1997). https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"11_CR23","unstructured":"Parliament, E.: Cyber resilience act (March 2024). https:\/\/www.europarl.europa.eu\/doceo\/document\/TA-9-2024-0130_EN.html. Accessed 14 Nov 2024"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Samuel, J., Mathewson, N., Cappos, J., Dingledine, R.: Survivable key compromise in software update systems. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 61\u201372. CCS \u201910, Association for Computing Machinery, New York, NY, USA (October 2010). https:\/\/doi.org\/10.1145\/1866307.1866315","DOI":"10.1145\/1866307.1866315"},{"key":"11_CR25","doi-asserted-by":"publisher","first-page":"71907","DOI":"10.1109\/ACCESS.2019.2919760","volume":"7","author":"K Zandberg","year":"2019","unstructured":"Zandberg, K., Schleiser, K., Padilla, F.A., Tschofenig, H., Baccelli, E.: Secure firmware updates for constrained IoT devices using open standards: a reality check. IEEE Access 7, 71907\u201371920 (2019). https:\/\/doi.org\/10.1109\/ACCESS.2019.2919760","journal-title":"IEEE Access"}],"container-title":["IFIP Advances in Information and Communication Technology","ICT Systems Security and Privacy Protection"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-92882-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,15]],"date-time":"2025-05-15T14:34:03Z","timestamp":1747319643000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-92882-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031928819","9783031928826"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-92882-6_11","relation":{},"ISSN":["1868-4238","1868-422X"],"issn-type":[{"value":"1868-4238","type":"print"},{"value":"1868-422X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"16 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors declare that they have no competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"SEC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"IFIP International Conference on ICT Systems Security and Privacy Protection","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Maribor","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Slovenia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"40","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sec2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sec2025.um.si\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}