seL4 : Le premier système d'exploitation prouvé sans erreur par une équipe de recherche Australienne (le NICTA)
Le 2009-08-18 10:07:56, 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/
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/
-
pseudocodeRédacteurJe pense qu'il est temps d'arrêter d'utiliser des langages de programmations dans lesquels les "buffers overflow" sont possibles.le 18/08/2009 à 11:23
-
FR119492RédacteurSalut!
L'utilité de ceci est d'être sûr que certaines failles classiques ne peuvent être exploités.
Jean-Marcle 18/08/2009 à 11:34 -
granquetMembre expérimenté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?le 18/08/2009 à 13:11 -
pseudocodeRédacteurLe 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.le 18/08/2009 à 13:33 -
millieRédacteurle 18/08/2009 à 14:08
-
granquetMembre expérimenté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 lucideThis 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. le 19/08/2009 à 14:08 -
pseudocodeRédacteurCa implique qu'il faut écrire dans la spec "je ne veux pas de buffer overflow" ?le 19/08/2009 à 14:18
-
nicoramaEn attente de confirmation mailC'est quoi une spec ?le 19/08/2009 à 23:00
-
c0r3nt1nMembre régulierle 19/08/2009 à 23:04
-
csperandioMembre habituéMode humour ON
Une spécification fonctionnelle est un document dans lequel on exprime ce qui doit faire l'application. C'est un document vite lu par les développeurs qui en oublient la moitié ensuite.
Une spécification technique est un document que le développeur écrit comment il a développé son programme pour répondre à la spéc fonctionnelle. Ce document est ensuite oublié et tout le monde met le nez dans le codele 19/08/2009 à 23:29