Proceedings of ISP RAS


TLS Clients Testing

A.V. Nikeshin (ISP RAS, Moscow), N.V. Pakulin (ISP RAS, Moscow), V.Z. Shnitman (ISP RAS, Moscow)

Abstract

The paper presents a model-based approach to conformance testing of TLS implementations. It discusses the formal model of TLS protocol, the structure of the test suite. JavaTesK tool, based on  UniTESK  technology, was used to develop the test suite. A set of fuzz operators was developed  for general data types and included in the test suite. We applied the test suite to a several popular implementations of TLS client, and present brief results. This approach has proved his efficiency, various errors and vulnerabilities had been found in all chosen TLS implementations.

Keywords

testing, verification, formal methods, formal specifications, Model Based Testing, TLS, SSL, UniTESK, Fuzz Testing

Edition

Proceedings of the Institute for System Programming, vol. 27, issue 2, 2015, pp. 145-160.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2015-27(2)-9

Full text of the paper in pdf (in Russian) Back to the contents of the volume