Ce qui pointe un autre problème de B et consorts : si on prouve que le programme respecte ses spécifications, il faut encore réussir à montrer que la spécification est bien ce qu'on veut.
Et là, aucun outil formel ne permet de réduire le décalage entre la compréhension de l'utilisateur/client et la prose, très technique, de la spécif (prendre l'exemple des machines à voter, où la certif démontre normalement un tas de truc, qui finalement ne garantit en rien un vote fiable).
Bref, pour la sécurité, tous les maillons sont importants. Il faudrait d'ailleurs des méthodes formelles pour s'assurer qu'aucun maillon n'a été laissé de côté... (hum). J'imagine qu'en pratique il existe une certaine liste de points à vérifier, établie par l'expérience.
[^] # Re: personne ne parle
Posté par Aldoo . En réponse au journal Qu'est-ce qu'un langage sécurisé ?. Évalué à 5.
Et là, aucun outil formel ne permet de réduire le décalage entre la compréhension de l'utilisateur/client et la prose, très technique, de la spécif (prendre l'exemple des machines à voter, où la certif démontre normalement un tas de truc, qui finalement ne garantit en rien un vote fiable).
Bref, pour la sécurité, tous les maillons sont importants. Il faudrait d'ailleurs des méthodes formelles pour s'assurer qu'aucun maillon n'a été laissé de côté... (hum). J'imagine qu'en pratique il existe une certaine liste de points à vérifier, établie par l'expérience.