Table of contents

Mikino, formal verification made accessible

Connecting Software Heritage with the OCaml ecosystem

Alt-Ergo-Fuzz, hunting the bugs of the bug hunter

OCamlPro at the JFLA2022 Conference

Authors: OCamlPro, Dario Pinto
Date: 2022-07-12
Category: OCamlPro
Tags: jfla, Software Heritage, swh, ocaml, Alt-Ergo, fuzzing, mikino, rust, formal verification


Domaine d'Essendiéras , located in French Region Perigord, where the JFLA2022 took place!

In today's article, we share our contributions to the 2022 JFLAs, the French-Speaking annual gathering on Application Programming Languages, mainly Functional Languages such as OCaml (Journées Francophones des Langages Applicatifs).

This much awaited event is organised by Inria, the French National Institute for Research in Science and Digital Technologies.

This is always the best occasion for us to directly share our latest works and contributions with this diverse community of researchers, professors, students and industrial actors alike. Moreover, it allows us to meet up with all our long known peers and get in contact with an ever changing pool of actors in the fields of functional languages in general, formal methods and everything OCaml!

This year the three papers we submitted were selected, and this is what this article is about!

Mikino, formal verification made accessible⚓

Mikino and all correlated content mentionned in this article was made by Adrien Champion

If you follow our Blog, you may have already read our Mikino blogpost, but if you haven't here's a quick breakdown and a few pointers... In case you wish to play around or maybe contribute to the project. ;)

So what is Mikino ?

Mikino is a simple induction engine over transition systems. It is written in Rust, with a strong focus on ergonomics and user-friendliness.

Depending on what your needs are, you could either be interested in the Mikino Api or the Mikino Binary or just, for purely theoretical reasons, want to undergo our Verification for Dummies: SMT and Induction tutorial which is specifically tailored to appeal to the newbies of formal verification!

Have a go at it, learn and have fun!

For further reading: OCamlPro's paper for the JFLA2022 (Mikino) (French-written article describing the entire project).

Connecting Software Heritage with the OCaml ecosystem⚓

The archiving of OCaml packages into the SWH architecture, the release of swhid library and the integration of SWH into opam was done by Léo Andrès, Raja Boujbel, Louis Gesbert and Dario Pinto

Once again, if you follow our Blog, you must have seen Software Heritage (SWH) mentioned in our yearly review article.

Now you can also look at SWH paper by OCamlPro for the JFLA2022 (French) if you are looking for a detailed explanation of how important Software Heritage is to free software as a whole, and in what manner OCamlPro contributed to this gargantuan long-term endeavour of theirs.

This great collaboration was one of the highlights of last year from which arose an OCaml library called swhid and the guaranteed perennity of all the packages found on opam.

The work we did to achieve this was to:

  • add a few modules to the SWH architecture in order to store all the OCaml packages found on opam in the Library of Alexandria of open source software.
  • release a library used for computing SWH identifiers
  • add support in opam in order to allow a fallback on SWH architecture if a given package is missing from the opam repository
  • patch the opam repository in order to detect already missing packages

Alt-Ergo-Fuzz, hunting the bugs of the bug hunter⚓

The fuzzing of the SMT-Solver Alt-Ergo was done by Hichem Rami Ait El Hara, Guillaume Bury and Steven de Oliveira

As the last entry of OCamlPro's papers that have made it to this year's JFLA: a rundown of Hichem's work, guided by Guillaume and Steven, on developping a Fuzzer for Alt-Ergo.

When it comes to critical systems, and industry-borne software, there are no limits to the requirements in safety, correctness, testing that would prove a program's reliability.

This is what SMT (Satisfiability Modulo Theory)-Solvers like Alt-Ergo are for: they use a complex mix of theory and implementation in order to prove, given a set of input theories, whether a program is acceptable... But SMT-Solvers, like any other program in the world, has to be searched for bugs or unwanted behaviours - this is the harsh reality of development.

With that in mind, Hichem sought to provide a fuzzer for Alt-Ergo to help hunt the bugs of the bug hunter: Alt-Ergo-Fuzz.

This tool has helped identify several bugs of unsoundness and crashes:

More details in OCamlPro's paper for the JFLA2022 (Alt-Ergo-Fuzz).


About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from experts with a state-of-the-art knowledge of programming languages theory and practice.

  • We provide audit, support, custom developer tools and training for both the most modern languages, such as Rust, WASM and OCaml, and for legacy languages, such as COBOL or even home-made domain-specific languages;
  • We design, create and implement software with great added-value for our clients. High complexity is not a problem for our PhD-level experts. For example, we developed the prototype of the Tezos proof-of-stake blockchain.
  • We have a long history of creating open-source projects, such as the Opam package manager, the LearnOCaml web platform, and contributing to other ones, such as the Flambda optimizing compiler, or the GnuCOBOL compiler.
  • We are also experts of Formal Methods, developing tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club) and using them to prove safety or security properties of programs.

Please reach out, we'll be delighted to discuss your challenges: contact@ocamlpro.com or book a quick discussion.