| Title | : | Towards a Verified Garbage Collector for OCaml |
| Speaker | : | Sheera Shamsu (IITM) |
| Details | : | Wed, 10 May, 2023 11:00 AM @ MR-1(SSB-233) |
| Abstract: | : | Memory safety is an important property that ensures the absence of memory related bugs such as dangling pointers, memory leaks and buffer overflows. Manual memory management often introduces such bugs when the programmer accidentally forgets to free memory after use (memory leaks) or frees memory that is still being referenced by a pointer (dangling pointers). Such bugs can, at best, cause crashes and performance issues, but at worst, cause silent corruptions and open up security vulnerabilities. To overcome such serious bugs, managed languages like OCaml rely on automatic memory management through garbage collectors (GCs) which are often implemented as part of their runtime system. Ironically, GCs themselves can introduce memory safety bugs if their implementations incorrectly frees a memory block that is in use.
In this work, we have developed an approach to the practical formal verification of an efficient and portable mark and sweep GC for OCaml-style objects. Our approach relies on the principle of separation of concerns where we have separated the correctness specifications, the efficiency concerns, and the concrete implementation into three separate layers. These layers are linked together through proofs of equivalence between them such that the overall proof oriented development leads to the extraction of a verified, efficient and portable implementation of the mark function in C. Our entire formal development is in F*, a proof-oriented, solver-aided programming language. F* provides a low-level subset called Low* that facilitates the extraction of verified C code that is guaranteed to be correct and free from memory safety bugs. Our mark implementation runs in linear time in the number of allocated objects and in the number of references between them. Experimental evaluation o n a standard GC benchmark shows that our verified C implementation performs as well as a hand-written, unverified mark implementation. |
