Conference proceeding
On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees
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
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.
Details
- Title: Subtitle
- On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees
- Creators
- Joyanta Debnath - University of Iowa, Computer ScienceSze Yiu Chau - Chinese University of Hong KongOmar Chowdhury - University of Iowa, Computer Science
- Resource Type
- Conference proceeding
- Publication Details
- CCS '21: Proceedings of the ACM Conference on Computer and Communications Security, pp.1388-1404
- Conference
- CCS '21: The 2021 ACM SIGSAC Conference on Computer and Communications Security (Virtual Event, Republic of Korea, 11/15/2021 - 11/19/2021)
- Publisher
- Association for Computing Machinery (ACM)
- DOI
- 10.1145/3460120.3484793
- ISSN
- 1543-7221
- Grant note
- name: National Science Foundation, award: CNS-2006556
- Language
- English
- Date published
- 11/13/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984473238402771
Metrics
16 Record Views