La version de développement 0.6 du micronoyau open source à très haut niveau de sécurité et de fiabilité Muen Separation Kernel est désormais compatible avec la technologie Spark 2014. C’est ce que viennent de confirmer l’éditeur ...français AdaCore et l’institut des technologies et applications Internet de l’université suisse des sciences appliquées de Rapperswil qui ont utilisé le langage et les outils Spark 2014 pour prouver de manière formelle l’absence d’erreurs dans l’environnement d’exécution et, partant, assurer toute confiance dans l’utilisation du micronoyau.

Muen, rappelons-le, amène une isolation stricte et robuste entre composants logiciels tournant sur un même système physique. L’idée est de protéger des applications critiques et de les rendre non vulnérables à des corruptions frappant des applications moins critiques avec lesquelles elles cohabitent sur le même environnement matériel. Spark 2014 est, pour sa part,  une évolution majeure du langage de programmation Spark qui utilise et étend en particulier l'approche de la programmation par contrat introduite dans Ada 2012, permettant ainsi aux développeurs de code critique Ada d'exprimer et de vérifier les propriétés essentielles qu'un programme doit respecter. Le support de Spark 214 est notamment assuré dans la dernière version en date de l'environnement de vérification et de développement intégré Spark Pro d’Adacore.

L’équipe de développement Muen a donc exploité l’approche de vérification Spark 2014 en complétant leur utilisation des méthodes formelles avec celui du framework de test unitaire GNATtest pour générer le harnais et les modèles de simulation de test.

Depuis la publication de la précédente préversion de Muen à l’automne 2013, la plate-forme a elle-même évolué avec le support des machines virtuelles Linux et l’implémentation du mécanisme PCI-Device Passthrough (pour l’assignation directe d’un circuit PCI physique de la machine hôte à un environnement logiciel « invité » au-dessus du micronoyau). Par ailleurs, l’ajout d’un langage de description système modulaire permet désormais aux utilisateurs d’intégrer des systèmes complexes à composants logiciels au-dessus du noyau Muen.