seL4 : Le premier système d'exploitation prouvé sans erreur par une équipe de recherche Australienne (le NICTA)

Le , par millie, Rédacteur
Une équipe de chercheur du NICTA (Australia's Information and Communications Technology Centre of Excellence) a écrit un micro-noyau de système d'exploitation orienté système embarqué dont la sécurité face à plusieurs types de failles a été prouvé formellement (typiquement, des buffers overflow).

L'écriture des 7500 lignes de code a nécessité 4 ans, la preuve est composé de 10.000 théorèmes et de 200.000 lignes de preuves.

L'utilité de ceci est d'être sûr que certaines failles classiques ne peuvent être exploités.

Vous en pensez-quoi ?

Plus de détails sur le projet : http://www.ertos.nicta.com.au/research/sel4/


Vous avez aimé cette actualité ? Alors partagez-la avec vos amis en cliquant sur les boutons ci-dessous :


 Poster une réponse

Avatar de granquet granquet - Membre expérimenté https://www.developpez.com
le 20/08/2009 à 13:02
Citation Envoyé par Mac LAK  Voir le message
Donc, c'est très intéressant, mais je pense que ça n'arrive pas encore au niveau des OS certifiés tels qu'OSE ou QNX Neutrino...

ce micro noyau permet de faire tourner un autre noyau en host!
pour l'instant il permet de faire tourner Linux sur x86 et bientot sur ARM !
et la, ca deviens tres interessant
Avatar de FR119492 FR119492 - Rédacteur https://www.developpez.com
le 20/08/2009 à 13:32
Salut!
Je pense que réaliser un OS sans failles est utopique

100 % d'accord. On peut certifier qu'une certaine faille est absente, mais comme il existe une quasi-infinité de possibilités de failles, il n'est pas possible de certifier qu'on les a toutes éliminées, surtout celles qu'on ne connait pas encore.
Jean-Marc Blanc
Avatar de Mac LAK Mac LAK - Inactif https://www.developpez.com
le 20/08/2009 à 13:51
Citation Envoyé par granquet  Voir le message
ce micro noyau permet de faire tourner un autre noyau en host!
pour l'instant il permet de faire tourner Linux sur x86 et bientot sur ARM !
et la, ca deviens tres interessant

Uniquement si le micro-noyau seL4 permet de "détecter" les erreurs, en plus de les empêcher : sinon, ça n'offre aucun avantage de faire tourner un co-noyau avec, vu que le co-noyau en question pourrait planter allègrement sans même alerter le kernel seL4 !!
Avatar de pseudocode pseudocode - Rédacteur https://www.developpez.com
le 20/08/2009 à 14:29
Citation Envoyé par Mac LAK  Voir le message
Uniquement si le micro-noyau seL4 permet de "détecter" les erreurs, en plus de les empêcher : sinon, ça n'offre aucun avantage de faire tourner un co-noyau avec, vu que le co-noyau en question pourrait planter allègrement sans même alerter le kernel seL4 !!

Surtout que les hackers ne cherchent pas le "plantage" mais l'accès aux données.
Avatar de Mac LAK Mac LAK - Inactif https://www.developpez.com
le 20/08/2009 à 14:33
Citation Envoyé par pseudocode  Voir le message
Surtout que les hackers ne cherchent pas le "plantage" mais l'accès aux données.

J'avoue que je vois surtout l'aspect SdF dans ce micro-noyau plutôt que l'aspect "protection des données".
Avatar de Ubiquité Ubiquité - Membre confirmé https://www.developpez.com
le 20/08/2009 à 23:40
Citation Envoyé par millie  Voir le message

L'écriture des 7500 lignes de code a nécessité 4 ans, la preuve est composé de 10.000 théorèmes et de 200.000 lignes de preuves.

[...]

Vous en pensez-quoi ?

Ben qu'on est pas près de voir arriver la preuve formelle dans les processus industriel de création de logiciels ^^.
Avatar de amaury pouly amaury pouly - Membre actif https://www.developpez.com
le 21/08/2009 à 0:07
Je pense que les preuves assistés par ordinateurs ont surtout leur intérêt pour prouver que des algorithmes fonctionnent, ce qui peut être très importants pour certains logiciels cruciaux (avions par exemple).
Cela peut aussi être intéressants pour les compilateurs même si en pratique on ne pourra jamais prouver un compilo entier avec toutes les optimisations, ...
Mais c'est vrai que pour le génie logiciel, cela a peu d'intérêt. De même pour les OS, sauf peut-être des noyau sur des systèmes embarqués vitaux.
Avatar de Mac LAK Mac LAK - Inactif https://www.developpez.com
le 21/08/2009 à 8:10
Citation Envoyé par Ubiquité  Voir le message
Ben qu'on est pas près de voir arriver la preuve formelle dans les processus industriel de création de logiciels ^^.

C'est pour cela que l'on a inventé les outils d'analyse statique / dynamique, comme Coverity, Polyspace, etc.
Ce n'est pas aussi "bon" qu'une preuve formelle, mais c'est déjà mieux que rien.
Avatar de SpiceGuid SpiceGuid - Membre émérite https://www.developpez.com
le 23/08/2009 à 17:35
Citation Envoyé par millie
L'écriture des 7500 lignes de code a nécessité 4 ans, la preuve est composé de 10.000 théorèmes et de 200.000 lignes de preuves.

L'utilité de ceci est d'être sûr que certaines failles classiques ne peuvent être exploités.

Citation Envoyé par amaury pouly
Ce genre d'initiative est intéressante surtout pour la rechercher en preuves formelles.

Tout à fait d'accord. Ces nouveaux langages pour l'assistance de preuve fonctionnent à merveille sur les petits exemples jouets. Le but des développements plus ambitieux (certification de programmes réalistes et formalisation de gros théorèmes) c'est avant tout d'identifier les obstacles au passage à l'échelle. Ceci afin de concevoir la syntaxe, les abstractions et les automatisations qui permettront à ces langages de sortir des labos pour rencontrer des usages métiers (à commencer par les maths et la sécurité des personnes).

Mine de rien on assiste à la maturation d'un nouveau paradigme.
Avatar de Graffito Graffito - Expert éminent https://www.developpez.com
le 24/08/2009 à 22:02
Et est-ce qu'ils ont testé leurs tests ?

Excellente question.
Dans les normes aviation DO218-ED109, il est précisé que les logiciels de tests doivent être conçus avec les mêmes niveaux de qualité que les logciels testés . Ce qui est évidement absurde, vu que les outils de tests, qui sont en pratique plus complexes que les logiciels testés, doivent être eux-mèmes testés et ainsi de suite.

Quand j'ai soulevé le problème auprès de certains des rédacteurs de la norme ED109, ils ont éludé la question, en disant que c'était de la responsabilité des dévellopeurs de s'accomoder de cette prescription .
Avatar de amaury pouly amaury pouly - Membre actif https://www.developpez.com
le 25/08/2009 à 1:04
En pratique, on peut s'arranger pour que les outils de tests soient eux aussi certifiés et testés. Par exemple on peut écrire une version préliminaire réduite dans laquelle on prouve qu'une implémentation plus complète est correcte et ainsi de suite. On peut alors réduire les risques d'erreurs à des programmes les plus simples possibles. Bien entendu, on est jamais certain qu'il ne reste pas des bugs
Offres d'emploi IT
Architecte sécurité des systèmes d'information embarqués H/F
Safran - Ile de France - 100 rue de Paris 91300 MASSY
Ingénieur H/F
Safran - Ile de France - Moissy-Cramayel (77550)
Ingénieur intégration, validation, qualification du système de drone H/F
Safran - Ile de France - Éragny (95610)

Voir plus d'offres Voir la carte des offres IT
Contacter le responsable de la rubrique Débuter - Algorithmique