Project Description

Transport layer security (TLS) and secure socket layer (SSL) protocols aim to establish a secure channel with confidentiality and integrity guarantees over an insecure network. SSL/TLS is currently being used to protect a large number of servers and websites including banks, file servers, and social networks. To avoid impersonation attacks in SSL/TLS, users initiating an SSL/TLS communication are recommended to authenticate their communication peer to ensure they are interacting with the intended party and not an impostor.

The X.509 public-key infrastructure (PKI) compensates for the Internet's inherent lack of trust by providing a cryptography-backed authentication framework in which entities are organized hierarchically based on trust, and each entity can obtain a certificate confirming its identity.

While there is open-source software that implements the X.509 prescribed authentication checks, bugs in this software can leave users vulnerable to impersonation attacks or loss of service. The X.509 open-source standard implementations, unlike SSL/TLS, have escaped rigorous security evaluations despite the fact that the security of SSL/TLS critically hinges on a correct X.509 implementation. This project seeks to reduce the attack surface of SSL/TLS and other applications that use X.509 as the authentication provider by developing an automatic technique for detecting logical bugs in X.509 implementations.

This project will take advantage of the insight that a given X.509 implementation partitions the certificate input universe into accepting (certificates considered valid by the implementation) and rejecting (certificates considered invalid) universes. One can use symbolic execution to automatically extract an approximation of the two universes from a given X.509 implementation and represent them with logical formulas.

The project then aims to precisely capture the X.509 standard specification in some formal logic and also develop a reference implementation of the X.509 standard. To prove the compliance of the reference implementation against the formal specification, the research will leverage a combination of model checking and deductive verification techniques.

With the provably correct reference implementation, say R, at hand, it will be possible to detect logical bugs and inconsistencies in a given X.509 implementation, T, by checking whether T deviates from R. Deviations will be efficiently calculated by comparing the certificate universes of R and T. In addition to its research impact, the techniques and research findings of this project will have a positive impact on the training of the future generation of computer security professionals.

This series of work is funded by NSF CRII SaTC Award #1657124.

---

Publications

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

• Authors:
  • Sze Yiu Chau (Purdue University)
  • Omar Chowdhury (The University of Iowa)
  • Endadul Hoque (Florida International University)
  • Huangyi Ge (Purdue University)
  • Aniket Kate (Purdue University)
  • Cristina Nita-Rotaru (Northeastern University)
  • Ninghui Li (Purdue University)
• Published in: IEEE Symposium on Security and Privacy (Oakland) 2017
• Recognition: CSAW '17 (Applied Research) Finalist
• Impact:
  • Found 48 instances of noncompliance in various small-footprint SSL/TLS libraries
  • Revisit results of previous research papers and found inaccurate claims
  • New CVEs:
    • MatrixSSL date-time checking; CVE-2017-1000415 (CVSS Severity: Medium)
    • axTLS date-time checking; CVE-2017-1000416 (CVSS Severity: Medium)
    • MatrixSSL OID comparison; CVE-2017-1000417 (CVSS Severity: Medium)
      * Findings independently found and fixed by library developers are not reported for CVEs.
• High level Idea:
  
  In this paper we focus on small footprint SSL/TLS libraries. Thanks to the recent bloom of Internet of Things (IoT) devices and their constrained resources and computational power, new small footprint SSL/TLS libraries are gaining momentum in the market. They are typically written in the C programming language and heavily optimized in memory usage and performance. We leverage the availability of multiple open source libraries from different vendors for differential testing.
  
  The above figure illustrates our noncompliance finding approach for X.509 CCVL implementations. Symbolic execution engine takes as input a CCVL implementation and extracts the approximated accepted and rejecting certificate universe whereas extraction validator validates it through concrete execution. Missing field check detector finds unscrutinized certificate fields from the universes. Cross validation engine performs cross validation among two implementations universes.
• Artifacts: Paper|Errata|Talk|Samples of extracted path constraints|GUI for making concrete inputs symbolic

---

Contact

Dr. Omar Chowdhury
Assistant Professor
Department of Computer Science
The University of Iowa

• Email: omar-chowdhury@uiowa.edu

• Telephone: (319) 335-0745

---