Discussion:Noyau de système d'exploitation formellement prouvé

Bonjour,

Étudiants en Master2 TIIR à l'université de Lille1, nous avons été amenés à rédiger un article dans le cadre du Projet Informatique 2.0 initié par notre université. Notre article Noyau de système d'exploitation formellement prouvé a été rédigé par Mme Narjis Taoufik, M.Mohamed El alaoui najib, M.Loik Demons, M.Lahcene Abdelhak et encadré par le professeur Gilles Grimaud.N'hésitez pas à faire des remarques.

Cordialement.

--LahceneTiir (discuter) 9 janvier 2017 à 08:23 (CET) --Simo.93 (discuter) 11 janvier 2017 à 11:45 (CET)

Suite aux retours sur les fautes d'orthographe, une relecture de l'article a été faite et normalement, toutes les fautes ont été corrigées. N'hésitez pas à nous dire s'il en reste encore. Dans le cas contraire, nous retirerons le bandeau signalant les fautes.

--Tiir IIR (discuter) 19 janvier 2017 à 10:05 (CET)

Remarques globales sur l'article

Corriger les fautes d'orthographe/grammaire qui parsèment l'article (je n'en fais pas la liste exhaustive, ce n'est pas le but).
Beaucoup plus de ressources bibliographiques que de références au dites-ressources. Elles doivent pouvoir être utilisées pour compléter l'article et sourcer ce qui ne l'est pas déjà.

Résumé

"[...] on parle d’outils comme Spin ou ComFoRT qui sont des models checkeurs ou alors via des langages formels comme Hasquel ou Coq." : Hasquel n'existe pas. Il était sûrement question d'Haskell.
Haskell et Coq ne me semblent pas vraiment des langages formels, en tout cas pas au sens mathématique du terme.

Généralités

Définitions

Pas de précision sur ce que l'on cherche à prouver dans un noyau ? Ça peut être l'absence de "bugs" ou de failles de sécurité, ou alors la conformité à une spécification comme le respect strict de contraintes (par exemple temporelles) pour les noyaux temps-réel.

En effet, c'est une excellente remarque. As-tu trouvés dans les sources de quoi a discuter ce point ? As-tu l'impression qu'ils parlent de preuve de propriété temporelles (dans tes références ? dans l'article wikipédia ?) Gilles.Grimaud (discuter) 7 septembre 2017 à 17:44 (CEST)

Système d'exploitation

Article "Operating_system" en français et en meilleure forme.
Une seule source de renseignée.

 "Il est possible de pousser la robustesse et la sécurité au point de garantir l’absence de bugs ainsi que la présence de très hautes propriétés de sécurités, mais cela avec de très petits noyaux. En effet, il est inévitable d’avoir des erreurs dans un code informatique, par conséquent plus la taille du code est élevée, plus la possibilité d’avoir des erreurs est grande."

L'argument pour la preuve de petits noyaux semble plus être la complexité et la difficulté de la tâche (d'après la source avancée en tout cas).

 "Évidemment, la réduction parfois radicale de la taille des systèmes d'exploitation peut amener à une forte augmentation de la complexité"

Plutôt paradoxal et même faux si on se réfère toujours à la même source.

Méthodes formelles

Avec juste un lien vers un article sur le sujet, cette section n'a pas lieu d'être. Expliquer le rôle des méthodes formelles dans les preuves. En lien avec la méthode B. — Le message qui précède, non signé, a été déposé par Chtim (discuter), le 6 août 2017 à 22:53 (CEST)

Méthodes de vérifications

Vérification de modèles

La section parle, à juste titre, de formaliser le noyau sous forme de modèle. Comment ? Ajouter une partie sur la formalisation serait intéressant.
L'article sur le lien https://www.usenix.org/legacy/event/hotos05/final_papers_backup/tuch/tuch_html/index.html mentionne la méthode B.

Theorem proving

Titre à mettre en français ainsi que ces références. C'est d'autant plus justifié qu'il en est ainsi dans l'article pour "Proof-carrying code".
Lien mal mis en forme.
Aucune source pour appuyer, d'autant plus que certains passages, comme :

 "[...] cette méthode requiert plus d'interaction humaine, mais cela peut justement être sa force : cela permet de savoir que le système est correct mais aussi pourquoi."

