Automatic verification of spatial memory safety for low level programs with complex data structures is still an open problem despite the big advances accomplished by software verification. Indeed, it is difficult to find a good balance between scalability, precision and automation when complex memory invariants shall be specified, inferred and verified in presence of aliasing. In this talk, we will present an automated method combining TypedC, an expressive type system, and abstract interpretation to prove spatial memory safety of low-level programs as type-safety. In addition, we show that our method provides for inference of types specifying complex memory invariants for low-level programs. This method is implemented by the Codex framework and successfully applied to the verification of binary and C programs.

Professor at ENS Paris-Saclay, University Paris-Saclay and member of LMF. PhD from University of Grenoble under the supervision of Hubert Garavel at Verimag and INRIA. Previously member of IRIF and University of Paris-Cité.