Higher-Order Probabilistic and resource-aware Reasoning – HOPR

The digitalization of our societies comes with increasing risks in security and privacy. Formal methods based on logic initially developed for verification of critical software have been progressively applied to cryptography and privacy. In particular some domain-specific proof-assistant tools like Easycrypt and Squirrel can prove security of cryptographic constructions in the computational model, which provides strong guarantees. Differential privacy is a well-accepted notion of privacy relying on statistical guarantees. Ensuring that a given program is differentially private can however be a difficult task, and some formal methods have also been introduced for that. One difference though between the specialized tools above and the general-purpose Coq proof-assistant is that Coq supports higher-order functions, that is to say functionals which can take functions as arguments. This allows for modular proofs, which have been the key to some successes in verification of compilers and mathematical theorems. Squirrel and Easycrypt currently only feature a limited form of higher-order which is not sufficient for full modularity. They also lack reasoning on the complexity of attackers. This is due to the difficulty of combining in a common logical framework three advanced features: higher-order computation, probabilistic reasoning and representation of complexity-bounded computation. Our first objective is thus to define some logical frameworks that can handle together these features. Our second objective is to use these logical frameworks in the two application domains mentioned above. In cryptography we plan to extend the higher-order features and complexity analysis capabilities of Squirrel and Easycrypt. In differential privacy we plan to define a new Hoare logic combining the benefits of two existing approaches, that is to say allowing both for verification of primitives and for defining typing rules allowing to automate verification of large programs.