IRILL - Research and Innovation on Free Software OCaml provides an FFI mechanism (Foreign Function Interface) allowing OCaml programs to call external functions implemented in C, typically by writing "glue code" helping bridge the two languages. This "glue code" needs to be carefully written and obey a number of rules when interacting with the OCaml runtime (cf chapter 22 of the manual). Failure to follow one of these rules typically result in silent corruption of the program memory, resulting in fatal and hard to debug crashes. This presentation will present ongoing research on formalizing the rules one need to follow to correctly use the OCaml FFI. We will see how a small number of permissions can capture the requirements one must obey in order to write bug-free glue code.
Les slides sont disponibles sur https://framagit.org/oups/talks/-/blob/main/05_23/gueneau.pdf