In the challenge of getting provably correct implementations of security protocols, much effort has been recently put into two strategies: model-driven-development to generate new implementations; and verification of the source code of already existing implementations.
However, no approach currently deals with legacy implementations for which no source code is available. This paper presents a formal approach to design and implement monitors that
stop insecure protocol runs executed by legacy implementations, without the need of their source code. We demonstrate the approach at a case study about monitoring a generic SSL server implementation. Our monitoring approach allowed us to detect a flaw in an SSL client
implementation.
|