Dynamic Symbolic Execution Based SSL/TLS Checking

Secure Sockets Layer or Transport Layer Security(SSL/TLS)protocol is a security-related and important part of Hypertext Transfer Protocol Secure(HTTPS)which is widely used on the Internet.Certificate validation in SSL/TLS authenticates identities in the phase of handshake.It determines the security of key agreement and subsequent communications that whether certificate validation is implemented correctly.Hence,it is of significance to the security of Internet that checking certificate validation in SSL/TLS implementations.A novel approach for checking certificate validation in SSL/TLS,named RFCcert,is put forward based on the Request for Comments(RFC)set by Internet Engineering Task Force(IETF).Firstly,rules of certificates are extracted automatically from RFC 5280 according to the 11 capitalized key words which are specified by RFC 2119 to express different requirements or prohibitions of specifications.The extracted rules are updated automatically according to RFC 6818.The updated rules are classified into producer,consumer and shared rules according to which roles should conform to the rules.Consumer and shared rules are further classified into breakable and unbreakable rules according to whether the constraints can be broken.Breakable and unbreakable rules are expressed as rule variables.Secondly,rule variables are used to generate symbolic programs automatically.The symbolic programs are employed to generate low-level test cases by using dynamic symbolic execution(DSE)technique.Thirdly,high-level test cases,i.e.X.509 digital certificates,are assembled according to the information provided by low-level test cases.Finally,the assembled X.509 digital certificates are employed to test certificate validation in SSL/TLS implementations through the token-ring approach to look for latent vulnerabilities and bugs.RFCcert has the following advantages: it does not depend on source codes of certificate validation;it determines the validity of a discrepancy and the correctness of certificate validation automatically;it provides reasons for invalid and valid discrepancies based on the rules of certificates in RFC 5280;it automatically computes the number of bugs and the conformance ratio of certificate validation with respect to RFC 5280;it is able to test certificate validation in a single SSL/TLS implementation;and the automated token-ring testing approach is useful in improving the testing efficiency.In order to study the ability of RFCcert to check certificate validation in SSL/TLS implementations,the prototype tool named RFCcertDT has been implemented.RFCcertDT consists of two modules which are in charge of generating test cases and executing differential testing of certificate validation,respectively.The modules mentioned above comprise 10 submodules such as the rule extraction submodule.RFCcertDT is compared with Mucert,NEZHA and SymCerts which are tools employed to test certificate validation.In the comparison of RFCcertDT with Mucert,experimental results show that the ratio of finding discrepancies and the average speed of finding a discrepancy of RFCcertDT are better than those of Mucert.In the comparison of RFCcertDT with NEZHA,experimental results show that the integrated ratio of finding discrepancies and the integrated average speed of finding a discrepancy of RFCcertDT are better than the ratio of finding discrepancies and the average speed of finding a discrepancy of the coarse path ?-diversity guidance engine,the fine path ?-diversity guidance engine,and the output ?-diversity guidance engine of NEZHA.In the comparison of RFCcertDT with SymCerts,experimental results show that RFCcertDT spends less time in finding more instances violating specifications in newer versions of certificate validation than SymCerts does.The comparison above shows that RFCcertDT is more efficient than existing tools.In addition,experimental results show that traditional differential testing approaches are invalid in the case that discrepancies are triggered by optional terms such as“MAY”.Among the bugs discovered and reported by RFCcertDT,9 ones have been confirmed or fixed by related enterprises or organizations: Google has confirmed one reported bug as a security bug and fixed it in Chrome v58.0.3029.81,and this security bug has been included in the Common Vulnerabilities and Exposures(CVE)and its number is CVE-2017-5066;Microsoft has confirmed one reported bug found in Internet Explorer;GnuTLS has confirmed and fixed three bugs;and wolfSSL has confirmed and fixed four bugs.Experiments and practical applications show that RFCcert and its prototype tool RFCcertDT are good at checking certificate validation in SSL/TLS implementations and thus reinforce the security of SSL/TLS implementations.RFCcert is combined with mutation approaches to develop a new approach named mRFCcert.mRFCcert employs X.509 digital certificates assembled by RFCcert as seed certificates which provide basic information on rules to be obeyed or violated.mRFCcert tracks the mutation process to obtain the mutation information.When a mutated certificate triggers a discrepancy,the basic and mutation information is employed to find reasons for the discrepancy.According to mRFCcert,the mutation tracking function is added to the tool for Mucert.The augmented tool adopts mutation operators and 6 mutation strategies of Mucert to mutate digital certificates provided by RFCcert in the experiment.Experimental results show that mRFCcert adds the coverage of discrepancies found by Mucert and enhances the ability of 5 mutation strategies to find new discrepancies.In summary,RFCcert overcomes the limitation and invalidity of traditional differential testing approaches.The X.509 digital certificates generated by RFCcert provide information which is useful in determining and analyzing discrepancies and bugs.The prototype tool RFCcertDT has a good ability to check certificate validation in SSL/TLS implementations and find one new vulnerability and eight new bugs.RFCcert is used in conjunction with mutation approaches such as Mucert to develop a new and efficient approach.RFCcert is helpful to reinforce the security of SSL/TLS implementations which in turn guarantee the security of Internet.