SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Sun 22 Oct 2023 14:00 - 14:30 at Room IV - Paper presentations 2 Chair(s): Kyungmin Bae

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 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
Paper presentations 2FTSCS at Room IV
Chair(s): Kyungmin Bae POSTECH
14:00
30m
Talk
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
30m
Talk
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
30m
Talk
Discussions, Closing
FTSCS
Peter Ölveczky University of Oslo, Cyrille Artho KTH Royal Institute of Technology, Sweden