Prouver qu'un système d'exploitation est fiable... est possible

Par 31 août 2009
Mots-clés : Smart city

Première mondiale : le seL4 est le premier micronoyau de système d'exploitation certifié sans grosse erreur de code

"Le code C du microkernel seL4 intègre correctement les comportements décrits dans ses spécifications abstraites et rien de plus". Plus simplement, c'est la première fois qu'un micronoyau de système d'exploitation généraliste est certifié sans erreur pour les services qu'il est censé rendre. C'est en tout cas l'assertion du centre d'excellence australien en technologies de l'information (NICTA), relayée par The New Scientist. En l'occurrence, ce sont donc les actions de près de 7500 lignes de code qui ont été scrutées, sur les 8700 que compte le seL4. Le code machine pour ARM11 a également été laissé de côté. Cette preuve formelle amène des résultats concrets.
Vers des applications plus sûres ?
Les ingénieurs certifient entre autres que les attaques de type "Buffer overflows" (ou dépassement de tampon) n'ont pas d'effet sur seL4, que des erreurs comme celles qui sont liées aux pointeurs (‘Null pointer references’, par exemple), ou les fuites de mémoires (Memory Leaks) n'y adviennent pas. L'avantage est qu'il sera dorénavant plus "simple" de certifier les programmes qui font appel à ce micro-kernel. Comme l'indique son nom, le Secure Embedded L4 est une version sécurisée de la famille de micronoyaux L4. Sur cette version peut venir se greffer un OS Linux, avec un processeur x86 ou ARM 11. À noter que cette dernière architecture est utilisée pour la plupart des microprocesseurs embarqués dans les téléphones mobiles et les assistants personnels.
Des accès "privilèges"
  Ces noyaux disposent des plus forts privilèges d'accès au matériel. Mais ils sont très limités en fonction : pas de gestion des fichiers ni de piles réseau. Les autres nombreux services, potentiellement plus risqués pour l'intégrité du système, sont placés dans l'espace utilisateur dont l'accès aux ressources du système est plus limité. Les systèmes d'exploitation qui font usage de micro-kernels - comme l'Unix d'IBM, AIXPour le centre d'excellence australien en nouvelles technologies, il s'agit aussi de la plus grande preuve formelle jamais établie. (Advanced Interactive eXecutive) - sont logiquement considérés comme plus sûrs.

Mentions légales © L’Atelier BNP Paribas