Je confirme que c'est de la fiction, car les productions scientifiques de Lamport et/ou de l'INRIA ne sont pas libres et c'est la guerre entre les labos de recherche. Cela dit, quand l'un a pondu l'article du siècle c'est une avancée qui profite à tous ! D'ailleurs Lamport a déjà bien fait avancer les choses dans le domaine de formalisation des protocoles distribués.
Pour ce qui est de la preuve, attention à ne pas confondre protocole et implémentation ! On peut très bien prouver plein de choses sur les protocoles SSL/TLS, ce qui n'empêchera pas leurs implémentations d'être buggées !
Je veux dire par là que dans la preuve du protocole, on suppose que les méthodes « send(message) » et « receive(message) » sont fiables. Si ce n'est pas le cas (comme pour SSL d'après ce que j'ai compris) la preuve ne tient plus :(
Je me rappelle avoir posé cette question à un chercheur dans le domaine de la vérification formelle : « What if the OS running your proved protocol didn't behave as expected ? Do you run your implementation on proved OS ? Do they run on proved CPU ?»
[^] # Re: On verra
Posté par vlamy . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 9. Dernière modification le 26 avril 2014 à 13:41.
Je confirme que c'est de la fiction, car les productions scientifiques de Lamport et/ou de l'INRIA ne sont pas libres et c'est la guerre entre les labos de recherche. Cela dit, quand l'un a pondu l'article du siècle c'est une avancée qui profite à tous ! D'ailleurs Lamport a déjà bien fait avancer les choses dans le domaine de formalisation des protocoles distribués.
Pour ce qui est de la preuve, attention à ne pas confondre protocole et implémentation ! On peut très bien prouver plein de choses sur les protocoles SSL/TLS, ce qui n'empêchera pas leurs implémentations d'être buggées !
Je veux dire par là que dans la preuve du protocole, on suppose que les méthodes « send(message) » et « receive(message) » sont fiables. Si ce n'est pas le cas (comme pour SSL d'après ce que j'ai compris) la preuve ne tient plus :(
Je me rappelle avoir posé cette question à un chercheur dans le domaine de la vérification formelle : « What if the OS running your proved protocol didn't behave as expected ? Do you run your implementation on proved OS ? Do they run on proved CPU ?»
Sa réponse :
« Fuck ! »