Discussion :

[granquet]

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

[FR119492]

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

[Mac LAK]

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 !!

[pseudocode]

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.

[Mac LAK]

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".

[Ubiquité]

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 ^^.

[amaury pouly]

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.

[Mac LAK]

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.

[SpiceGuid]

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.

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.

[Graffito]

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 .

[amaury pouly]

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