A voir également:
- Politique de sécurité et model checker
- Question de sécurité - Guide
- Votre appareil ne dispose pas des correctifs de qualité et de sécurité importants - Guide
- Mode securite - Guide
- Webcam model - Guide
- Clé de sécurité windows 10 gratuit - Guide
3 réponses
bonjour,
je vais essayer de répondre à ta question est pour ça je vais devoir préciser quelques choses.
Le model-checking (technique utilisant un model-checker) est un technique qui permet de prouver (au sens mathématique) qu'un modèle vérifie une propriété.
Par modèle je veux dire une représentation symbolique(souvent mathématique) de la réalité, comme je ne connais pas ton contexte professionnel je vais tenter plusieures approches (si tu connais déjà ce qu'est un modèle excuse-moi d'avance !) : on modélise les mouvements d'un pendule qui oscille par un système d'équations mathématiques, les pensées des gens par de méthode d'analyse cognitives (entre autre), les couleurs par leurs trois composantes (rouge-vert-bleu), un programme informatique par une machine à état (cf wikipédia), etc ...
La propriété quand à elle reflète une comportement, une relation que l'on souhaite voir toujours (ou au contraire jamais) vraie.(par exemple : la centrale atomique ne fonctionne pas si la porte est ouverte ...)
Par exemple on pourrait faire un modèle du programme windows Xp (tm) et demander au model-checker de vérifier la propriété aucune erreur critique n'arrive, là le model-cher répond par 2 solutions : oui (la propriété est vérifiée) ou non, dans ce cas il fournit un contre exemple : un suite d'évolution du système qui amène au non-respect de la propriété. Typiquement pour le cas ci-dessus il reviendrait surement avec le cas d'un logiciel mal utilisé, ou bien lorsque trop de logiciels tournent en même temps, on verrait alors dans la trace les différents logiciel ce lancer les uns après les autres jusqu'à arriver au moment ou win XP plante .
Bon maintenant (enfin) la réponse à ta question. Un model-checker permet de vérifier que la politique de sécurité testée vérifie certaine propriétés. En faisant les modèles des différentes parties de cette politique (accord des supérieurs, passe-droit, lecture d'empreinte digitale, ...) on peut ensuite demander au model-checker de vérifier certaines propriétés (la porte du coffre est toujours fermée entre minuit et 6 heure du amtin, un contrat ne peut être signé sans l'accord d'au moin 3 responsable de rang A ...).
La grande force du model-checker est qu'il est exhaustif, à savoir qu'il test toutes les possibilités avant de donner sa réponse. Une réponse positive signifie donc que la propriété est vraie, quelque soit le scénario suivit.
cependant il y a des limites à cette méthode, il est souvent difficile de définir les propriétés (elle doivent être écrite dans un langage que le model-checker comprend (cf LTL, CTL sur wikipédia), et de plus si cette propriété est mal définie le model-checker ne s'en rend pas compte (si on se trompe porte dans un propriété du style la porte YY ne s'ouvre que pendant 5 minute maximum). Une autre limitation est aussi le fait que beaucoup de model-checker ne donnent qu'un contre-exemple . Pour finir sur des modèle de grande taille
(par exemple le modèle de win XP) on à beaucoup de mal à calculer la réponse (imagine faire paris - pekin en trottinette ..).
Si jamais je n'ai pas totalement répondu à ta question , précise-là et je tenterai d'y répondre encore mieux !
je vais essayer de répondre à ta question est pour ça je vais devoir préciser quelques choses.
Le model-checking (technique utilisant un model-checker) est un technique qui permet de prouver (au sens mathématique) qu'un modèle vérifie une propriété.
Par modèle je veux dire une représentation symbolique(souvent mathématique) de la réalité, comme je ne connais pas ton contexte professionnel je vais tenter plusieures approches (si tu connais déjà ce qu'est un modèle excuse-moi d'avance !) : on modélise les mouvements d'un pendule qui oscille par un système d'équations mathématiques, les pensées des gens par de méthode d'analyse cognitives (entre autre), les couleurs par leurs trois composantes (rouge-vert-bleu), un programme informatique par une machine à état (cf wikipédia), etc ...
La propriété quand à elle reflète une comportement, une relation que l'on souhaite voir toujours (ou au contraire jamais) vraie.(par exemple : la centrale atomique ne fonctionne pas si la porte est ouverte ...)
Par exemple on pourrait faire un modèle du programme windows Xp (tm) et demander au model-checker de vérifier la propriété aucune erreur critique n'arrive, là le model-cher répond par 2 solutions : oui (la propriété est vérifiée) ou non, dans ce cas il fournit un contre exemple : un suite d'évolution du système qui amène au non-respect de la propriété. Typiquement pour le cas ci-dessus il reviendrait surement avec le cas d'un logiciel mal utilisé, ou bien lorsque trop de logiciels tournent en même temps, on verrait alors dans la trace les différents logiciel ce lancer les uns après les autres jusqu'à arriver au moment ou win XP plante .
Bon maintenant (enfin) la réponse à ta question. Un model-checker permet de vérifier que la politique de sécurité testée vérifie certaine propriétés. En faisant les modèles des différentes parties de cette politique (accord des supérieurs, passe-droit, lecture d'empreinte digitale, ...) on peut ensuite demander au model-checker de vérifier certaines propriétés (la porte du coffre est toujours fermée entre minuit et 6 heure du amtin, un contrat ne peut être signé sans l'accord d'au moin 3 responsable de rang A ...).
La grande force du model-checker est qu'il est exhaustif, à savoir qu'il test toutes les possibilités avant de donner sa réponse. Une réponse positive signifie donc que la propriété est vraie, quelque soit le scénario suivit.
cependant il y a des limites à cette méthode, il est souvent difficile de définir les propriétés (elle doivent être écrite dans un langage que le model-checker comprend (cf LTL, CTL sur wikipédia), et de plus si cette propriété est mal définie le model-checker ne s'en rend pas compte (si on se trompe porte dans un propriété du style la porte YY ne s'ouvre que pendant 5 minute maximum). Une autre limitation est aussi le fait que beaucoup de model-checker ne donnent qu'un contre-exemple . Pour finir sur des modèle de grande taille
(par exemple le modèle de win XP) on à beaucoup de mal à calculer la réponse (imagine faire paris - pekin en trottinette ..).
Si jamais je n'ai pas totalement répondu à ta question , précise-là et je tenterai d'y répondre encore mieux !
Bonjour,
J'ai eu le plaisir de lire la réponse que M.poulpe a envoyé précedement sur le model checking.
Je trouve qu'il a efficacement résumé se sujet qui est pourtant pas si évident à saisir.
J'aimerai à mon tour obtenir des informations (j'ai posté une question similaire, je tente ma chance ici aussi au cas où..)
Je parle de la vérification formelle en informatique qui est un domaine dans lequel s'inscrit le model checking.
N'Etant pas un spécialiste
Je souhaiterais obtenir des informations concernant les methodes formelles de verification dans le logiciel (plus précisement les logiciels critiques).
Je sais que le sujet est vaste. Mais , néansmoins, je souhaite obtenir quelques informations me permettant d'y voir plus clair dans cette brume de methodes et outils proposés (toutes plus obscures les unes que les autres).
J'aimerais saisir les différence qu'il y a entre:
Le model checking.
La Methode B.
Les assistants de preuve.
SCADE
etc.
Les informations que j'ai glané sur internet ne me permet pas de comprendre toutes les subtilités du domaine.
J'aimerais pouvoir saisir, quelle méthode ou quel outil s'applique dans quel domaine et à quel moment dans un cycle de développement logiciel.
voila, je pense qu'il s'agit d'une précision au sujet abordé.
Si quelqu'un à la force de me répondre pour ce sujet au combien barb(bip)ant captivant, je me ferais une joie de lire sa réponse avec la plus grande attention.
MERCI.
J'ai eu le plaisir de lire la réponse que M.poulpe a envoyé précedement sur le model checking.
Je trouve qu'il a efficacement résumé se sujet qui est pourtant pas si évident à saisir.
J'aimerai à mon tour obtenir des informations (j'ai posté une question similaire, je tente ma chance ici aussi au cas où..)
Je parle de la vérification formelle en informatique qui est un domaine dans lequel s'inscrit le model checking.
N'Etant pas un spécialiste
Je souhaiterais obtenir des informations concernant les methodes formelles de verification dans le logiciel (plus précisement les logiciels critiques).
Je sais que le sujet est vaste. Mais , néansmoins, je souhaite obtenir quelques informations me permettant d'y voir plus clair dans cette brume de methodes et outils proposés (toutes plus obscures les unes que les autres).
J'aimerais saisir les différence qu'il y a entre:
Le model checking.
La Methode B.
Les assistants de preuve.
SCADE
etc.
Les informations que j'ai glané sur internet ne me permet pas de comprendre toutes les subtilités du domaine.
J'aimerais pouvoir saisir, quelle méthode ou quel outil s'applique dans quel domaine et à quel moment dans un cycle de développement logiciel.
voila, je pense qu'il s'agit d'une précision au sujet abordé.
Si quelqu'un à la force de me répondre pour ce sujet au combien barb(bip)ant captivant, je me ferais une joie de lire sa réponse avec la plus grande attention.
MERCI.
