形式化可验证的生成 ASN.1/ACN 编码器与解码器：一项案例研究
软件工程
2024-12-11 v1 编程语言
摘要
我们为 ASN1SCC 提出一个经过验证的可执行 Scala 后端。ASN.1 是广泛用于地面和空间电信领域描述数据结构的语言。ACN 可与 ASN.1 配合使用，用于描述复杂的二进制格式和遗留协议。为了避免易出错且耗时的手动编写序列化器，我们展示了如何将 ASN.1/ACN 代码生成器移植以生成 Scala 代码。随后我们增强该生成器，使其不仅输出可执行代码，还输出足够强的前置条件、后置条件以及用于归纳证明的引理。这使得我们能够使用 Scala 程序验证工具 Stainless 对生成的标注代码进行验证。我们证明的性质包括运行时错误的缺失，例如越界访问或除以零。对于基础库，我们还证明了编码和解码函数的可逆性，表明解码可得到编码值。此外，我们的系统自动为生成代码中的任意记录插入可逆性证明，验证了超过 300,000 个验证条件。我们也为和与数组建立了此类证明的关键步骤。
引用
@article{arxiv.2412.07235,
title = {Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study},
author = {Mario Bucev and Samuel Chassot and Simon Felix and Filip Schramka and Viktor Kunčak},
journal= {arXiv preprint arXiv:2412.07235},
year = {2024}
}