Verified Erasure Correction in Coq with MathComp and VST

Joshua M. Cohen, Qinshi Wang, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

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’s authors. We use Coq’s Mathematical Components library to prove the algorithm’s 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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 34th International Conference, CAV 2022, Proceedings
EditorsSharon Shoham, Yakir Vizel
PublisherSpringer Science and Business Media Deutschland GmbH
Pages272-292
Number of pages21
ISBN (Print)9783031131875
DOIs
StatePublished - 2022
Event34th International Conference on Computer Aided Verification, CAV 2022 - Haifa, Israel
Duration: Aug 7 2022Aug 10 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13372 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference34th International Conference on Computer Aided Verification, CAV 2022
Country/TerritoryIsrael
CityHaifa
Period8/7/228/10/22

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Keywords

  • Reed-Solomon coding
  • functional correctness verification
  • interactive theorem proving

Fingerprint

Dive into the research topics of 'Verified Erasure Correction in Coq with MathComp and VST'. Together they form a unique fingerprint.

Cite this