FTSCS 2023 - Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, Co-located: SPLASH 2023. :37-47
Both Rust and SPARK are memory-safe programming languages and feature stronger safety guarantees than other popular programming languages for embedded software. However, modern systems often combine software written in multiple programming languages using the Foreign Function Interface (FFI). When using safety-oriented programming languages such as Rust and SPARK, maintaining compile-time safety guarantees across a language boundary is a challenge. The objective of this study is to explore if/how the inherent safety guarantees of these languages are preserved, and their potential benefits when establishing a library interface between them. In particular, we apply our method to the BBQueue circular buffer library that features complex ownership hand-over patterns when using FFI. Results reveal that most of the inherent consistency and safety features of these languages can be maintained. Yet, special caution is required at the FFI boundary to prevent potential vulnerabilities.
