Hammurabi: A Framework for Pluggable, Logic-Based X.509 Certificate Validation Policies

This paper proposes using a logic programming language to disentangle X.509 certificate validation policy from mechanism. Expressing validation policies in a logic programming language provides multiple benefits. First, policy and mechanism can be more independently written, augmented, and analyzed compared to the current practice of interweaving them within a C or C++ implementation. Once written, these policies can be easily shared and modified for use in different TLS clients. Further, logic programming allows us to determine when clients differ in their policies and use the power of imputation to automatically generate interesting certificates, e.g., a certificate that will be accepted by one browser but not by another. We present a new framework called Hammurabi for expressing validation policies, and we demonstrate that we can express the complex policies of the Google Chrome and Mozilla Firefox web browsers in this framework. We confirm the fidelity of the Hammurabi policies by comparing the validation decisions they make with those made by the browsers themselves on over ten million certificate chains derived from Certificate Transparency logs, as well as 100K synthetic chains. We also use imputation to discover nine validation differences between the two browsers' policies. Finally, we demonstrate the feasibility of integrating Hammurabi into Firefox and the Go language in less than 100 lines of code each. CCS CONCEPTS • Security and privacy → Web protocol security; Logic and verification.