Discussion:CertiKOS

Relecture

Commentaires généraux

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

Introduction

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

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

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

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

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

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,‎ octobre 2009 (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

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é

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)

IOMMU : https://fr.wikipedia.org/wiki/Gestionnaire_de_m%C3%A9moire_virtuelle#Contre-mesure_%C3%A0_l'attaque_DMA_:_IOMMU

(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

le premier paragraphe n'a pas de source

(0xA ZERTY (discuter) 30 janvier 2019 à 14:06 (CET)).