Ironclad – noyau de type Unix temps réel

• Ironclad est un noyau de type Unix temps réel fondé sur la vérification formelle pour les environnements grand public et embarqués
  • Vérification formelle (Formal verification) : ensemble de processus et de contrôles appliqués au code du noyau afin de garantir l’absence d’erreurs à l’exécution (AoRTE, Absence of Runtime Errors) et l’exactitude des composants
• Écrit en SPARK et Ada, il est composé à 100 % de logiciel libre
• Prend en charge une interface compatible POSIX, le multitâche préemptif, le contrôle d’accès obligatoire (MAC) et l’ordonnancement temps réel strict
• Distribué sous licence GPLv3, il conserve une architecture entièrement open source sans blob firmware
• Portable sur plusieurs plateformes, avec un écosystème en expansion via des distributions comme Gloire

---

Présentation du noyau du système d’exploitation Ironclad

• Ironclad est un noyau de type UNIX temps réel utilisant partiellement la vérification formelle (formal verification)
  • Conçu à la fois pour les systèmes à usage général et les systèmes embarqués
  • Vérification formelle (Formal verification) : ensemble de processus et de contrôles appliqués au code du noyau afin de garantir l’absence d’erreurs à l’exécution (AoRTE, Absence of Runtime Errors) et l’exactitude des composants
  • Pour cela, il s’appuie sur ** SPARK**, un sous-ensemble de Ada
  • L’ensemble du code est constitué de logiciel libre
• Le noyau fournit une interface compatible POSIX et prend en charge le multitâche préemptif, le contrôle d’accès obligatoire (MAC) et l’ordonnancement temps réel strict
  • Il offre une expérience de développement proche des environnements UNIX existants
  • Sa structure est adaptée aux systèmes nécessitant un contrôle temps réel

Caractéristiques en tant que logiciel libre

• Ironclad est distribué comme un projet entièrement open source sous licence GPLv3
  • Le noyau n’inclut aucun blob firmware (firmware blob)
  • Tous les composants de la pile sont fournis sous forme open source

Vérification formelle (Formal Verification)

• Il exploite les fonctions de vérification formelle du langage SPARK pour garantir l’absence d’erreurs et l’exactitude des composants clés
• SPARK permet de vérifier mathématiquement la cohérence logique du code en spécifiant dans le code Ada des préconditions (Pre), postconditions (Post) et dépendances (Depends)
  • Les éléments vérifiés incluent notamment des modules cryptographiques, le système MAC et des fonctions liées à l’interface utilisateur

Portabilité et environnement de développement

• Ironclad a été porté sur plusieurs plateformes et cartes, et a été conçu pour faciliter les portages supplémentaires
  • Il ne dépend que de la toolchain GNU, ce qui permet une compilation croisée aisée
  • Grâce à sa compatibilité POSIX, le portage logiciel et le développement sont facilités

Distributions et écosystème

• Le projet Ironclad fournit des distributions (distribution) pour diverses architectures et cartes
  • La principale distribution libre et open source est Gloire
  • Des images de distribution téléchargeables au format tarball sont proposées

Soutien au projet et pérennité

• Ironclad reste un projet librement utilisable, étudiable et modifiable
  • Le fonctionnement du projet repose sur les dons et les subventions
  • Chaque contribution a un impact direct sur l’extension et le développement du projet

[GN⁺]

Avis Hacker News

• Projet intéressant. Je me demande quelles sont les limites de la vérification formelle du temps d’exécution dans le pire des cas (WCET)
  Il existe aussi d’autres noyaux vérifiés comme seL4 et atmosphere, et on peut aussi empiler une couche de compatibilité POSIX comme avec genode
  Il existe également des noyaux complètement compatibles et matures comme QNX ou VxWorks, donc une vérification complète n’apporte peut-être pas une si grande valeur ajoutée
  En revanche, j’ai rarement vu des exemples réunissant à la fois WCET + vérification formelle + compatibilité POSIX
  À ce stade, il me semble difficile de considérer que le niveau de maturité est suffisant pour l’utiliser immédiatement dans les cas d’usage temps réel mentionnés dans la documentation

  • Dans le monde actuel, n’importe quel gouvernement peut obtenir une RCE sur un OS. C’est pourquoi la vérification formelle de l’isolation des processus est vraiment importante
    seL4 est bien plus rapide que Linux, mais celui-ci me semble plus lent. POSIX est fondamentalement défectueux, et le MAC est trop complexe pour être utilisable en pratique
  • Ce n’est encore qu’au niveau de stone, mais il semble possible qu’il puisse obtenir une certification officielle à l’avenir. Un OS formellement vérifié représente une grande avancée pour la sécurité

