TY - GEN
T1 - Verified Erasure Correction in Coq with MathComp and VST
AU - Cohen, Joshua M.
AU - Wang, Qinshi
AU - Appel, Andrew W.
N1 - Publisher Copyright:
© 2022, The Author(s).
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - Reed-Solomon coding
KW - functional correctness verification
KW - interactive theorem proving
UR - http://www.scopus.com/inward/record.url?scp=85136142567&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85136142567&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-13188-2_14
DO - 10.1007/978-3-031-13188-2_14
M3 - Conference contribution
AN - SCOPUS:85136142567
SN - 9783031131875
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 272
EP - 292
BT - Computer Aided Verification - 34th International Conference, CAV 2022, Proceedings
A2 - Shoham, Sharon
A2 - Vizel, Yakir
PB - Springer Science and Business Media Deutschland GmbH
T2 - 34th International Conference on Computer Aided Verification, CAV 2022
Y2 - 7 August 2022 through 10 August 2022
ER -