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 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.
Sun 22 OctDisplayed time zone: Lisbon change
14:00 - 15:30 | |||
14:00 30mTalk | Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library FTSCS Aïssata Maiga , Cyrille Artho KTH Royal Institute of Technology, Sweden, Florian Gilcher , Yannick Moy AdaCore | ||
14:30 30mTalk | Formal Verification of a Mechanical Ventilator using UPPAALRemote FTSCS Jaime Cuartas Universidad del Valle, David Cortés , Joan S Betancourt , Jesus Aranda Universidad del Valle, Jose Garcia , Andres Valencia , James Ortiz Université de Namur | ||
15:00 30mTalk | Discussions, Closing FTSCS |