{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T18:32:36Z","timestamp":1771957956490,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"French National Research Agency","award":["ANR-22-PECY-0004"],"award-info":[{"award-number":["ANR-22-PECY-0004"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705880","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"140-155","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formally Verified Hardening of C Programs against Hardware Fault Injection"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3575-7770","authenticated-orcid":false,"given":"Basile","family":"Pesin","sequence":"first","affiliation":[{"name":"Ecole Nationale de l'Aviation Civile, Toulouse, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9501-9606","authenticated-orcid":false,"given":"Sylvain","family":"Boulm\u00e9","sequence":"additional","affiliation":[{"name":"University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, Grenoble, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7671-6126","authenticated-orcid":false,"given":"David","family":"Monniaux","sequence":"additional","affiliation":[{"name":"University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, Grenoble, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7070-6290","authenticated-orcid":false,"given":"Marie-Laure","family":"Potet","sequence":"additional","affiliation":[{"name":"University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, Grenoble, France"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_9"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460860"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243745"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-024-00352-6"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2005.862424"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858930.2858931"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00029"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","unstructured":"Nicolas Belleville Karine Heydemann Damien Courouss\u00e9 Thierno Barry Bruno Robisson Abderrahmane Seriai and Henri-Pierre Charles. 2018. Automatic Application of Software Countermeasures Against Physical Attacks. Cham. isbn:978-3-319-98935-8 https:\/\/doi.org\/10.1007\/978-3-319-98935-8_7 10.1007\/978-3-319-98935-8_7","DOI":"10.1007\/978-3-319-98935-8_7"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","unstructured":"Pascal Berthom\u00e9 Karine Heydemann Xavier Kauffmann-Tourkestansky and J. Lalande. 2012. High Level Model of Control Flow Attacks for Smart Card Functional Security. In ARES \u201912. isbn:978-1-4673-2244-7 https:\/\/doi.org\/10.1109\/ARES.2012.79 10.1109\/ARES.2012.79","DOI":"10.1109\/ARES.2012.79"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_3_2_2_14_1","volume-title":"Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC) 23","author":"Boespflug Etienne","year":"2023","unstructured":"Etienne Boespflug, Abderrahmane Bouguern, Laurent Mounier, and Marie-Laure Potet. 2023. A tool assisted methodology to harden programs against multi-faults injections. In Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC) 23."},{"key":"e_1_3_2_2_15_1","volume-title":"Lipton","author":"Boneh Dan","year":"1997","unstructured":"Dan Boneh, Richard A. DeMillo, and Richard J. Lipton. 1997. On the Importance of Checking Cryptographic Protocols for Faults. In Advances in Cryptology \u2014 EUROCRYPT \u201997. Berlin, Heidelberg. isbn:978-3-540-69053-5"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455776"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3054924"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-013-0049-3"},{"key":"e_1_3_2_2_19_1","unstructured":"Coq Development Team. 2020. The Coq proof assistant reference manual. https:\/\/coq.inria.fr\/distrib\/current\/refman\/"},{"key":"e_1_3_2_2_20_1","volume-title":"Picon: Control Flow Integrity on LLVM IR. In SSTIC. https:\/\/www.sstic.org\/2015\/presentation\/control_flow_integrity_on_llvm_ir\/","author":"Coudray Thomas","year":"2015","unstructured":"Thomas Coudray, Arnaud Fontaine, and Pierre Chifflier. 2015. Picon: Control Flow Integrity on LLVM IR. In SSTIC. https:\/\/www.sstic.org\/2015\/presentation\/control_flow_integrity_on_llvm_ir\/"},{"key":"e_1_3_2_2_21_1","volume-title":"ProSpeCT: Provably Secure Speculation for the Constant-Time Policy. In 32nd USENIX Security Symposium, USENIX Security 2023","author":"Daniel Lesly-Ann","year":"2023","unstructured":"Lesly-Ann Daniel, Marton Bognar, Job Noorman, S\u00e9bastien Bardin, Tamara Rezk, and Frank Piessens. 2023. ProSpeCT: Provably Secure Speculation for the Constant-Time Policy. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/daniel"},{"key":"e_1_3_2_2_22_1","volume-title":"meeting. https:\/\/llvm.org\/devmtg\/2019-04","author":"de Ferri\u00e8re Fran\u00e7ois","year":"2019","unstructured":"Fran\u00e7ois de Ferri\u00e8re. 2019. A compiler approach to Cyber-Security. 2019 European LLVM developers\u2019 meeting. https:\/\/llvm.org\/devmtg\/2019-04"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-31271-2_7"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3566097.3567925"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3407023.3407049"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622799"},{"key":"e_1_3_2_2_27_1","volume-title":"Formally verified software countermeasures for control-flow integrity of smart card C code. Computers & Security, 85","author":"Heydemann Karine","year":"2019","unstructured":"Karine Heydemann, Jean-Fran\u00e7ois Lalande, and Pascal Berthom\u00e9. 2019. Formally verified software countermeasures for control-flow integrity of smart card C code. Computers & Security, 85 (2019)."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2018.00097"},{"key":"e_1_3_2_2_30_1","volume-title":"Formal verification of a realistic compiler. Commun. ACM, 52, 7","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), HAL:inria-00415861."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477314.3507341"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3640537.3641570"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636952"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38828-6_3"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3436809"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2014.34"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3141234"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-013-0065-3"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2005.34"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD51259.2020.00048"},{"key":"e_1_3_2_2_43_1","volume-title":"Control-flow integrity: attacks and protections. Applied Sciences, 9, 20","author":"Sayeed Sarwar","year":"2019","unstructured":"Sarwar Sayeed, Hector Marco-Gisbert, Ismael Ripoll, and Miriam Birch. 2019. Control-flow integrity: attacks and protections. Applied Sciences, 9, 20 (2019)."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806611"},{"key":"e_1_3_2_2_45_1","volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe (DATE \u201913)","author":"Nikolaus Thei\u00df","year":"2013","unstructured":"Nikolaus Thei\u00df ing, Dominik Merli, Michael Smola, Frederic Stumpf, and Georg Sigl. 2013. Comprehensive analysis of software countermeasures against fault attacks. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE \u201913). San Jose, CA, USA. isbn:9781450321532"},{"key":"e_1_3_2_2_46_1","volume-title":"A\u00efna Linn Georges, Catalin Hritcu, and Andrew Tolmach.","author":"Thibault J\u00e9r\u00e9my","year":"2024","unstructured":"J\u00e9r\u00e9my Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, A\u00efna Linn Georges, Catalin Hritcu, and Andrew Tolmach. 2024. SECOMP: Formally Secure Compilation of Compartmentalized C Programs. arxiv:2401.16277"},{"key":"e_1_3_2_2_47_1","unstructured":"Simon Tollec. 2024. Formal Verification of Processor Microarchitecture to Analyze System Security against Fault Attacks. Ph. D. Dissertation. Universit\u00e9 Paris-Saclay."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/FDTC57191.2022.00017"},{"key":"e_1_3_2_2_49_1","volume-title":"Sixth workshop on Principles of Secure Compilation (PriSC\u201922)","author":"Torrini Paolo","year":"2022","unstructured":"Paolo Torrini and Sylvain Boulm\u00e9. 2022. A CompCert Backend with Symbolic Encryption. In Sixth workshop on Principles of Secure Compilation (PriSC\u201922), part of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022). Philadelphia, Pennsylvania, United States. https:\/\/hal.science\/hal-03555551"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2018.2860010"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377555.3377897"},{"key":"e_1_3_2_2_52_1","volume-title":"Proceedings of the NATO Advanced Study Institute on Program Design Calculi","author":"Wadler Philip","year":"1992","unstructured":"Philip Wadler. 1992. Monads for functional programming. In Program Design Calculi, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28 - August 9, 1992 (NATO ASI Series, Vol. 118). https:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/marktoberdorf\/baastad.pdf"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632914"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Denver CO USA","acronym":"CPP '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"]},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705880","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705880","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705880"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":54,"alternative-id":["10.1145\/3703595.3705880","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705880","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}