A critical moment during the launch of a mission is when communication is established for the first time. For ground control to communicate with a satellite or payload, the engineering teams must formulate the communication protocols as early as the requirements definition phase, refine and implement them during the design, verification, and production phases, and maintain them after launch. ESA addresses this need for reliability despite constant change with the OPUS and the ASN1SCC projects. These tools generate documentation and code from standardized protocol definitions, which engineers can maintain more reliably with less effort. We propose to extend these toolsets with a Scala code generator that produces formally verifiable code, which can then be converted to embeddable C code. We prove that the generated protocol implementations are free of software defects, like buffer overflows and other bugs, and adhere to the specification. As a result, this approach significantly increases the reliability of core components and eliminates certain cybersecurity attack vectors. After successfully demonstrating the correctness of the Scala generator, we will extend the proofs to include higher-level requirements and more program logic (e.g., state and parameter management). Extending the results of this project, we envision eventually building out a complete library of formally verified COTS components.
