2017 · 72 citations · 18 references
ComputingComputer ScienceComputer SystemsComputer SecurityNetwork SecuritySecurity ProtocolsCertificate ManagementCertificationCertification TestingProtocol AnalysisProtocol VerificationSecurity Protocol VerificationAutomatic Protocol VerificationBlack-box TestingCertificate ValidationSsl Handshake ProtocolTls Certificate ValidationTls Handshake ProtocolX.509 Certificate ValidationX.509 Certificates
SSL/TLS is the most commonly deployed family of protocols for securing network communications. The security guarantees of SSL/TLS are critically dependent on the correct validation of the X.509 server certificates presented during the handshake stage of the SSL/TLS protocol. Hostname verification is a critical component of the certificate validation process that verifies the remote server's identity by checking if the hostname of the server matches any of the names present in the X.509 certificate. Hostname verification is a highly complex process due to the presence of numerous features and corner cases such as wildcards, IP addresses, international domain names, and so forth. Therefore, testing hostname verification implementations present a challenging task. In this paper, we present HVLearn, a novel black-box testing framework for analyzing SSL/TLS hostname verification implementations, which is based on automata learning algorithms. HVLearn utilizes a number of certificate templates, i.e., certificates with a common name (CN) set to a specific pattern, in order to test different rules from the corresponding specification. For each certificate template, HVLearn uses automata learning algorithms to infer a Deterministic Finite Automaton (DFA) that describes the set of all hostnames that match the CN of a given certificate. Once a model is inferred for a certificate template, HVLearn checks the model for bugs by finding discrepancies with the inferred models from other implementations or by checking against regular-expression-based rules derived from the specification. The key insight behind our approach is that the acceptable hostnames for a given certificate template form a regular language. Therefore, we can leverage automata learning techniques to efficiently infer DFA models that accept the corresponding regular language. We use HVLearn to analyze the hostname verification implementations in a number of popular SSL/TLS libraries and applications written in a diverse set of languages like C, Python, and Java. We demonstrate that HVLearn can achieve on average 11.21% higher code coverage than existing black/gray-box fuzzing techniques. By comparing the DFA models inferred by HVLearn, we found 8 unique violations of the RFC specifications in the tested hostname verification implementations. Several of these violations are critical and can render the affected implementations vulnerable to active man-in-the-middle attacks.
18
Introduction to the Theory of Computation
Michael Sipser · ACM SIGACT News · 1996 · 2.8K citations
Learning regular sets from queries and counterexamples
Dana Angluin · Information and Computation · 1987 · 2.1K citations
Test selection based on finite state models
Susumu Fujiwara, Gregor von Bochmann, Ferhat Khendek et al. · IEEE Transactions on Software Engineering · 1991 · 564 citations
Why eve and mallory love android
Sascha Fahl, Marian Harbach, Thomas Muders et al. · 2012 · 491 citations
Lower bounds for natural proof systems
Dexter Kozen · 1977 · 446 citations