ou certifier qu'une partie/la plupart du code est correct.
Même ça c'est impossible à faire. Je suis pas un expert mais suffit d'avoir pratiquer un peu les méthodes formelles (type langage B) pour comprendre la complexité qu'il y a pour prouver le comportement d'un programme de quelques dizaines de lignes. Et encore, c'est fait avec des outils adaptés (langage formelle avec outil de preuve).
Alors maintenant si tu passes à quelques centaines de lignes (en imaginant que tu regardes que le bloc le plus critique), qu'en plus c'est codé en C (langage à la sémantique plus que douteuse), et qu'il faille en plus s'imaginer que beaucoup de bugs/failles/backdoor n'apparaissent que dans des conditions bien précises qui impliquent bien d'autres chose que le code source (le compilateur, le linker, le kernel qui exécute, les libs associées) : oui, on peut en conclure qu'avoir le code source n'apporte au final quasiment rien.
Au final les solutions les plus adaptées pour analyser le comportement du programme resterons les mêmes que pour les applications "propriétaires" : non pas l'humain/reviewer devant le code source mais des outils qui analysent le comportement du binaire (une fois qu'on a mis toute la chaîne compilo, linker et contexte d'exécution).
Si on a inventé la compilation, c'est pour traduire ce que dit l'humain en un code compréhensible par... un autre code/machine. L'analyse est bien plus efficace - et pertinente puisqu'incluant toute les maillons de la chaîne de compilation - par des outils binaires sur un autre binaire que sur un code source.
[^] # Re: Et tu aurais voulu qu'ils fassent quoi d'autre ?
Posté par TImaniac (site web personnel) . En réponse au journal Microsoft : pbpg a-t-il eu une attaque ? "Votre vie privée est notre priorité". Évalué à 3.
Même ça c'est impossible à faire. Je suis pas un expert mais suffit d'avoir pratiquer un peu les méthodes formelles (type langage B) pour comprendre la complexité qu'il y a pour prouver le comportement d'un programme de quelques dizaines de lignes. Et encore, c'est fait avec des outils adaptés (langage formelle avec outil de preuve).
Alors maintenant si tu passes à quelques centaines de lignes (en imaginant que tu regardes que le bloc le plus critique), qu'en plus c'est codé en C (langage à la sémantique plus que douteuse), et qu'il faille en plus s'imaginer que beaucoup de bugs/failles/backdoor n'apparaissent que dans des conditions bien précises qui impliquent bien d'autres chose que le code source (le compilateur, le linker, le kernel qui exécute, les libs associées) : oui, on peut en conclure qu'avoir le code source n'apporte au final quasiment rien.
Au final les solutions les plus adaptées pour analyser le comportement du programme resterons les mêmes que pour les applications "propriétaires" : non pas l'humain/reviewer devant le code source mais des outils qui analysent le comportement du binaire (une fois qu'on a mis toute la chaîne compilo, linker et contexte d'exécution).
Si on a inventé la compilation, c'est pour traduire ce que dit l'humain en un code compréhensible par... un autre code/machine. L'analyse est bien plus efficace - et pertinente puisqu'incluant toute les maillons de la chaîne de compilation - par des outils binaires sur un autre binaire que sur un code source.