Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
summary
Adds a verified Scala backend to ASN1SCC and uses Stainless verifier to prove crash freedom and semantic properties for generated serializers. Builds a Scala bitstream (≈3,700 LOC) and ACN codecs (≈4,000 LOC), proves absence of bounds/overflow/divzero and invertibility of decode(encode(x)) for the bitstream and records (sums/arrays and floats/strings remain partial). Generation emits sizes, pre/postconditions and lemmas automatically; verification produces about 335,000 VCs across ~300 PUSC and TC packet formats and uncovers bugs in existing C/Ada backends.
AI-written summary · about
chapters (16)
- 0:00Introduction to ASN.1/ACN encoders
- 1:17Formal verification for space missions
- 2:22ASN.1 and ACN formats explained
- 4:30Stainless framework overview
- 7:17Verification of static primitives
- 8:41Bitstream data structure
- 13:14ACN codec primitives verification
- 15:27Tailoring code generation
- 17:32Generated code verification
- 19:20Experimental results
- 20:42Lessons learned and bugs
- 22:05Key takeaways
- 23:09Project conclusion
- 23:52Q&A: Scala efficiency
- 24:34Q&A: Extending to JSON/Protobuf
- 25:39Q&A: Comparison with others
related talks
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
01h 04mSoftware Verification meets Real-World Cryptography
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
01h 07mThe Cogent and Dargent approach to facilitating verified software development
01h 07mThe seL4 verification: the art and craft of proof and the reality of commercial s
21mMechanised Hypersafety Proofs about Structured Data
47mHow to trust a verified program?
18mRISC-V Spotlight: Improving RISC-V Quality with Verification Standards and Advanc...