Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study

TL;DR

This paper presents a verified Scala backend for ASN.1/ACN code generation, enabling automatic proof of correctness properties like error absence and invertibility, thus improving reliability in telecommunications data serialization.

Contribution

It introduces a verified code generator for ASN.1/ACN that produces Scala code with embedded correctness proofs, enhancing reliability and automation in data serialization.

Findings

Proved absence of runtime errors in generated code

Verified invertibility of encoding and decoding functions

Automatically generated over 300,000 verification conditions

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.