Search code, repositories, users, issues, pull requests...

This repository contains the code implementation for the master's thesis CORAL: a Rust-like Borrow Checker for C and the LCTES'24 paper Foundations for a Rust-Like Borrow Checker for C. The code provided here is meant to support the findings and experiments described in both works.

The C/C++ programming languages have been used for more than 50 years, and their popularity has not wavered. Being a de facto standard programming language, C is still used to maintain legacy code and to write new software, despite being prone to many vulnerabilities, including the lack of memory safety rules. Over the last decade, new languages adequate for low-level programming have risen as alternatives, such as Rust or Go.

A relevant portion of these vulnerabilities can be tackled by simply using a language that is type-safe, and whose compiler checks for memory and concurrency safety, such as Rust. However, learning a new language is a time-consuming task, and the transition of existing C codebases requires a significant effort to rewrite. Moreover, many traditional C compilation targets, such as the embedded systems market, are not yet ready to adopt Rust as a viable alternative, as they lack the build tools and libraries necessary to compile to their hardware.

Source-to-source compilation allows the direct analysis and transformation of the original source code. This allows transformations to be composed upstream of the compiler. Through the use of this technique, it is possible to apply successive transformations to the source code whilst keeping it in the original language, which can be leveraged to preserve the correctness of the program, while approximating it to a desired set of non-functional properties and guarantees.

Leave a Comment