Treffer: A Comparative Study on Deductive Verification for Rust and C ; En jämförande studie av deduktiv verifiering för Rust och C

In programming, deductive verification is a technique to generate proof that a function obeys a set of manually specified regulations in the form of annotations. In addition to these annotations, the verifier also utilizes the constraints of the underlying programming language to prove that the function cannot cause the program to crash unexpectedly. This thesis investigates how the type system of Rust, specifically built-in memory-safety guarantees, can affect the amount and types of annotations required for a verifier to generate a proof of the correctness of a function, as compared to C. This was done by comparing the differences in the annotations required to verify example functions in Rust and C, using their respective verification tools, Prusti and Frama-C. The results show that the number of required annotations for a function implemented in C is higher when compared to Rust. Furthermore, the annotations used in Rust were a strict subset of those in C for the functions tested. This indicates that the memory-safety guarantees present in Rust play a role in the practicality of annotating functions for deductive verification. However, future work with more data and verification tools with a richer feature set is needed to draw more precise conclusions. ; Deduktiv verifiering är en teknik inom programmering som kan generera ett bevis för att en funktion följer en uppsättning av manuellt angivna bestämmelser i form av noteringar. Utöver dessa noteringar använder verifieraren också begränsningarna för det underliggande programmeringsspråket för att bevisa att funktionen inte kan få programmet att oväntat krascha. Denna studie undersöker hur typsystemet för programmeringsspråket Rust, specifikt de inbyggda minnessäkerhetsgarantierna, kan påverka mängden och typerna av noteringar som krävs för att en verifierare ska kunna generera ett bevis för en funktion, jämfört med C. Detta gjordes genom att jämföra skillnaderna i de noteringar som krävs för att verifiera exempelfunktioner i Rust och C, med hjälp av deras ...