A predicated grammar for X509 certificates and its parser : systematically checking for syntactic soundness of digital certificates

TLS is a widely used protocol to guarantee secure communication over an untrusted network. TLS ensures 3 different properties: confidentiality, authentication and integrity. Authentication is commonly provided using Public Key Infrastructure, which is based on digital certificates. Nevertheless, certificate parsing is still an open problem, as suggested by bugs which continuously emerge in current implementations. In this work, we analyze this problem from a language theoretical point of view, and we try a new approach to achieve properly parsing goal, which is a milestone in order to guarantee PKI security. Proposed approach tries to avoid current parsing issues by designing a grammar which can be used to automatically generate a parser. The main problem with this approach is that the language to express certificate structure is context-sensitive, while algorithms to generate parsers generally required context-free grammars. We tackle this issue by analyzing if it is possible to obtain a new context-free language, which obviously includes all current certificates, and a corresponding context-free grammar to generate a parser. While we succeed in language definition, context-free grammar turns out to require too many rules to recognize this new language. Therefore, we employ predicated grammars, which allows to automatically generate a parser even for context-sensitive languages, but with the drawback of introducing semantic predicates, and thus potentially Turing complete statements, in the parser. Nevertheless, our analysis suggests that generated parser is equivalent to a linear bounded automaton, and recognize a context-sensitive language which is a subset of the one defined in X509 standard. We also perform a comparison between our parser and main TLS libraries in order to spot advantages and pitfalls of our approach against current implementations. Results show our parser outperforms these ones, recognizing actually invalid certificates which other libraries consider valid, while basically no issues in our parser recognizing capabilities have been found. These results prove the goodness of our approach and suggest its usage in current implementations.