Test Suite development for verification of TLS security protocol

Abstract

Despite the fact that TLS and its predecessor SSL are in use for more than 15 years, there are no accepted public conformance test suite for those protocols. Implementers do have their own test suites, but the primary objective of those tests are internals of the corresponding implementation rather than conformance against the standard. Furthermore, such tests are too much implementation specific to be used to be used for implementation other than they were developed for. In general it is impossible to test a TLS/SSL implementation with tests from another implementation. The paper presents an approach to conformance testing of TLS/SSL server implementations. The approach is based on Model- Based Testing methodology. A test suite was developed and propped against a number of open TLS/SSL server implementations. The developed approach to conformance testing is based on automated testing against formal specifications. Requirements in the text specification are statements in a natural language, describing desired behavior of TLS implementations. Following the approach used we elicited more than 300 functional requirements to server implementations and formalized in the specification extension of Java language. The language used is part of UniTESK family of MBT technologies. Using the extension, the protocol model is presented as a contract specification with pre- and postcondition defining constraints on the allowed behavior. The specification is backed with a technique for on-the-fly test construction provided by UniTESK tools. We tried the test suite against three open implementations of TLS. Testing revealed discrepancies with the standard in all three implementations, and one implementation suffers from violation of a critical requirement. The work proved that the proposed approach to verification, based on protocol modeling with contract specifications, provides efficient automation of protocols as complex as security protocols. Furthermore, thanks to formal models, the tests have well-defined and trackable coverage criteria that greatly enhances quality of testing.