Logo image
Back
On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees
Conference proceeding   Open access

On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees

Joyanta Debnath, Sze Yiu Chau and Omar Chowdhury
CCS '21: Proceedings of the ACM Conference on Computer and Communications Security, pp.1388-1404
CCS '21: The 2021 ACM SIGSAC Conference on Computer and Communications Security (Virtual Event, Republic of Korea, 11/15/2021–11/19/2021)
11/13/2021
DOI: 10.1145/3460120.3484793
Appears in  UI Libraries Support Open Access
url
https://doi.org/10.1145/3460120.3484793View
Published (Version of record) Open Access

Abstract

The X.509 Public-Key Infrastructure (PKI) standard is widely used as a scalable and flexible authentication mechanism. Flaws in X.509 implementations can make relying applications susceptible to impersonation attacks or interoperability issues. In practice, many libraries implementing X.509 have been shown to suffer from flaws that are due to noncompliance with the standard. Developing a compliant implementation is especially hindered by the design complexity, ambiguities, or under-specifications in the standard written in natural languages. In this paper, we set out to alleviate this unsatisfactory state of affairs by re-engineering and formalizing a widely used fragment of the X.509 standard specification, and then using it to develop a high-assurance implementation. Our X.509 specification re-engineering effort is guided by the principle of decoupling the syntactic requirements from the semantic requirements. For formalizing the syntactic requirements of X.509 standard, we observe that a restricted fragment of attribute grammar is sufficient. In contrast, for precisely capturing the semantic requirements imposed on the most-widely used X.509 features, we use quantifier-free first-order logic (QFFOL). Interestingly, using QFFOL results in an executable specification that can be efficiently enforced by an SMT solver. We use these and other insights to develop a high-assurance X.509 implementation named CERES. A comparison of CERES with 3 mainstream libraries (i.e., mbedTLS, OpenSSL, and GnuTLS) based on 2 million real certificate chains and 2 million synthetic certificate chains shows that CERES rightfully rejects malformed and invalid certificates.
 network security differential testing PKI SSL/TLS protocol SMT solver X.509 certificate authentication UIOWA OA Agreement

Details

Metrics

22 Record Views
4 Times Cited - Web of Science
Logo image