X.509 公钥基础设施（PKI）是广泛使用的可扩展且灵活的身份认证机制，但其标准文本由自然语言编写，存在设计复杂、歧义和欠规定（under-specification）等问题，导致实现者难以完全遵循标准。实际中，很多 X.509 实现库因不符合标准而出现缺陷，进而可能使依赖应用遭受冒充攻击或互操作性问题。本文旨在通过重新工程化（re-engineering）并形式化 X.509 标准中一个广泛使用的片段，并基于此开发一个高可信实现来缓解上述问题。作者的核心思路是将语法要求与语义要求解耦。对于语法要求，他们发现属性文法（attribute grammar）的一个受限片段足以形式化 X.509 的语法结构。对于语义要求，作者使用无量词一阶逻辑（Quantifier-Free First-Order Logic, QFFOL）来精确描述最常用 X.509 功能上的语义约束。有趣的是，使用 QFFOL 所得到的规范是可执行的（executable specification），并且可以由 SMT 求解器高效地执行检查。作者利用这些洞见开发了一个名为 CERES 的高可信 X.509 实现。他们使用 200 万条真实证书链和 200 万条合成证书链，将 CERES 与 mbedTLS、OpenSSL 和 GnuTLS 三个主流库进行了对比实验。结果表明，CERES 能够正确拒绝格式错误和无效的证书，而主流库中存在的相关的非合规缺陷则被暴露出来。该工作为使用形式化方法重新工程化自然语言标准提供了可行范例，也为提升 X.509 生态的整体安全性提供了一条建设性路径。本文适合 PKI/证书安全研究人员、标准制定者以及负责实现或审计 TLS/X.509 库的软件工程师阅读。