Une exagération très légère... Si le langage choisi (F7 pour le travail de Prosecco) est bien fait, toutes les failles d'implémentation devraient être décelées.
Non, c'est clairement exagéré. Toutes celles pour lesquelles on a écrit des "preuves". Une approche formelle ne garantie rien "magiquement". Par exemple, dans mitls, il n'y a pas de modélisation explicite du temps, donc on ne peut rien prouver sur les "timings attacks" (ce qui ne veut pas dire pour autant que leur implémentation est incorrecte de ce point de vue là).
L'autre question évidemment est la possibilité d'embedder ça dans les différents logiciels, je ne suis pas trop sûr de l'interoparibilité de F7
[^] # Re: Implémentation prouvée
Posté par zul . En réponse au journal OpenSSL est mort, vive (le futur) LibreSSL. Évalué à 10.
Non, c'est clairement exagéré. Toutes celles pour lesquelles on a écrit des "preuves". Une approche formelle ne garantie rien "magiquement". Par exemple, dans mitls, il n'y a pas de modélisation explicite du temps, donc on ne peut rien prouver sur les "timings attacks" (ce qui ne veut pas dire pour autant que leur implémentation est incorrecte de ce point de vue là).
L'autre question évidemment est la possibilité d'embedder ça dans les différents logiciels, je ne suis pas trop sûr de l'interoparibilité de F7