SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations

Sze Yiu Chau, Omar Chowdhury, Endadul Hoque, Huangyi Ge, Aniket Kate, Cristina Nita-Rotaru, Ninghui Li

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

Abstract

The X.509 Public-Key Infrastructure has long been used in the SSL/TLS protocol to achieve authentication. A recent trend of Internet-of-Things (IoT) systems employing small footprint SSL/TLS libraries for secure communication has further propelled its prominence. The security guarantees provided by X.509 hinge on the assumption that the underlying implementation rigorously scrutinizes X.509 certificate chains, and accepts only the valid ones. Noncompliant implementations of X.509 can potentially lead to attacks and/or interoperability issues. In the literature, black-box fuzzing has been used to find flaws in X.509 validation implementations, fuzzing, however, cannot guarantee coverage and thus severe flaws may remain undetected. To thoroughly analyze X.509 implementations in small footprint SSL/TLS libraries, this paper takes the complementary approach of using symbolic execution. We observe that symbolic execution, a technique proven to be effective in finding software implementation flaws, can also be leveraged to expose noncompliance in X.509 implementations. Directly applying an off-the-shelf symbolic execution engine on SSL/TLS libraries is, however, not practical due to the problem of path explosion. To this end, we propose the use of SymCerts, which are X.509 certificate chains carefully constructed with a mixture of symbolic and concrete values. Utilizing SymCerts and some domain-specific optimizations, we symbolically execute the certificate chain validation code of each library and extract path constraints describing its accepting and rejecting certificate universes. These path constraints help us identify missing checks in different libraries. For exposing subtle but intricate noncompliance with X.509 standard, we cross-validate the constraints extracted from different libraries to find further implementation flaws. Our analysis of 9 small footprint X.509 implementations has uncovered 48 instances of noncompliance. Findings and suggestions provided by us have already been incorporated by developers into newer versions of their libraries.

Original languageEnglish (US)
Title of host publication2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages503-520
Number of pages18
ISBN (Electronic)9781509055326
DOIs
StatePublished - Jun 23 2017
Externally publishedYes
Event2017 IEEE Symposium on Security and Privacy, SP 2017 - San Jose, United States
Duration: May 22 2017May 24 2017

Publication series

NameProceedings - IEEE Symposium on Security and Privacy
ISSN (Print)1081-6011

Conference

Conference2017 IEEE Symposium on Security and Privacy, SP 2017
CountryUnited States
CitySan Jose
Period5/22/175/24/17

    Fingerprint

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Software
  • Computer Networks and Communications

Cite this

Chau, S. Y., Chowdhury, O., Hoque, E., Ge, H., Kate, A., Nita-Rotaru, C., & Li, N. (2017). SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations. In 2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings (pp. 503-520). [7958595] (Proceedings - IEEE Symposium on Security and Privacy). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/SP.2017.40