Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
Mario Bucev, Samuel Chassot, Simon Felix, Filip Schramka, Viktor Kunčak
TL;DR
The paper tackles the risk of bugs in serialized data by building a formally verifiable generator for ASN.1/ACN encoders and decoders. It introduces a Scala backend for ASN1SCC that emits verifiable code and inductive specifications, enabling Stainless to prove runtime safety and invertibility. Through a PUS-C aerospace case study, the authors demonstrate substantial progress, including invertibility proofs for records and automatic lemma generation, while revealing and addressing bugs in the generator. The work provides a practical path to reliable, verified serialization for legacy and complex binary formats, with potential impact on space mission software and secure-as-built pipelines.
Abstract
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.