sont loin d'être évidents.

Preuve par le code

Framework -> quadriciel ?
Aucune source pour appuyer cette section.

Exemple d'OS formellement prouvés

Un seul exemple ne mérite pas une partie complète. Si aucun autre exemple, la fusionner dans une autre partie (pas encore d'idée).
Limité au SeL4, il doit y avoir d'autres exemples de noyaux. La partie sur SeL4 est elle-même très modeste et pourrait être étoffée.

 "Il a subi la Worst Case Execution Time, cette dernière devenue indispensable dans la vérification des systèmes , a essayé de tester les limites du Sel4."

D'après l'article "OS Verification -- Now", on cherche à garantir un pire temps d'exécution (WCET) pour prouver la sûreté du noyau (actuellement je n'ai pas compris exactement de quoi il est question par ce terme). Mais en aucun cas ce n'est quelque chose que l'on fait subir à un noyau dans le cadre de la preuve. — Le message qui précède, non signé, a été déposé par Chtim (discuter), le 6 août 2017 à 23:11 (CEST)

exact, a moins de considérer que le calcul du WCET est assorti d'une preuve de CET, ce qui n'est pas le cas. Et donc ? Gilles.Grimaud (discuter) 7 septembre 2017 à 17:47 (CEST)

Intérêts de la vérification formelle d'OS

Très peu sourcée. Cet article peut servir : https://www.usenix.org/legacy/event/hotos05/final_papers_backup/tuch/tuch_html/index.html

On peut ajouter une section sur les limitations de la technique : l'article "It’s Time for Trustworthy Systems" relève la confiance dans les axiomes de la preuve (comme la fiabilité du matériel) et les différences entre le modèle et la réalité du système prouvé.

Je ne sais pas si l'on peut parler de limite de la technique (au sens ou la technique à laquelle tu fait référence est la preuve). Parce que toute preuve repose sur un système axiomatique... Donc il ne faut pas parler de Limite, mais plutôt de "sur-intreprétation" de ce qu'apporte une preuve de programme. Si on prouve que l'algo X a la propriété Y selon les axiome Z. Cela n'implique pas que l'implémentation X' à la propriété Y sans aucun doute. On peut (1) douter des axiomes Z. On peut (2) doute de l'implémentation de X... Tu peux trouver des publis qui traitent de (2) de la part de SeL4, et d'autre qui montre que dans le cas de SeL4 (1) est parfois faux... Cela contribuerait à une bonne amélioration de l'article. Gilles.Grimaud (discuter) 7 septembre 2017 à 17:57 (CEST)

La section "Coûts" semble hors-sujet. Entre autres :

 "Cela a entraîné une réduction significative du coût de la vérification formelle [...]"

L'amélioration des procédés et outils de la vérification formelle n'est pas un intérêt intrasèque de la vérification formelle (sauf si j'ai mal compris l'intention). — Le message qui précède, non signé, a été déposé par Chtim (discuter), le 6 août 2017 à 22:56 (CEST)

Discuter du cout (financier) qu'induit le fait de vouloir prouver un noyau de système d'exploitation est un aspect important. parceque produire un programme prouvé est bien plus complexe que produire un programme traditionnel. Cependant la section est... incompréhensible. Et en tout état de cause, cela n'est pas une sous section de la section "Intérêts de la vérification formelle d'OS". Gilles.Grimaud (discuter) 7 septembre 2017 à 17:57 (CEST)

Historique

Aucune source pour appuyer les données. Pas encore trouvés parmi les sources avancées.
Que signifient "Specs" et "Preuves" ? Que signifient les ratios ? Ce n'est pas clair.
Colonne "Approche" : que signifie HDM ?
Globalement le tableau n'est pas clair. Il faudrait mieux définir les titres de colonnes : "plus haut niveau" et "plus bas niveau" ne sont pas clairs mais semble être les niveaux d'abstraction du noyau qui ont été approchés, "specs" est très obscure. Le contenu de ces colonnes est confus (pour la catégorie "plus haut niveau", quel rapport entre "tâches isolés", "modèles de sécurité" et "ne crashe pas" ?).
--Chtim (discuter) 19 juillet 2017 à 00:40 (CEST)