On the Adequacy of Statecharts as a Source of Tests for Cryptographic Protocols

The effectiveness of statecharts as a tool to express the desired behavior of security protocols and a source of tests for their implementations was investigated. Specifically, TLS protocol was modeled as a statechart and tests generated from its flattened version. The GnuTLS implementation of the protocol was then tested against the generated tests. The MC/DC coverage of different components of the implementation varied from 51% to 81%. A "what if" analysis revealed that while some defects in the uncovered code will not lead to any security vulnerability due to in-built fault tolerance, others might lead to improper authentication, integrity failure, session hijacking, denial of service, and loss of confidentiality. The analysis suggests that statecharts alone might not be an adequate tool as a source of tests for implementations of security protocols and that tests so generated must be augmented through other formal means such as random testing, stress testing, and code coverage analysis.