Discussion :

[millie]

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/

[pseudocode]

Vous en pensez-quoi ?

Je pense qu'il est temps d'arrêter d'utiliser des langages de programmations dans lesquels les "buffers overflow" sont possibles.

[FR119492]

Salut!

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

Ne te fais pas de soucis: des failles, les gens en trouveront d'autres!
Jean-Marc

[granquet]

que l'on m'arrete si je me trompe:
-on as une spec
-on as un code du noyau en C
-on as un code en Haskell qui prouve que le code C repond bien a la spec

on en deduis que le code C correspond bien a la spec. jusque la tout vas bien ...

mais qui me prouve que la spec est juste?

[pseudocode]

mais qui me prouve que la spec est juste?

Le jour ou on pourra prouver formellement qu'une spec est "juste", on pourra taper les specs directement dans eclipse, avec complétion/correction à la volée.

En attendant, les specs sont aux mieux relue/revues (non formellement) et considérées comme la source de vérité absolue.

- Oui monsieur, le premier item du menu Démarrer est "Arrêter...". C'est écrit dans la spec.

[millie]

mais qui me prouve que la spec est juste?

Mais qu'est-ce qu'une spéc juste ?

[granquet]

le mot "juste" est clairement mal choisi;

je suis tombe sur cette page (je trouve leur site pas vraiment clair quand meme, mais passons):
http://ertos.nicta.com.au/research/l...fied/proof.pml

c'est tres interessant, accessible et surtout pour une fois ca parait completement lucide

This doesn't sound like much, but it is a very strong formal statement, called functional correctness. A cynic might say: proofs like this only show that every fault in the specification has been precisely implemented in C. This is true, the above statement does not exclude this problem. But: at some point you have to say what you want (the "abstract specification") and that is what you get.

[Mac LAK]

Vous en pensez-quoi ?

En soi, c'est intéressant, mais hélas limité dans ses applications concrètes je pense :

• Un micro-noyau est en général dédié à des systèmes très réduits et/ou critiques.
• Or, ces systèmes sont souvent isolés et fonctionnent dans un environnement connu et déterminé.
• Dans les systèmes plus ouverts, on utilise en général des tonnes de librairies / applications au dessus du noyau.
• Et ces applications, elles, ne sont hélas pas certifiées...

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... Même s'ils ne sont certes pas prouvés formellement, ils ont malgré tout passé des normes extrêmement restrictives tout en fournissant un ensemble d'API et de services très complet.

Après, si le noyau est capable de détecter des comportements anormaux de ses applications et donc de déclencher un watchdog, là c'est nettement plus intéressant et applicable à court terme. Par exemple, s'il est capable de détecter un buffer overflow (et donc, potentiellement, un bug) tout en l'interdisant, c'est une fonctionnalité qui pourrait se révéler très utile.

[romaintaz]

Et est-ce qu'ils ont testé leurs tests ?

[millie]

Et est-ce qu'ils ont testé leurs tests ?

En théorie, tu n'as pas besoin de tester. En pratique, tu as des limitations liées au langage (et au compilateur) ce qui fait qu'il peut y avoir quand même des bugs ...

[ctiti60]

Je ne suis pas du tout un spécialiste de ce domaine. Je pense qu'effectivement c'est intéressant pour des domaines bien spécifiques ou universitaires.

Par contre, dans le monde industriel, j'ai peur qu'une telle application ne soit pas assez réactive. Si l'on veut corriger une nouvelle faille ou faire ne serait-ce qu'une petite modication. Combien de temps cela va prendre ? Il va falloir tout retester (bon c'est plutôt bien), mais peut-être ajouter des théorèmes en plus + rajouter les tests corerspondants.

[amaury pouly]

Cette initiative me rappelle une plus ancien où Xavier Leroy a prouvé formellement un compilateur pour un sous-ensemble du C vers une machine abstraite. Ce genre d'initiative est intéressante surtout pour la rechercher en preuves formelles.

[s4mk1ng]

de toutes façon ils en trouveront tôt ou tard...

[Hunter_H]

les failles , y en a toujours.

[maitredede]

Bonjour,

(humour on)

La première source de faille se situe en la chaise et le clavier.

Les specs, c'est pour justifier la déforestation.

(humour off)

Concevoir une spec "juste" reviens à compter combien il y a de molécules d'eau sur Terre.

Je pense que réaliser un OS sans failles est utopique, car si la faille n'est pas dans l'OS, elle sera dans le proc, la carte mère, le disque dur... Il suffit qu'un électron saute d'une piste à l'autre pour provoquer une erreur.

On pourra toujours dire "mon OS est certifié sans failles", mais ça sera toujours "sans failles connus" et on ne pourra jamais atteindre le zéro failles absolu. On ne pourra que s'en approcher.

(humour on)

Il n' a qu'a voir dans les filmes Transformers la vitesse à laquelle les systèmes surprotégés de l'armée se font piratés.

[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

[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

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