« Ce n'est pas parce qu'un code répond à des contraintes formelles que tu peux en déduire que des gens sont fiables. »
Je n'ai jamais dit ça non. Juste que si tu a un outil pour prouver que leur code est bon selon certaines propriété, alors tu ne risque rien d'eux. Si tu peux prouver qu'un programme lit pas sur ton disque, ça veux pas dire que le programmeur est gentil, mais ça veut dire que ce programme ci ne fera pas cette attaque là.
«
- données == programmes
- test de Turing
- théorèmes d'indécidabilité
- etc.
»
Bah j'ai jamais dit que c'étaient des méthodes complètes. Les gens qui font de la vérif ou de l'analyses font tous des approximations pour rendre le problème décidable. Mais ce sont des approximations correctes, c'est à dire que si un prog passe le test c'est qu'il est bon, mais des prog bons peuvent echouer au test.
Exemple en java: tu es sûr que le code que tu executes est type safe (càd pas d'accès illégaux à la mémoire, pas de buffer overflow, etc.), mais il existe des programmes bytecode type safe qui ne passe pas les vérifications de la jvm. Ceci dit, le compilo java produit des programmes toujours vérifiables, ce qui prouve que l'incompletude n'est pas vraiment limitante.
[^] # Re: Premier BIOS TCPA/Palladium
Posté par tgl . En réponse à la dépêche Premier BIOS TCPA/Palladium. Évalué à 2.
Je n'ai jamais dit ça non. Juste que si tu a un outil pour prouver que leur code est bon selon certaines propriété, alors tu ne risque rien d'eux. Si tu peux prouver qu'un programme lit pas sur ton disque, ça veux pas dire que le programmeur est gentil, mais ça veut dire que ce programme ci ne fera pas cette attaque là.
«
- données == programmes
- test de Turing
- théorèmes d'indécidabilité
- etc.
»
Bah j'ai jamais dit que c'étaient des méthodes complètes. Les gens qui font de la vérif ou de l'analyses font tous des approximations pour rendre le problème décidable. Mais ce sont des approximations correctes, c'est à dire que si un prog passe le test c'est qu'il est bon, mais des prog bons peuvent echouer au test.
Exemple en java: tu es sûr que le code que tu executes est type safe (càd pas d'accès illégaux à la mémoire, pas de buffer overflow, etc.), mais il existe des programmes bytecode type safe qui ne passe pas les vérifications de la jvm. Ceci dit, le compilo java produit des programmes toujours vérifiables, ce qui prouve que l'incompletude n'est pas vraiment limitante.