On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees
On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees
复制标题
DOI：
10.1145/3460120.3484793
复制
发表时间：
2021-11
期刊：
影响因子：
--
通讯作者：
Joyanta Debnath;Sze Yiu Chau;Omar Chowdhury
中科院分区：
文献类型：
--
作者：
Joyanta Debnath;Sze Yiu Chau;Omar Chowdhury
X.509公钥基础设施（PKI）标准被广泛用作可扩展和灵活的认证机制。X.509实现中的缺陷会使依赖应用程序容易受到模拟攻击或互操作性问题的影响。在实践中，许多实现X.509的库已经被证明存在由于不符合标准而导致的缺陷。开发一个兼容的实现尤其会受到设计复杂性、模糊性或用自然语言编写的标准中规范不足的阻碍。在本文中，我们着手减轻这种不令人满意的状态，通过重新设计和形式化的X.509标准规范的广泛使用的片段，然后用它来开发一个高保证的实现。我们的X.509规范再工程工作的指导原则是从语义需求的语法需求解耦。对于形式化的语法要求的X.509标准，我们观察到，一个有限的片段的属性语法是足够的。相比之下，为了精确地捕捉最广泛使用的X.509功能的语义要求，我们使用无量词一阶逻辑（QFFOL）。有趣的是，使用QFFOL会产生一个可执行的规范，SMT求解器可以有效地执行该规范。我们使用这些和其他见解来开发一个名为CERES的高保证X.509实现。CERES与3个主流库（即，mbedTLS、OpenSSL和GnuTLS）基于200万个真实的证书链和200万个合成证书链的测试表明，CERES正确地拒绝了格式错误和无效的证书。
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.