{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T18:02:30Z","timestamp":1745172150891,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131875"},{"type":"electronic","value":"9783031131882"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Most methods of data transmission and storage are prone to errors, leading to data loss. Forward erasure correction (FEC) is a method to allow data to be recovered in the presence of errors by encoding the data with redundant parity information determined by an error-correcting code. There are dozens of classes of such codes, many based on sophisticated mathematics, making them difficult to verify using automated tools. In this paper, we present a formal, machine-checked proof of a C implementation of FEC based on Reed-Solomon coding. The C code has been actively used in network defenses for over 25 years, but the algorithm it implements was partially unpublished, and it uses certain optimizations whose correctness was unknown even to the code\u2019s authors. We use Coq\u2019s Mathematical Components library to prove the algorithm\u2019s correctness and the Verified Software Toolchain to prove that the C program correctly implements this algorithm, connecting both using a modular, well-encapsulated structure that could easily be used to verify a high-speed, hardware version of this FEC. This is the first end-to-end, formal proof of a real-world FEC implementation; we verified all previously unknown optimizations and found a latent bug in the code.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_14","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"272-292","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified Erasure Correction in\u00a0Coq with\u00a0MathComp and\u00a0VST"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9555-8781","authenticated-orcid":false,"given":"Joshua M.","family":"Cohen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6486-3409","authenticated-orcid":false,"given":"Qinshi","family":"Wang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-22102-1_2","volume-title":"Interactive Theorem Proving","author":"R Affeldt","year":"2015","unstructured":"Affeldt, R., Garrigue, J.: Formalization of error-correcting codes: from Hamming to modern coding theory. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 17\u201333. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_2"},{"key":"14_CR2","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. In: 2016 International Symposium on Information Theory and Its Applications (ISITA), pp. 532\u2013536 (2016)"},{"issue":"6","key":"14_CR3","doi-asserted-by":"publisher","first-page":"1123","DOI":"10.1007\/s10817-019-09538-8","volume":"64","author":"R Affeldt","year":"2020","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: A library for formalization of linear error-correcting codes. J. Autom. Reason. 64(6), 1123\u20131164 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09538-8","journal-title":"J. Autom. Reason."},{"issue":"2","key":"14_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2701415","volume":"37","author":"AW Appel","year":"2015","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 1\u201331 (2015). https:\/\/doi.org\/10.1145\/2701415","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"14_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/11442","volume":"13","author":"AW Appel","year":"2020","unstructured":"Appel, A.W., Bertot, Y.: C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1), 1\u201316 (2020). https:\/\/doi.org\/10.6092\/issn.1972-5787\/11442","journal-title":"J. Formaliz. Reason."},{"key":"14_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Bourgeat, T., Pit-Claudel, C., Chlipala, A.: The essence of Bluespec: a core language for rule-based hardware design. In: PLDI\u201920: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 243\u2013257 (2020)","DOI":"10.1145\/3385412.3385965"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Devarajegowda, K., Servadei, L., Han, Z., Werner, M., Ecker, W.: Formal verification methodology in an industrial setup. In: 2019 22nd Euromicro Conference on Digital System Design (DSD), pp. 610\u2013614 (2019). https:\/\/doi.org\/10.1109\/DSD.2019.00094","DOI":"10.1109\/DSD.2019.00094"},{"key":"14_CR9","unstructured":"Dobrescu, M., Argyraki, K.: Software dataplane verification. In: 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14), pp. 101\u2013114. USENIX Association, Seattle, April 2014"},{"key":"14_CR10","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2015). https:\/\/hal.inria.fr\/inria-00258384"},{"key":"14_CR11","unstructured":"Hagiwara, M., Nakano, K., Kong, J.: Formalization of coding theory using lean. In: 2016 International Symposium on Information Theory and Its Applications (ISITA), pp. 522\u2013526 (2016)"},{"key":"14_CR12","unstructured":"ISO: ISO\/IEC 9899:2011 Information technology \u2013 Programming languages \u2013 C, December 2011. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1548.pdf"},{"key":"14_CR13","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier (2008)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Kong, J., Webb, D.J., Hagiwara, M.: Formalization of insertion\/deletion codes and the Levenshtein metric in lean. In: 2018 International Symposium on Information Theory and Its Applications (ISITA), pp. 11\u201315 (2018)","DOI":"10.23919\/ISITA.2018.8664354"},{"issue":"7","key":"14_CR15","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"14_CR16","unstructured":"Lvov, A., Lastras-Monta\u00f1o, L.A., Paruthi, V., Shadowen, R., El-Zein, A.: Formal verification of error correcting circuits using computational algebraic geometry. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 141\u2013148 (2012)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-030-44914-8_16","volume-title":"Programming Languages and Systems","author":"W Mansky","year":"2020","unstructured":"Mansky, W., Honor\u00e9, W., Appel, A.W.: Connecting higher-order separation logic to a first-order outside world. In: ESOP 2020. LNCS, vol. 12075, pp. 428\u2013455. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_16"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"McAuley, A.J.: Reliable broadband communication using a burst erasure correcting code. In: Proceedings of the ACM Symposium on Communications Architectures & Protocols, SIGCOMM 1990, New York, NY, USA, pp. 297\u2013306 (1990). https:\/\/doi.org\/10.1145\/99508.99566","DOI":"10.1145\/99508.99566"},{"key":"14_CR19","unstructured":"McAuley, A.J.: Forward error correction code system. U.S. Patent 5,115,436 (1992)"},{"issue":"5","key":"14_CR20","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/s10836-020-05904-2","volume":"36","author":"M Naseer","year":"2020","unstructured":"Naseer, M., Ahmad, W., Hasan, O.: Formal verification of ECCs for memories using ACL2. J. Electron. Test. 36(5), 643\u2013663 (2020). https:\/\/doi.org\/10.1007\/s10836-020-05904-2","journal-title":"J. Electron. Test."},{"issue":"9","key":"14_CR21","doi-asserted-by":"publisher","first-page":"995","DOI":"10.1002\/(SICI)1097-024X(199709)27:9<995::AID-SPE111>3.0.CO;2-6","volume":"27","author":"JS Plank","year":"1997","unstructured":"Plank, J.S.: A tutorial on Reed-Solomon coding for fault-tolerance in RAID-like systems. Softw. Pract. Exp. 27(9), 995\u20131012 (1997)","journal-title":"Softw. Pract. Exp."},{"issue":"5","key":"14_CR22","doi-asserted-by":"publisher","first-page":"1123","DOI":"10.1109\/18.42233","volume":"35","author":"FP Preparata","year":"2006","unstructured":"Preparata, F.P.: Holographic dispersal and recovery of information. IEEE Trans. Inf. Theory 35(5), 1123\u20131124 (2006). https:\/\/doi.org\/10.1109\/18.42233","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"14_CR23","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1145\/62044.62050","volume":"36","author":"MO Rabin","year":"1989","unstructured":"Rabin, M.O.: Efficient dispersal of information for security, load balancing, and fault tolerance. J. ACM 36(2), 335\u2013348 (1989). https:\/\/doi.org\/10.1145\/62044.62050","journal-title":"J. ACM"},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1137\/0108018","volume":"8","author":"IS Reed","year":"1960","unstructured":"Reed, I.S., Solomon, G.: Polynomial codes over certain finite fields. J. Soc. Ind. Appl. Math. 8, 300\u2013304 (1960)","journal-title":"J. Soc. Ind. Appl. Math."},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Schwarz, T., Buckhard, W.: RAID organization and performance. In: [1992] Proceedings of the 12th International Conference on Distributed Computing Systems, pp. 318\u2013325 (1992). https:\/\/doi.org\/10.1109\/ICDCS.1992.235025","DOI":"10.1109\/ICDCS.1992.235025"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: Towards optimization-safe systems: analyzing the impact of undefined behavior. In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP 2013, pp. 260\u2013275. Association for Computing Machinery (2013). https:\/\/doi.org\/10.1145\/2517349.2522728","DOI":"10.1145\/2517349.2522728"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Wicker, S.B., Bhargava, V.K.: Reed-Solomon Codes and Their Applications. Wiley-IEEE Press (1999)","DOI":"10.1109\/9780470546345"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedTLS HMAC-DRBG. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, New York, NY, USA, pp. 2007\u20132020 (2017). https:\/\/doi.org\/10.1145\/3133956.3133974","DOI":"10.1145\/3133956.3133974"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Zaostrovnykh, A., et al.: Verifying software network functions with no verification expertise. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, New York, NY, USA, pp. 275\u2013290 (2019). https:\/\/doi.org\/10.1145\/3341301.3359647","DOI":"10.1145\/3341301.3359647"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Zaostrovnykh, A., Pirelli, S., Pedrosa, L., Argyraki, K., Candea, G.: A formally verified NAT. In: Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2017, New York, NY, USA, pp. 141\u2013154 (2017). https:\/\/doi.org\/10.1145\/3098822.3098833","DOI":"10.1145\/3098822.3098833"},{"key":"14_CR31","unstructured":"Zhang, K., Zhuo, D., Akella, A., Krishnamurthy, A., Wang, X.: Automated verification of customizable middlebox properties with Gravel. In: 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pp. 221\u2013239. USENIX Association, Santa Clara, CA, February 2020. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/zhang-kaiyuan"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:19:48Z","timestamp":1659687588000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}