Mikino, formal verification made accessible
OCamlPro at the JFLA2022 Conference
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, 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:
- #474 - Crash
- #475 - Crash
- #476 - Unsoundness
- #477 - Unsoundness
- #479 - Unsoundness
- #481 - Crash
- #482 - Crash
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 helped the French Income Tax Administration re-adapt and improve their internally kept M language, we designed a DSL to model and express revenue streams in the Cinema Industry, codename Niagara, and we also developed the prototype of the Tezos proof-of-stake blockchain from 2014 to 2018.
- 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.
Most Recent Articles
2024
- opam 2.3.0 release!
- Optimisation de Geneweb, 1er logiciel français de Généalogie depuis près de 30 ans
- Alt-Ergo 2.6 is Out!
- Flambda2 Ep. 3: Speculative Inlining
- opam 2.2.0 release!
- Flambda2 Ep. 2: Loopifying Tail-Recursive Functions
- Fixing and Optimizing the GnuCOBOL Preprocessor
- OCaml Backtraces on Uncaught Exceptions
- Opam 102: Pinning Packages
- Flambda2 Ep. 1: Foundational Design Decisions
- Behind the Scenes of the OCaml Optimising Compiler Flambda2: Introduction and Roadmap
- Lean 4: When Sound Programs become a Choice
- Opam 101: The First Steps
2023
- Maturing Learn-OCaml to version 1.0: Gateway to the OCaml World
- The latest release of Alt-Ergo version 2.5.1 is out, with improved SMT-LIB and bitvector support!
- 2022 at OCamlPro
- Autofonce, GNU Autotests Revisited
- Sub-single-instruction Peano to machine integer conversion
- Statically guaranteeing security properties on Java bytecode: Paper presentation at VMCAI 23
- Release of ocplib-simplex, version 0.5