si ce n'est (si j'ai bien compris ce qui ce disait plus haut) : une absence de bugs mathematiquement prouvée.
Ne nous emballons pas.
Autant que je me souvienne (mais je jurerais pas non plus et j'ai super la flemme de remettre le nez dans les CC), en EAL5, il n'y a pas encore de "preuve de l'absence de bug" (càd de vérification formelle du code). C'est au niveau du design que se situe l'utilisation de méthodes (semi-)formelles, et ce qui est démontré c'est que la description super détaillée du design de bas niveau colle bien avec celle super détaillée aussi de plus haut niveau, qui elle colle bien avec les spécifications fonctionnelles super détaillées aussi et avec le modèle formel de sécurité qu'on a décidé d'implémenter. En gros, on s'assure avec un très fort degré de confiance que tout ce qui est prévu est bien pensé et bien fichu.
Par là dessus, l'implémentation elle est soumise à des tests très systématiques, ce qui n'est possible que grâce à tous nos super-détails énumérés ci-dessus. À ce niveau, on parle de test (semi-)formel, parcequ'ils ne sont pas juste fait suivant l'inspiration du programmeur mais peuvent être vraiment dérivés méthodiquement de la spec de chaque composant de bas niveau.
Mais la vérification du code (ou sa génération à partir du modèle prouvé, comme en B ou en Coq), c'est plutôt aux niveaux EAL6 et 7 que ça se fait vraiment. Et là, on est pas près de rencontrer un système de ce niveau de complexité amha.
[^] # Re: Mandrake n'est pas seul
Posté par tgl . En réponse à la dépêche Mandrakesoft retenue pour le développement d'un système d'exploitation ouvert de haute sécurité. Évalué à 4.
Ne nous emballons pas.
Autant que je me souvienne (mais je jurerais pas non plus et j'ai super la flemme de remettre le nez dans les CC), en EAL5, il n'y a pas encore de "preuve de l'absence de bug" (càd de vérification formelle du code). C'est au niveau du design que se situe l'utilisation de méthodes (semi-)formelles, et ce qui est démontré c'est que la description super détaillée du design de bas niveau colle bien avec celle super détaillée aussi de plus haut niveau, qui elle colle bien avec les spécifications fonctionnelles super détaillées aussi et avec le modèle formel de sécurité qu'on a décidé d'implémenter. En gros, on s'assure avec un très fort degré de confiance que tout ce qui est prévu est bien pensé et bien fichu.
Par là dessus, l'implémentation elle est soumise à des tests très systématiques, ce qui n'est possible que grâce à tous nos super-détails énumérés ci-dessus. À ce niveau, on parle de test (semi-)formel, parcequ'ils ne sont pas juste fait suivant l'inspiration du programmeur mais peuvent être vraiment dérivés méthodiquement de la spec de chaque composant de bas niveau.
Mais la vérification du code (ou sa génération à partir du modèle prouvé, comme en B ou en Coq), c'est plutôt aux niveaux EAL6 et 7 que ça se fait vraiment. Et là, on est pas près de rencontrer un système de ce niveau de complexité amha.