Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

Algorithmes et structures de données Discussion :

Noyau d'OS prouvé sans erreur par une équipe de recherche [News]


Sujet :

Algorithmes et structures de données

  1. #1
    Rédacteur

    Avatar de millie
    Profil pro
    Inscrit en
    juin 2006
    Messages
    7 013
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : juin 2006
    Messages : 7 013
    Points : 9 696
    Points
    9 696
    Par défaut Noyau d'OS prouvé sans erreur par une équipe de recherche
    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/
    Je ne répondrai à aucune question technique en privé

  2. #2
    Rédacteur
    Avatar de pseudocode
    Homme Profil pro
    Architecte système
    Inscrit en
    décembre 2006
    Messages
    10 061
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 47
    Localisation : France, Hérault (Languedoc Roussillon)

    Informations professionnelles :
    Activité : Architecte système
    Secteur : Industrie

    Informations forums :
    Inscription : décembre 2006
    Messages : 10 061
    Points : 15 768
    Points
    15 768
    Par défaut
    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.
    ALGORITHME (n.m.): Méthode complexe de résolution d'un problème simple.

  3. #3
    Rédacteur

    Homme Profil pro
    Comme retraité, des masses
    Inscrit en
    avril 2007
    Messages
    2 978
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 79
    Localisation : Suisse

    Informations professionnelles :
    Activité : Comme retraité, des masses
    Secteur : Industrie

    Informations forums :
    Inscription : avril 2007
    Messages : 2 978
    Points : 5 145
    Points
    5 145
    Par défaut
    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
    Calcul numérique de processus industriels
    Formation, conseil, développement

    Point n'est besoin d'espérer pour entreprendre, ni de réussir pour persévérer. (Guillaume le Taiseux)

  4. #4
    Membre expérimenté
    Avatar de granquet
    Profil pro
    Étudiant
    Inscrit en
    octobre 2005
    Messages
    1 201
    Détails du profil
    Informations personnelles :
    Localisation : France, Pyrénées Orientales (Languedoc Roussillon)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : octobre 2005
    Messages : 1 201
    Points : 1 398
    Points
    1 398
    Par défaut
    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?
    click my www
    ............|___
    ...................\
    .................._|_
    ..................\ /
    ..................."

  5. #5
    Rédacteur
    Avatar de pseudocode
    Homme Profil pro
    Architecte système
    Inscrit en
    décembre 2006
    Messages
    10 061
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 47
    Localisation : France, Hérault (Languedoc Roussillon)

    Informations professionnelles :
    Activité : Architecte système
    Secteur : Industrie

    Informations forums :
    Inscription : décembre 2006
    Messages : 10 061
    Points : 15 768
    Points
    15 768
    Par défaut
    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.
    ALGORITHME (n.m.): Méthode complexe de résolution d'un problème simple.

  6. #6
    Rédacteur

    Avatar de millie
    Profil pro
    Inscrit en
    juin 2006
    Messages
    7 013
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : juin 2006
    Messages : 7 013
    Points : 9 696
    Points
    9 696
    Par défaut
    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 ?
    Je ne répondrai à aucune question technique en privé

  7. #7
    Membre expérimenté
    Avatar de granquet
    Profil pro
    Étudiant
    Inscrit en
    octobre 2005
    Messages
    1 201
    Détails du profil
    Informations personnelles :
    Localisation : France, Pyrénées Orientales (Languedoc Roussillon)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : octobre 2005
    Messages : 1 201
    Points : 1 398
    Points
    1 398
    Par défaut
    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.
    click my www
    ............|___
    ...................\
    .................._|_
    ..................\ /
    ..................."

  8. #8
    Rédacteur
    Avatar de pseudocode
    Homme Profil pro
    Architecte système
    Inscrit en
    décembre 2006
    Messages
    10 061
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 47
    Localisation : France, Hérault (Languedoc Roussillon)

    Informations professionnelles :
    Activité : Architecte système
    Secteur : Industrie

    Informations forums :
    Inscription : décembre 2006
    Messages : 10 061
    Points : 15 768
    Points
    15 768
    Par défaut
    Ca implique qu'il faut écrire dans la spec "je ne veux pas de buffer overflow" ?
    ALGORITHME (n.m.): Méthode complexe de résolution d'un problème simple.

  9. #9
    En attente de confirmation mail

    Homme Profil pro
    Inscrit en
    juillet 2006
    Messages
    766
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 44
    Localisation : France, Haute Garonne (Midi Pyrénées)

    Informations forums :
    Inscription : juillet 2006
    Messages : 766
    Points : 1 219
    Points
    1 219
    Par défaut
    C'est quoi une spec ?

  10. #10
    Membre régulier

    Homme Profil pro
    Développeur Java
    Inscrit en
    novembre 2007
    Messages
    13
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 32
    Localisation : France, Loire Atlantique (Pays de la Loire)

    Informations professionnelles :
    Activité : Développeur Java
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : novembre 2007
    Messages : 13
    Points : 94
    Points
    94
    Par défaut
    Citation Envoyé par nicorama Voir le message
    C'est quoi une spec ?
    Une notion dépassée

  11. #11
    Membre habitué
    Profil pro
    Architecte logiciel
    Inscrit en
    décembre 2008
    Messages
    77
    Détails du profil
    Informations personnelles :
    Localisation : France, Hauts de Seine (Île de France)

    Informations professionnelles :
    Activité : Architecte logiciel

    Informations forums :
    Inscription : décembre 2008
    Messages : 77
    Points : 152
    Points
    152
    Par défaut
    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

  12. #12
    Futur Membre du Club
    Profil pro
    Inscrit en
    juin 2009
    Messages
    4
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : juin 2009
    Messages : 4
    Points : 8
    Points
    8
    Par défaut
    loool csperandio, c'est trop vrai

  13. #13
    Inactif  
    Avatar de Mac LAK
    Profil pro
    Inscrit en
    octobre 2004
    Messages
    3 893
    Détails du profil
    Informations personnelles :
    Âge : 45
    Localisation : France, Haute Garonne (Midi Pyrénées)

    Informations forums :
    Inscription : octobre 2004
    Messages : 3 893
    Points : 4 721
    Points
    4 721
    Par défaut
    Citation Envoyé par millie Voir le message
    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.
    Mac LAK.
    ___________________________________________________
    Ne prenez pas la vie trop au sérieux, de toutes façons, vous n'en sortirez pas vivant.

    Sources et composants Delphi sur mon site, L'antre du Lak.
    Pas de question technique par MP : posez-la dans un nouveau sujet, sur le forum adéquat.

    Rejoignez-nous sur : Serveur de fichiers [NAS] Le Tableau de bord projets Le groupe de travail ICMO

  14. #14
    Rédacteur
    Avatar de romaintaz
    Homme Profil pro
    Java craftsman
    Inscrit en
    juillet 2005
    Messages
    3 790
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 41
    Localisation : France, Yvelines (Île de France)

    Informations professionnelles :
    Activité : Java craftsman
    Secteur : Finance

    Informations forums :
    Inscription : juillet 2005
    Messages : 3 790
    Points : 7 700
    Points
    7 700
    Par défaut
    Et est-ce qu'ils ont testé leurs tests ?
    Nous sommes tous semblables, alors acceptons nos différences !
    --------------------------------------------------------------
    Liens : Blog | Page DVP | Twitter
    Articles : Hudson | Sonar | Outils de builds Java Maven 3 | Play! 1 | TeamCity| CitConf 2009
    Critiques : Apache Maven

  15. #15
    Membre régulier Avatar de ctiti60
    Homme Profil pro
    Développeur informatique
    Inscrit en
    octobre 2007
    Messages
    75
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 46
    Localisation : France, Oise (Picardie)

    Informations professionnelles :
    Activité : Développeur informatique

    Informations forums :
    Inscription : octobre 2007
    Messages : 75
    Points : 124
    Points
    124
    Par défaut
    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.

  16. #16
    Membre actif Avatar de amaury pouly
    Profil pro
    Inscrit en
    décembre 2002
    Messages
    157
    Détails du profil
    Informations personnelles :
    Âge : 30
    Localisation : France

    Informations forums :
    Inscription : décembre 2002
    Messages : 157
    Points : 215
    Points
    215
    Par défaut
    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.

  17. #17
    Membre éprouvé Avatar de s4mk1ng
    Homme Profil pro
    Administrateur systèmes et réseaux
    Inscrit en
    juillet 2008
    Messages
    535
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 26
    Localisation : France, Oise (Picardie)

    Informations professionnelles :
    Activité : Administrateur systèmes et réseaux
    Secteur : High Tech - Multimédia et Internet

    Informations forums :
    Inscription : juillet 2008
    Messages : 535
    Points : 1 181
    Points
    1 181
    Par défaut
    de toutes façon ils en trouveront tôt ou tard...
    Ph'nglui mglw'nafh Cthulhu R'lyeh wgah'nagl fhtagn

  18. #18
    Rédacteur

    Avatar de millie
    Profil pro
    Inscrit en
    juin 2006
    Messages
    7 013
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : juin 2006
    Messages : 7 013
    Points : 9 696
    Points
    9 696
    Par défaut
    Citation Envoyé par romaintaz Voir le message
    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 ...
    Je ne répondrai à aucune question technique en privé

  19. #19
    Candidat au Club
    Profil pro
    Inscrit en
    septembre 2008
    Messages
    2
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : septembre 2008
    Messages : 2
    Points : 2
    Points
    2
    Par défaut
    les failles , y en a toujours.

  20. #20
    Membre régulier Avatar de maitredede
    Homme Profil pro
    Pisseur de code
    Inscrit en
    mai 2006
    Messages
    59
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Nouvelle-Calédonie

    Informations professionnelles :
    Activité : Pisseur de code

    Informations forums :
    Inscription : mai 2006
    Messages : 59
    Points : 104
    Points
    104
    Par défaut
    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.

Discussions similaires

  1. Réponses: 6
    Dernier message: 20/11/2008, 16h55
  2. Réponses: 5
    Dernier message: 10/05/2008, 19h11
  3. Réponses: 2
    Dernier message: 10/05/2008, 18h53
  4. Background degradé sans passer par une image?
    Par j14z dans le forum Balisage (X)HTML et validation W3C
    Réponses: 7
    Dernier message: 28/03/2008, 16h02
  5. changer les valeurs graphique sans passer par une cellule
    Par mennix dans le forum Macros et VBA Excel
    Réponses: 5
    Dernier message: 06/11/2007, 20h56

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo