IdentifiantMot de passe
Mot de passe oublié ?Je m'inscris ! (gratuit)

Vous êtes nouveau sur Developpez.com ? Créez votre compte ou connectez-vous afin de pouvoir participer !

Vous devez avoir un compte Developpez.com et être connecté pour pouvoir participer aux discussions.

Vous n'avez pas encore de compte Developpez.com ? Créez-en un en quelques instants, c'est entièrement gratuit !

Si vous disposez déjà d'un compte et qu'il est bien activé, connectez-vous à l'aide du formulaire ci-dessous.

Identifiez-vous
Identifiant
Mot de passe
Mot de passe oublié ?
Créer un compte

L'inscription est gratuite et ne vous prendra que quelques instants !

Je m'inscris !

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

Le , par millie
30 commentaires

16PARTAGES

0  0 
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 lu gratuitement 849 articles depuis plus d'un an.
Soutenez le club developpez.com en souscrivant un abonnement pour que nous puissions continuer à vous proposer des publications.

Une erreur dans cette actualité ? Signalez-nous-la !

30 commentaires
Commenter Signaler un problème
pseudocode
Avatar de pseudocode
Rédacteur https://www.developpez.com
Le 18/08/2009 à 11:23
Citation Envoyé par millie Voir le message
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.
0  0 
FR119492
Avatar de FR119492
Rédacteur https://www.developpez.com
Le 18/08/2009 à 11:34
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
0  0 
granquet
Avatar de granquet
Membre expérimenté https://www.developpez.com
Le 18/08/2009 à 13:11
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?
0  0 
pseudocode
Avatar de pseudocode
Rédacteur https://www.developpez.com
Le 18/08/2009 à 13:33
Citation Envoyé par granquet Voir le message
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.
0  0 
millie
Avatar de millie
Rédacteur https://www.developpez.com
Le 18/08/2009 à 14:08
Citation Envoyé par granquet Voir le message

mais qui me prouve que la spec est juste?
Mais qu'est-ce qu'une spéc juste ?
0  0 
granquet
Avatar de granquet
Membre expérimenté https://www.developpez.com
Le 19/08/2009 à 14:08
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.
0  0 
pseudocode
Avatar de pseudocode
Rédacteur https://www.developpez.com
Le 19/08/2009 à 14:18
Ca implique qu'il faut écrire dans la spec "je ne veux pas de buffer overflow" ?
0  0 
nicorama
Avatar de nicorama
En attente de confirmation mail https://www.developpez.com
Le 19/08/2009 à 23:00
C'est quoi une spec ?
0  0 
c0r3nt1n
Avatar de c0r3nt1n
Membre régulier https://www.developpez.com
Le 19/08/2009 à 23:04
Citation Envoyé par nicorama Voir le message
C'est quoi une spec ?
Une notion dépassée
0  0 
csperandio
Avatar de csperandio
Membre habitué https://www.developpez.com
Le 19/08/2009 à 23:29
Citation Envoyé par nicorama Voir le message
C'est quoi une spec ?
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 code
0  0 
Commenter Signaler un problème