We propose a verified executable Scala backend for ASN1SCC, a compiler for ASN.1/ACN. ASN.1 is a language for describing data structures widely employed in ground and space telecommunications. ACN can be used along ASN.1 to describe complex binary formats and legacy protocols. To avoid error-prone and time-consuming manual writing of serializers, we show how to port an ASN.1/ACN code generator to generate Scala code. We then enhance the generator to emit not only the executable code but also strong enough pre-conditions, post-conditions, and lemmas for inductive proofs. This allowed us to verify the resulting generated annotated code using Stainless, a program verifier for Scala. The properties we prove include the absence of runtime errors, such as out-of-bound accesses or divisions by zero. For the base library, we also prove the invertibility of the decoding and encoding functions, showing that decoding yields the encoded value back. Furthermore, our system automatically inserts invertibility proofs for arbitrary records in the generated code, proving over 300'000 verification conditions. We establish key steps towards such proofs for sums and arrays as well.

翻译：我们为ASN1SCC（一种ASN.1/ACN编译器）提出了一个经过验证的可执行Scala后端。ASN.1是一种广泛应用于地面与空间通信领域的数据结构描述语言。ACN可与ASN.1配合使用，用于描述复杂的二进制格式及遗留协议。为避免易出错且耗时的手动编写序列化器，我们展示了如何移植ASN.1/ACN代码生成器以生成Scala代码。随后我们对该生成器进行增强，使其不仅能输出可执行代码，还能生成足够强的前置条件、后置条件及归纳证明引理。这使得我们能够利用Scala程序验证器Stainless对生成的带标注代码进行验证。我们证明的性质包括运行时错误的消除，例如越界访问或除零错误。针对基础库，我们还证明了编解码函数的可逆性，即解码操作能还原出原始编码值。此外，我们的系统能自动为生成代码中的任意记录类型插入可逆性证明，已验证超过30万个验证条件。我们同时为和类型与数组类型建立了实现此类证明的关键步骤。