[Cryptography] Testing crypto protocol implementations

Sampo Syreeni decoy at iki.fi
Sun Mar 2 21:20:40 EST 2014

On 2014-03-02, Viktor Dukhovni wrote:

> My view is that a tool that tests the security of a protocol 
> implementation, likely needs to be a separate highly scriptable 
> implementation of that protocol which can be programmed to deviate 
> from the protocol at every step, (modify and/or re-order the expected 
> protocol messages in controlled ways).

Why not formalize the problem? True, formal protocol verification 
suffers from state space explosion, in general. But if you design your 
protocol to be easily verifiable, and match your verifier to what you're 
about to verify, you can skirt the problem to a high degree. In the 
absence of that, and/or in addition to it, if you have access to a 
similarly well-structured code base implementing the protocol, it 
should't be too hard to formalize well-covered white-box testing, 
intelligent fuzzing and whatnot, by automating at least every heuristic 
known to the testing community at large.

All of that should be doable at a generic level, if you're just willing 
to circumscribe the problem narrowly enough. No instrumentation in code, 
no problem specific code for test cases or anything like that, but just 
generic tools, able to handle say transactional grammars and a tightly 
regulated program flow encoded in plain C.

> This would be a costly project for each implementation to develop.

So, it's of course costly. But I don't think it'd need be for each 
implementation separately. I think it could be a single research project 
in verification of security minded protocol verification. The seeds of 
which already exist, in multiple places, if I'm not completely mistaken.
Sampo Syreeni, aka decoy - decoy at iki.fi, http://decoy.iki.fi/front
+358-40-3255353, 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2

More information about the cryptography mailing list