Automatic verification of confidentiality properties of cryptographic programs

We propose a method to statically analyze cryptographic programs, based on the theory of abstract interpretation, and enabling us to verify a policy of preservation of confidentiality for sensitive data. This method rests on an intruder model notably used in cryptographic protocol analysis by D. Bolignano, but differs from cryptographic protocol analysis in two ways. First, the analyzer is automatic. Then, the analyzer has only one program available, that is, only one of the roles of a cryptographic protocol, itself left unspecified. Finally, the analyzer must work on a real program, not an abstraction of it, as is customary. All this makes verification more difficult than in the case of protocols. Nevertheless, the techniques that we propose, and which rest on a calculus on symbolic constraints, can also prove useful in the setting of cryptographic protocols. We argue that our method is practical by investigating experimental evidence.