Pointer Ownership Model: AI-Powered Memory Safety for C Applications

Preventing improper use after memory has been freed is a key concern. This error results in an exploitable vulnerability when attackers access important information allocated to the previously freed memory. Among memory safety errors, use-after-free is second only to buffer overflow in the 2025 CWE Top 25 Most Dangerous Software Weaknesses.

The Pointer Ownership Model (POM) project enforces temporal memory safety. Inspired by Rust's Borrow Checker and C++’s RAII principle, POM employs a Large Language Model (LLM) and a Satisfiability (SAT) Solver to streamline the generation of models and formal proofs. POM automates the model development process, reducing the time to build a model and achieves 94 percent of pointers modelled correctly by the LLM. POM also leverages technology built in previous CMU SEI projects, Redemption and Detection of Malicious Code.

Any program that complies with POM can be statically analyzed to ensure that its design is consistent and secure regarding temporal memory safety.