Skip to main content

Generating formally verified communication protocol implementations

Running

Running

Prime contractor
Organisational Unit
Implementation progress
0%
15 December 2022

Duration: 18 months

Objective

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.

Contract number
4000140196
Programme
OSIP Idea Id
I-2022-00629
Related OSIP Campaign
New concepts for onboard software development
Subcontractors
ECOLE POLYTECHNIQUE FEDEDALE DE LAUSANNE
Main application area
Exploration
Budget
171835€
GENERATING FORMALLY VERIFIED COMMUNICATION PROTOCOL IMPLEMENTATIONS