Rudra
Yechan Bae, Young-Suk Kim, Ammar Askar, Jungwon Lim, Taesoo Kim
Abstract
Rust is a promising system programming language that guarantees memory safety at compile time. To support diverse requirements for system software such as accessing low-level hardware, Rust allows programmers to perform operations that are not protected by the Rust compiler with the unsafe keyword. However, Rust's safety guarantee relies on the soundness of all unsafe code in the program as well as the standard and external libraries, making it hard to reason about their correctness. In other words, a single bug in any unsafe code breaks the whole program's safety guarantee.
Topics & Concepts
CompilerComputer scienceMemory safetyRust (programming language)CorrectnessSoundnessProgramming languageOperating systemCode (set theory)Embedded systemSet (abstract data type)Software Testing and Debugging TechniquesFormal Methods in VerificationSoftware Reliability and Analysis Research