Discussion:CertiKOS
Relecture
[modifier le code]Commentaires généraux
[modifier le code]l'article pourrait être un peu bleui. (0xA ZERTY (discuter) 21 janvier 2019 à 17:52 (CET))
- Bonjour,
- Merci pour cette suggestion, mais pourriez vous préciser? Auriez vous repérer des mots qui mériteraient d'être mis en lien avec d'autres pages Wikipédia?
- cordialement, TV974 (discuter) 22 janvier 2019 à 09:47 (CET)TV974
- ok, je vais donc préciser dans chaque section ce qui de mon point de vue devrai être bleui.
- en terme général dans chaque section un terme doit être bleui si il n'a pas étais précédemment bleui dans la même section car un lecteur ne va pas forcement avoir une lecture séquentielle.
- (0xA ZERTY (discuter) 25 janvier 2019 à 13:32 (CET))
- Bonjour,j'ai rajouté des liens dans la page afin de "bleuir" un peu, mais afin de ne pas "alourdir" la page, je n'ai pas mis en bleu tout les mots ou termes en doublons dans un paragraphe ou une sous-partie. Je fais un rappel en début de paragraphe sur le mot en question, mais je ne bleui pas le reste du paragraphe avec les mêmes mots. --Cyril Kramp (discuter) 28 janvier 2019 à 14:23 (CET)
Commentaires détaillés
[modifier le code]Introduction
[modifier le code]les mots suivants devrait être bleui :
Université Yale : https://fr.wikipedia.org/wiki/Universit%C3%A9_Yale
Connecticut : https://fr.wikipedia.org/wiki/Connecticut
Certification : https://fr.wikipedia.org/wiki/Certification
Sémantique => Sémantique des langages de programmation : https://fr.wikipedia.org/wiki/S%C3%A9mantique_des_langages_de_programmation
Compilation (informatique) : https://fr.wikipedia.org/wiki/Compilateur
Noyau (informatique) : https://fr.wikipedia.org/wiki/Noyau_de_syst%C3%A8me_d%27exploitation
Processeurs multi-cœur : https://fr.wikipedia.org/wiki/Microprocesseur_multi-c%C5%93ur
(0xA ZERTY (discuter) 25 janvier 2019 à 13:34 (CET))
- Merci nous implémenterons ces suggestions
- TV974 (discuter) 25 janvier 2019 à 16:59 (CET)TV974
Motivations et enjeux
[modifier le code]les mots suivants devrait être bleui :
Noyau (informatique) : https://fr.wikipedia.org/wiki/Noyau_de_syst%C3%A8me_d%27exploitation
Hyperviseur : https://fr.wikipedia.org/wiki/Hyperviseur
logiciels/programmes : https://fr.wikipedia.org/wiki/Programme_informatique
code : https://fr.wikipedia.org/wiki/Code_source
Linux : https://fr.wikipedia.org/wiki/Linux
sécurisés => Sécurité des systèmes d'information : https://fr.wikipedia.org/wiki/S%C3%A9curit%C3%A9_des_syst%C3%A8mes_d%27information
bugs : https://fr.wikipedia.org/wiki/Bug_(informatique)
L'exploitation : https://fr.wikipedia.org/wiki/Exploit_(informatique)
données : https://fr.wikipedia.org/wiki/Donn%C3%A9e_(informatique)
correction fonctionnelle : https://fr.wikipedia.org/wiki/Correction_(logique)
Processeurs multi-cœur : https://fr.wikipedia.org/wiki/Microprocesseur_multi-c%C5%93ur
(0xA ZERTY (discuter) 25 janvier 2019 à 14:05 (CET))
- Merci nous implémenterons ces suggestions cependant certains liens sont redondants je me questionne sur l'intérêt
- TV974 (discuter) 25 janvier 2019 à 17:09 (CET)TV974
les mots suivants devrai être en italique
"The Linux Foundation"
"International Data Corporation"
"The Transparency Market Research"
(0xA ZERTY (discuter) 25 janvier 2019 à 14:05 (CET))
- Merci nous implémenterons ces suggestions nous les implémenterons.
- TV974 (discuter) 25 janvier 2019 à 17:09 (CET)TV974
(voir liens externes: "Bulletins d'informations, failles de sécurités") doit être dans les références
(0xA ZERTY (discuter) 25 janvier 2019 à 14:05 (CET))
"exergue" est un mot compliqué pour pas grand chose.
(0xA ZERTY (discuter) 25 janvier 2019 à 14:05 (CET))
- Je prends note de votre opinion.
- TV974 (discuter) 25 janvier 2019 à 17:09 (CET)TV974
Dans le début du second paragraphe, vous citez les problèmes que peuvent avoir les systèmes d'exploitation en mettant à chaque fois en source un exemple du problème qui est survenu. Mais vous n'en n'avez pas mis pour les interactions avec d'autres logiciels. Pourriez vous en rajouter pour que l'on puisse voir les problèmes que ça peut impliquer comme avec les défauts de conception et l'exemple de Toyota ? IratanRG (discuter) 30 janvier 2019 à 09:23 (CET)
- Bonjour
- https://www.olenick.com/olenick-blog/176-infamous-software-bugs-at-t-switches.html je m'étais inspiré de ça. Je vais le rajouter en lien externe.
- TV974 (discuter) 1 février 2019 à 12:30 (CET)TV974
La philosophie de Certikos
[modifier le code]les mots suivants devrait être bleui :
Système d'exploitation : https://fr.wikipedia.org/wiki/Syst%C3%A8me_d%27exploitation
programmes : https://fr.wikipedia.org/wiki/Programme_informatique
matériel de l'ordinateur : https://fr.wikipedia.org/wiki/Mat%C3%A9riel_informatique
Noyau (informatique) : https://fr.wikipedia.org/wiki/Noyau_de_syst%C3%A8me_d%27exploitation
méthode formelle : https://fr.wikipedia.org/wiki/Correction_(logique)
(0xA ZERTY (discuter) 25 janvier 2019 à 14:13 (CET))
- Merci nous implémenterons ces suggestions cependant certains liens sont redondants je me questionne sur l'intérêt
- TV974 (discuter) 25 janvier 2019 à 17:18 (CET)TV974
Certification du Noyau
[modifier le code]les mots suivants devrait être bleui :
Système d'exploitation : https://fr.wikipedia.org/wiki/Syst%C3%A8me_d%27exploitation
correction fonctionnelle : https://fr.wikipedia.org/wiki/Correction_(logique)
formules logiques : https://fr.wikipedia.org/wiki/Formule_logique
Noyau (informatique) : https://fr.wikipedia.org/wiki/Noyau_de_syst%C3%A8me_d%27exploitation
contexte utilisateur : https://fr.wikipedia.org/wiki/Exp%C3%A9rience_utilisateur
(0xA ZERTY (discuter) 25 janvier 2019 à 14:40 (CET))
- Merci nous implémenterons ces suggestions cependant certains liens sont redondants je me questionne sur l'intérêt.
- La suggestion du lien suivant https://fr.wikipedia.org/wiki/Exp%C3%A9rience_utilisateur pour illustrer "contexte utilisateur" ne me parait pas approprié. Il s'agit là de 2 choses différentes. le Liens plus adéquat serait Espace utilisateur
- TV974 (discuter) 25 janvier 2019 à 17:18 (CET)TV974
pourquoi cette phrase est entre parenthèse ?
(CertiKOS permet de certifier qu'entre chaque couches de fonctionnement, les fonctions à exécuter soient réalisées de manière attendue. Il ne doit pas y avoir d'altération d'état entre le niveau N et le niveau N-1.)
(0xA ZERTY (discuter) 25 janvier 2019 à 14:40 (CET))
- Effectivement il s'agit d'un mémo qui traine, nous allons si nous le reformulons pour l'intégrer ou le supprimer
- TV974 (discuter) 25 janvier 2019 à 17:18 (CET)TV974
Vous affirmez dans le début de cette partie que lorsque l'on veut une certaine qualité de preuve, la preuve devient plus difficile à fournir. Pourriez vous ajouter une citation à cette affirmation ?
Bien à vous,
IratanRG (discuter) 30 janvier 2019 à 09:53 (CET)
- Bonjour
- je ne dispose pas de citation précise pour cette phrase introductive. Je me suis inspiré de l'histoire autour du théorème des 4 couleurs pour la rédiger. J'ai réussi à trouver un lien aujourd'hui qui retrace une chronologie des différentes tentatives de preuve sur ce théorème => https://controverses.github.io/4CTpreuvesinformatiques/#2004 . L'objectif était pour moi en quelques lignes introductives de souligner l'importance de la qualité de la preuve et sur quoi cette dernière doit reposer. Aujourd'hui, le fait quelle soit vérifiable par machine est considéré comme un gage de qualité.
- Je vais dans premiers temps corriger les "ON".
- Ce passage introductif devrait il selon vous être supprimer?
TV974 (discuter) 1 février 2019 à 10:46 (CET)TV974
Spécifications profondes
[modifier le code]les mots suivants devrait être bleui :
Système d'exploitation : https://fr.wikipedia.org/wiki/Syst%C3%A8me_d%27exploitation
pilotes : https://fr.wikipedia.org/wiki/Pilote_informatique
Hyperviseur : https://fr.wikipedia.org/wiki/Hyperviseur
programmes : https://fr.wikipedia.org/wiki/Programme_informatique
correction : https://fr.wikipedia.org/wiki/Correction_(logique)
Noyau (informatique) : https://fr.wikipedia.org/wiki/Noyau_de_syst%C3%A8me_d%27exploitation
(0xA ZERTY (discuter) 25 janvier 2019 à 15:02 (CET))
- Merci nous implémenterons ces suggestions cependant certains liens sont redondants je me questionne sur l'intérêt
- TV974 (discuter) 25 janvier 2019 à 17:18 (CET)TV974
cette phrase peut être reformuler car tentative de vulgarisation devrait être dans la phrase puisque la tentative est réussi :
"On peut considérer les exemples suivants (tentative de vulgarisation)"
=> on peut vulgariser le concept de spécification avec les exemples suivants:
(0xA ZERTY (discuter) 25 janvier 2019 à 15:02 (CET))
- Merci nous implémenterons cette suggestion.
- TV974 (discuter) 25 janvier 2019 à 17:18 (CET)TV974
À mon avis, il serait plus judicieux de mettre l'exemple sans expliquer que l'on vulgarise car c'est du méta discours. Bien à vous,
IratanRG (discuter) 30 janvier 2019 à 09:59 (CET)
- Bonjour,
- remarque non pertinente, des modifications ont déjà été réalisées le: 25 janvier 2019 à 17:22 TV974 (discuter | contributions) m . . (39 385 octets) (+13) . . (→Spécifications profondes : Suppression du ON et reformulation "Il possible de représenter le concept de spécification avec les exemples suivants :")
- TV974 (discuter) 30 janvier 2019 à 12:10 (CET)TV974
- Bonjour,
- Quand je suis sur la page wikipédia, je ne vois malheureusement pas votre modification, d'où la présence de ma remarque. Désolé si cela a déjà été modifié
- Bien à vous,
- IratanRG (discuter) 30 janvier 2019 à 13:35 (CET)
Certification du code informatique: CompCertX
[modifier le code]L'assembleur n'est-il pas aussi un langage de programmation ? Pourquoi l'excluez vous en écrivant "dans un langage de programmation (ex : langage C) et/ou en assembleur" ? De plus, un exemple de langage n'est pas forcément nécessaire à mon avis. Serait il possible également d'ajouter une citation pour ces affirmations ? Bien à vous,
IratanRG (discuter) 30 janvier 2019 à 09:41 (CET)
- Bonjour,
- il s'agit là d'une mauvaise interprétation, mais ma phrase doit être ambigüe.
- Adaptations possibles:
- * dans un langage de programmation C et/ou en assembleur
- * dans un langage de programmation C et/ou en langage de programmation assembleur
- la citation suivante peut illustrer le propos: "seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler."
- * (en) G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T Sewell, H. Tuch et S. Winwood, « seL4: Formal Verification of an OS Kernel », the Association for Computing Machinery, (ISBN 978-1-60558-752-3, DOI 10.1145/1629575.1629596) page 1
- TV974 (discuter) 30 janvier 2019 à 11:52 (CET)TV974
Implémentation de CertiKOS
[modifier le code]Une phrase d'introduction pour présenter cette section serait à mon avis une bonne idée Bien à vous,
IratanRG (discuter) 30 janvier 2019 à 09:46 (CET)
- Bonjour
- Merci pour cette remarque nous réfléchissons à son application.
- TV974 (discuter) 1 février 2019 à 12:32 (CET)TV974
Au travers d'un Hyperviseur Certifié
[modifier le code]Bonjour,
Il n'y a pas de référence sur ce que vous avancez dans cette partie. Est ce du à une redondance des références avec ce qui a été dit dans les sections précédentes ou à un manque de source disponible sur cette partie ?
IratanRG (discuter) 29 janvier 2019 à 08:40 (CET)
- Bonjour, pour cette partie les informations citées sont principalement tirées de la publication des chercheurs. Je vais faire le nécessaire afin de sourcer un peu plus cette partie avec des liens externes.--Cyril Kramp (discuter) 30 janvier 2019 à 09:04 (CET)
les mots suivants devrait être bleui :
virtualisation : https://fr.wikipedia.org/wiki/Virtualisation
RAM : https://fr.wikipedia.org/wiki/M%C3%A9moire_vive
Disques : https://fr.wikipedia.org/wiki/Disque_dur
Interfaces : https://fr.wikipedia.org/wiki/Interface_(informatique)
(0xA ZERTY (discuter) 30 janvier 2019 à 14:10 (CET)).
le paragraphe "Allocation Interfaces :" semble parler que d'interfaces réseau
(0xA ZERTY (discuter) 30 janvier 2019 à 14:10 (CET)).
Au travers d'un Noyau Certifié: mCertiKOS, mC2
[modifier le code]le premier paragraphe n'a pas de source