Runtime Verification of OCaml Programs
Mercredi 18 octobre 2023 14h
Université Paris-Saclay, bâtiment 660, salle 40 (amphi)
Formal verification methods, in particular when it comes to deductive verification, bring strong guarantees about the correctness of software systems. However, they require a high degree of expertise and tremendous development time. These pitfalls sometimes jeopardize their application in industrial-grade software, almost always preventing scaling to complex systems. In that respect, dynamic (read: runtime) verification allows for a more gradual approach. While the user still expresses specifications in a formal, precise language, one checks the correctness of the implementation *via* automatic testing at runtime rather than proofs. It narrows the required expertise to the specification design and the interpretation of test results. These observations also apply to the OCaml programming language community. Despite the suitability of the language for formal methods, broad adoption still seems out of reach for tools that produce specified or verified code. Moreover, such tools must account for details of the language: its type system, memory representation, garbage collector, and functional idioms.
In this work, we propose runtime verification techniques for OCaml code that apply to preexisting codebases and engineers’ workflows. In particular, we briefly introduce Gospel, an accessible yet expressive specification language for OCaml. We describe Ortac, an automated runtime assertion checker for OCaml with a modular interface that allows for multiple usage scenarii (fuzzing, monitoring, tests). Ortac aims to support a non-trivial subset of OCaml (e.g. functors, exceptions, effects). It uses typing information to produce efficient verifications (e.g. narrowing the copies, handling arbitrary precision integers, partially verifying type invariants). Lastly, we elaborate on memory optimizations for verifying postconditions referencing the prestate. They consist of specification transformations, generalized to apply to other languages, that have been proven correct using the Coq proof assistant.
This work opens a way for an automated verification ecosystem that would be unintrusive and suitable for the developers’ needs in the OCaml community.