An RPKI Certificate Validator for Formal Correctness

The Border Gateway Protocol faces persistent risks from route hijacking, mitigated by Resource Public Key Infrastructure (RPKI) through cryptographically validated Route Origin Authorizations. However, existing RPKI validators need a formally verified reference for correctness, especially resource certificate validations. This paper design and present a formally verified RPKI validator to validate resource certificates. Built upon ARMOR, a formally verified X.509 validator for Transport Layer Security, our validator support parsing resource extensions and formalizing 17 semantic rules for RPKI certificate validations in RFC 6487. The validator can not only serve as a reference for testing existing RPKI validator implementations, but also be embedded into them to enhance their formal verification attributes.