Owi : Une exécution symbolique fluide pour WebAssembly

Le Défi

La vérification formelle est un levier puissant pour garantir la correction logicielle, mais les méthodes traditionnelles peuvent s'avérer manuelles, complexes et coûteuses. Les preuves déductives (via Rocq ou Lean) sont mathématiquement rigoureuses mais lentes et exigeantes en main-d'œuvre. Les outils d'analyse statique (comme Astrée ou MOPSA) automatisent les vérifications mais produisent souvent de nombreux faux positifs.

L'exécution symbolique offre un compromis idéal : elle trouve automatiquement les bugs en explorant le comportement du programme, tout en fournissant des contre-exemples concrets. Le défi consistait à rendre l'exécution symbolique accessible et pratique pour les workflows de développement modernes.

Pourquoi nous avons créé Owi

Titagone a développé Owi dans le cadre de sa mission visant à rendre les méthodes formelles opérationnelles pour le développement réel. En tirant parti de notre expertise en exécution symbolique, en WebAssembly et en vérification de programmes, nous avons vu l'opportunité de créer une alternative moderne à des outils vieillissants comme KLEE. Notre expérience en recherche et en vérification multi-langages nous a positionnés de manière unique pour construire un moteur d'exécution symbolique activement maintenu, basé sur des standards et simple d'utilisation.

Notre Solution : Owi

Développé par Titagone, Owi est un moteur d'exécution symbolique conçu pour fonctionner nativement avec WebAssembly (Wasm), un langage standardisé, de bas niveau et déterministe, facile à vérifier et largement supporté. Owi peut traiter du code compilé à partir du C, du C++ ou du Rust, unifiant plusieurs langages sous une interface unique.

Owi fonctionne en construisant un modèle complet du comportement du programme en Wasm, puis en l'exécutant symboliquement via une interface web ergonomique. Lorsqu'un bug potentiel est détecté, Owi produit un rapport d'erreur détaillé, s'appuyant sur des solveurs SMT comme Z3 ou Alt-Ergo.

Avantages par rapport à la concurrence

Contrairement à KLEE (le principal concurrent qui repose sur LLVM et souffre de problèmes de maintenance et de compatibilité), Owi est activement maintenu, supporte le standard Wasm et offre des performances comparables, ce qui le rend bien plus adaptable aux environnements de développement modernes.

Résultats

• Support multi-langages pour C, C++ et Rust via WebAssembly.
• Interface web interactive pour l'exploration de bugs et la génération de tests.
• Maintenance active avec des standards modernes et une meilleure compatibilité.
• Rend les méthodes formelles accessibles aux développeurs sans expertise profonde préalable.

Impact

Au-delà des performances pures, Owi rend l'exécution symbolique concrète. Il offre une interface fluide pour générer des tests, visualiser le comportement des programmes et explorer les cas limites dans un environnement interactif. En combinant les standards modernes (Wasm) et la rigueur de l'exécution symbolique, Owi permet aux ingénieurs de trouver les bugs plus rapidement et d'augmenter radicalement la fiabilité logicielle.