• ffi
• foreing function interfaces
• memory issues
• multi-language programs
• rust
• static analysis
• taint analysis

Rust è un linguaggio di programmazione emergente ed alternativo per la programmazione sicura a livello di sistema rispetto a C e Assembly, grazie alla sua gestione sicura della memoria senza necessità di garbage collector. Tuttavia, Rust permette l'interazione con codice C tramite il meccanismo delle Foreign Function Interface (FFI). L'inclusione di codice C potenzialmente non sicuro può compromettere le proprietà di sicurezza della memoria, causando potenziali problemi come never-free, use-after-free e double-free. Lo scopo della tesi è quello di progettare un'analisi statica (taint analysis) per individuare possibili errori di memoria in questo scenario cross-language. In primo luogo, viene formalizzata una parte significativa del linguaggio Rust fornendo una semantica operazionale che cattura le caratteristiche chiave di Rust e l'interazione con il codice non sicuro tramite FFI. Successivamente, vengono definite le regole semantiche statiche che prevedono, al momento della compilazione, il rilevamento di eventuali errori di memoria.


The Rust programming language is an emerging and promising alternative
for safe system-level programming with respect to C and Assembly because of its unique safe ownership-based memory management without garbage collector. However, Rust allows interaction with C code via the foreign function interface (FFI) mechanism. The inclusion of potentially unsase C code may undermine ownership properties, resulting in potential memory issues such as never-free, use-after-free and double-free. The purpose of this work consist of designing a static (taint) analysis to determine possible memory bugs in such cross-language scenario. First, we formalize a significant fragment of Rust language providing an operational semantics that captures the key features of Rust and the interaction through the FFI with unsafe code. Then, we define static semantic rules that predict at compile time whether some memory errors may arise.