{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:14:53Z","timestamp":1761920093140,"version":"build-2065373602"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"name":"ANR","award":["ANR-22-CE39-0014, ANR-22-CE25-0018, ANR-24-ASM2-0001"],"award-info":[{"award-number":["ANR-22-CE39-0014, ANR-22-CE25-0018, ANR-24-ASM2-0001"]}]},{"DOI":"10.13039\/501100005900","name":"French Ministry of Defense","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005900","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>\n                    The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack (TSS). The open-source library\n                    <jats:italic toggle=\"yes\">tpm2-tss<\/jats:italic>\n                    is a popular implementation of the TSS. Vulnerabilities in its code could allow attackers to recover sensitive information and take control of the system. This article presents a case study on formal verification of tpm2-tss using the\n                    <jats:sc>Frama-C<\/jats:sc>\n                    verification platform. Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool. We present several difficulties and tool limitations we faced, illustrate them with examples and describe solutions that allowed us to verify functional properties and the absence of runtime errors for a representative subset of functions. In particular, their verification required several lemmas proved in the interactive proof assistant\n                    <jats:sc>Coq<\/jats:sc>\n                    . We describe our verification results and desired tool improvements necessary to achieve a full formal verification of the target code.\n                  <\/jats:p>","DOI":"10.1145\/3743153","type":"journal-article","created":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T07:42:29Z","timestamp":1750405349000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-8540-1273","authenticated-orcid":false,"given":"Yani","family":"Ziani","sequence":"first","affiliation":[{"name":"Thales Research and Technology","place":["Palaiseau, France"]},{"name":"LIFO EA 4022, Univ. Orl\u00e9ans, INSA Centre Val de Loire","place":["Palaiseau, France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4834-7126","authenticated-orcid":false,"given":"T\u00e9o","family":"Bernier","sequence":"additional","affiliation":[{"name":"Thales Research and Technology","place":["Palaiseau, France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-2813","authenticated-orcid":false,"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[{"name":"Thales Research and Technology","place":["Palaiseau, France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9301-7829","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"additional","affiliation":[{"name":"LIFO EA 4022, Univ. Orl\u00e9ans, INSA Centre Val de Loire","place":["Orleans, France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5364-8244","authenticated-orcid":false,"given":"Daniel","family":"Gracia P\u00e9rez","sequence":"additional","affiliation":[{"name":"Thales Research and Technology","place":["Palaiseau, France"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,31]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12154-3_4"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_3_4_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4302-6584-9","volume-title":"A Practical Guide to TPM 2.0: Using the Trusted Platform Module in the New Age of Security (1st. ed.)","author":"Arthur Will","year":"2015","unstructured":"Will Arthur and David Challener. 2015. A Practical Guide to TPM 2.0: Using the Trusted Platform Module in the New Age of Security (1st. ed.). Apress, USA."},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"volume-title":"ACSL: ANSI\/ISO C Specification Language","author":"Baudin Patrick","key":"e_1_3_3_6_2","unstructured":"Patrick Baudin, Pascal Cuoq, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, Benjamin Monate, Yannick Moy, and Virgile Prevosto. [n. d.]. ACSL: ANSI\/ISO C Specification Language. Retrieved from http:\/\/frama-c.com\/acsl.html"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57259-3_14"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","unstructured":"Alex Le Blanc and Patrick Lam. 2024. Surveying the rust verification landscape. 10.48550\/arXiv.2410.01981","DOI":"10.48550\/arXiv.2410.01981"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3297280.3297495"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_6"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_9"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"e_1_3_3_14_2","unstructured":"Nathan Chong and Bart Jacobs. 2021. Formally verifying FreeRTOS\u2019 interprocess communication mechanism. (2021). Retrieved June 16 2025 from https:\/\/www.amazon.science\/publications\/formally-verifying-freertos-interprocess-communication-mechanism"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-76554-4_3"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/SecDev51306.2021.00028"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57246-3_18"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_16"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_16"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_9"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_23"},{"key":"e_1_3_3_24_2","volume-title":"Proceedings of the 11th European Congress on Embedded Real-Time Systems.","author":"Djoudi Adel","year":"2022","unstructured":"Adel Djoudi, Martin H\u00e1na, Nikolai Kosmatov, Milan K\u0159\u00ed\u017eeneck\u00fd, Franck Ohayon, Patricia Mouy, Arnaud Fontaine, and David F\u00e9liot. 2022. A bottom-up formal verification approach for common criteria certification: Application to JavaCard virtual machine. In Proceedings of the 11th European Congress on Embedded Real-Time Systems. Retrieved from https:\/\/hal.science\/hal-03704287"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.187.3"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_11"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_5"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/LCN.2004.38"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0419-0"},{"key":"e_1_3_3_31_2","volume-title":"Prusti in Practice","author":"Gijsberts Stef","year":"2023","unstructured":"Stef Gijsberts. 2023. Prusti in Practice. Master\u2019s thesis. Radboud University."},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.02.005"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"e_1_3_3_34_2","volume-title":"The Verifast Program Verifier","author":"Jacobs Bart","year":"2008","unstructured":"Bart Jacobs and Frank Piessens. 2008. The Verifast Program Verifier. Technical Report CW-520. KU Leuven."},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-55608-1"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.149.2"},{"key":"e_1_3_3_41_2","volume-title":"Program Proofs","author":"Leino Rustan K.","year":"2024","unstructured":"Rustan K. Leino. 2024. Program Proofs. MIT Press."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-54876-0_9"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139629294"},{"key":"e_1_3_3_44_2","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Proceedings of the 17th 17th International Conference on Verification, Model Checking, and Abstract Interpretation.","volume":"9583","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A verification infrastructure for permission-based reasoning. In Proceedings of the 17th 17th International Conference on Verification, Model Checking, and Abstract Interpretation.LNCS, Vol. 9583, Springer, 41\u201362."},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54994-7_22"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34968-4_23"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_9"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0435-1"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1049\/iet-ifs.2016.0005"},{"key":"e_1_3_3_50_2","volume-title":"CreuSAT-Using Rust and Creusot to Create the World\u2019s Fastest Deductively Verified SAT Solver","author":"Skot\u00e5m Sarek H\u00f8verstad","year":"2022","unstructured":"Sarek H\u00f8verstad Skot\u00e5m. 2022. CreuSAT-Using Rust and Creusot to Create the World\u2019s Fastest Deductively Verified SAT Solver. Master\u2019s thesis."},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_10"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50521-8_9"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-47705-8_8"},{"key":"e_1_3_3_54_2","unstructured":"The Coq Development Team. [n. d.]. The Coq Proof Assistant. Retrieved June 16 2025 from http:\/\/coq.inria.fr"},{"key":"e_1_3_3_55_2","unstructured":"Trusted Computing Group. 2019. Trusted Platform Module Library Specification Family \u201c2.0\u201d Level 00 Revision 01.59 \u2013 November. Retrieved from https:\/\/trustedcomputinggroup.org\/work-groups\/trusted-platform-module\/last accessed: May 2023."},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50011-9_33"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","unstructured":"Qianying Zhang and Shijun Zhao. 2020. A comprehensive formal security analysis and revision of the two-phase key exchange primitive of TPM 2.0. Computer Networks 179 (2020) 107369. DOI:10.1016\/j","DOI":"10.1016\/j"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-47705-8_6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3743153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:07:31Z","timestamp":1761919651000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3743153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,31]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3743153"],"URL":"https:\/\/doi.org\/10.1145\/3743153","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,10,31]]},"assertion":[{"value":"2024-09-07","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}