Collaborative Research: SaTC: CORE: Medium: Refine the Gap: Establishing Safety for Modern Foreign Function Interfaces

Developers of widely used software infrastructure like the Firefox, Chrome, and Linux are replacing components written in unsafe but fast languages like C/C++ with components written in Rust. Rust promises to eliminate the security vulnerabilities endemic to C/C++ codebases without compromising on performance. Alas, completely rewriting real-world software systems is not practical: Firefox, Chrome, and Linux are tens of millions of C/C++ code. Instead, Rust components must continue to interact with existing C/C++ code. In practice, this requires developers to write code that glues Rust and C/C++. Unfortunately, this glue code is notoriously difficult to write correctly: code at the language boundary can both introduce errors in previously safe code and impose new unchecked requirements, threatening the security of both the Rust code and the containing C/ C++ ecosystem. This project will address these challenges by building new abstractions, techniques, and tools that will help developers securely integrate Rust components within C/C++ applications (and vice versa). This research will span the spectrum from new theoretical and formal ideas to the deployment and integration of this technology in real-world software. The project has the potential to directly improve the security of software infrastructure used by billions of users, including Firefox, Chrome, and Linux. The project will also contribute to the graduate, undergraduate, and high school curriculum, introducing future developers to techniques and tools for building secure software. This project takes a principled and practical approach to building secure systems software by securing the glue layer between C/C++ and Rust and the foreign function interface (FFI) developers used to write this glue code. To accomplish these goals, this project will (1) build novel static analysis tools for the Rust ecosystem, which work in tandem with human auditing to detect, triage, and classify major weaknesses in existing FFIs; (2) build novel abstractions for the FFI layer based on refinement types to describe and automatically check memory safety and type safety properties at the FFI layer, and eliminate the ad-hoc glue code at the FFI layer; (3) build a lightweight sandboxing layer for calling C/C++ code from Rust, leveraging prior sandboxing mechanisms but marrying their abstractions with Rust's ownership type system. This research will yield new insights into the safety and security gaps in modern multi-language systems; contribute to the understanding of how refinement types can integrate with a modern memory-safe type system and mutability constraints; and develop our understanding of how modern security techniques -- including static analysis, type systems, and sandboxing -- are applicable to the Rust ecosystem and ownership model. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.