SSTIC 2013 - Noyau sécurisé en Ada
Par ???
Les systèmes d’exploitations sont vulnérables parce qu’il sont très complexes et très très volumineux ce qui fait une surface d’attaque monstrueuse. En plus ils sont de plus en plus interconnectés et allumés h24. Il existe diverses protections pour venir contrer les attaques noyaux (cf grsec, pax, uderef, randstack etc…).
L’architecture micro-noyau est connue depuis longtemps (minix, hurd, etc..), et sa taille en fait un composant très simple. Bon le problème, c’est qu’on remplace les call par des IPC et c’est lent. En plus la compromission de certains modules mènent à la compromission du système complet.
Les méthodes formelles peuvent être employées pour venir prouver mathématiquement les propriétés du noyau. Mais dans la pratique c’est la galère… 8500 lignes de C pour 250 000 lignes de preuve et 11 ans de travail. Avec des contraintes à la con comme l’absence d’allocation dynamique et pas de support d’archi multi-coeurs.
Si on choisit un langage garantissant l’absence de débordements de tampon, on élimine 80% des vulnérabilités noyau. D’ou le choix de Ada. Faire un noyau en Ada fut compliqué, parce que le langage est difficile à apprendre, il faut concevoir différemment et il à fallu 6 mois à l’auteur pour être à l’aise en développement Ada.
Pour écrire un simple hello world, on ne peut directement écrire en RAM directement en Ada. il faut créer des types et passer par ces types pour effectuer l’écriture du message sur l’écran (galère). Pour gérer les bugs en Ada, il faut gérer les erreurs de typages dynamiques dans le noyau en recodant les fonctions chargés de gérer les erreurs de typages dans les programmes Userland.
Ce qui est fort en Ada, c’est qu’en cas de bug, on a l’info sur l’origine de l’erreur ce qui facilite le débogage Tout ceci à un coût en cycles d’horloge et en taille. Pour se débarrasser de ce code supplémentaire, il est possible d’utiliser SPARK, un sous-ensemble de Ada plus facile à prouver ce qui réduit l’overhead à 15%.
Coté Ada, le temps perdu à l’apprentissage est gagné par la vitesse de débogage et la confiance que l’on peut avoir dans le code.
