Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library

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 compiletime 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.