• Ada fait partie de la famille des langages de Wirth (famille Pascal). Jusqu’à présent, le seul noyau de type Unix que je connaissais dans cette famille était TUNIS
  TUNIS a été implémenté en Concurrent Euclid

  • Il y avait aussi SPIN, développé à l’université de Washington dans les années 90. C’était un système à microkernel écrit en Modula-3 qui prenait en charge l’interface d’appels système de Digital UNIX
    Dans les années 80, l’INRIA avait aussi Sol, implémenté dans un dialecte de Pascal et fournissant un environnement compatible Unix, avant d’aboutir ensuite à Chorus

• Il existe aussi une entreprise liée aux NDA qui s’appelle Ironclad. Il faut faire attention aux problèmes de marque déposée
  Cela dit, ce genre de tentative est vraiment bienvenu. Mais dans la réalité, le maillon le plus faible de la sécurité reste la couche firmware
  Mon rêve serait un matériel comme les ordinateurs Framework, avec un firmware EFI vérifié et des firmwares audités composant par composant

  • Ironclad est aussi le nom d’une importante bibliothèque de cryptographie pour Common Lisp (ironclad GitHub)
  • MNT Research mérite aussi le détour. Ils fabriquent des ordinateurs portables réparables et publient matériel et logiciel en open source (mnt.re)
  • La vérification du firmware nécessite un noyau distinct. Ce genre de sujet devrait désormais être géré au niveau de la réglementation
  • Les marques ne posent pas de problème si elles partagent le même nom mais relèvent de secteurs d’activité différents. Par exemple, le cas d’Apple Computer et des Beatles avec Apple Music (xkcd 386)

• Créer un nouvel OS, c’est vraiment ambitieux. Radiant Computer est aussi apparu récemment, et je me demande s’il existe d’autres projets intéressants du même genre

  • Asterinas (noyau compatible Linux) et Redox OS sont prometteurs
  • Il y a aussi SerenityOS
  • C’est une alternative ancienne, mais Haiku OS reste intéressant
  • J’ai moi aussi une idée d’OS. Je réfléchis à plusieurs composants, du matériel au noyau jusqu’aux programmes utilisateur
  • ReactOS continue aussi d’évoluer. Ce n’est pas un OS entièrement nouveau, mais je le trouve malgré tout novateur

• J’espère qu’un jour les noyaux entièrement formellement vérifiés se généraliseront
  Vérifier l’ensemble de Linux est sans doute impossible, mais seL4 pourrait peut-être trouver sa chance sur des marchés comme celui des smartphones

  • seL4 est déjà utilisé dans des systèmes comme le Secure Enclave OS (L4 microkernel family)
  • seL4 est déjà utilisé dans plusieurs endroits, et si l’on regarde les cas d’usage et la liste des membres, il semble possible qu’il se diffuse encore davantage à l’avenir

• En regardant leur feuille de route de vérification, c’est excessif d’appeler cela de la « vérification formelle »
  Il n’y a aucune preuve de propriétés essentielles du noyau, et cela n’atteint pas le niveau de noyaux comme seL4 ou Tock

• CuBit est un autre OS écrit en SPARK/Ada
  Le code source peut être consulté sur GitHub

• Du point de vue d’un utilisateur ordinaire, le noyau seul ne sert à rien
  Un exemple d’OS utilisant le noyau Ironclad est Gloire

• La documentation sur le MAC est bien structurée (Mandatory Access Control)

• Quand on voit la mention « demander les prix » pour SPARK, cela semble davantage relever d’un autre sens de « free » que de logiciel libre

  • La plupart des liens GitHub ci-dessus facturent aussi le support commercial. Demander les prix est une procédure courante, donc il n’y a rien de particulièrement étrange
  • Au final, les développeurs doivent aussi gagner leur vie, ce qui est parfaitement normal