Programs are omnipresent in our lives; on the chips of transport cards, in cars or pacemak- ers for example. Many programs are also run on multiple hosts in order to be able to serve more users. However, these hosts may not always be safe and thus these programs need to be protected. Program obfuscation is a promising approach to protect secret information of softwares in untrusted environments. It consists in modifying programs in such a way that they are harder to understand but retain the same behaviour. It has been widely studied, however no theoretical basis to evaluate obfuscations has appeared. The purpose of the internship is to explore a new way to evaluate obfuscations based on the proof assistant Coq consisting in comparing the proofs of semantic preservation of said obfuscations. Indeed, such a proof can be seen as an explanation of why the programs behave the same way and is hence directly related to the potency of the obfuscation.
We present here a static control flow analysis used in the Simple Unified Policy Programming Language (SUPPL) compiler to detect internally inconsistent policies. These inconsistencies are called conflicts. The analysis is twofold, it first detects potential conflicts and then eliminates the unrealizable conflicts through the use of SMT solvers. Supposing that inputs to the solvers are correctly generated, the analysis is formally proven sound with the help of the proof assistant Coq.
Nous présentons ici une étude de la ''correction'' d'obfuscations de programmes. Nous commencons par spéci fier la sémantique d'un langage impératif minimaliste dans l'assistant de preuve Coq, puis nous prouvons que les obfuscations que nous étudions préservent la sémantique voulue du programme originel. Nous montrons ici la démarche suivie afi n d'accomplir cela, nous pouvons notamment observer qu'il ya une certaine correspondance entre la ''sécurité'' d'une obfuscation et la complexité de la preuve de la préservation de la sémantique.
Creation of a tool to help users to specify and verify cryptographic protocols in ProVerif.
Les protocoles dits cryptographiques – c’est-à-dire reposant sur l’utilisation de primitives cryptographiques – sont très largement utilisés dans la vie courante, et en particulier dans de nombreux domaines critiques. L’utilisation d’outils de vérification automatique permet de prouver certaines propriétés de sécurité sur de tels protocoles. Cependant, exprimer ces propriétés de manière formelle n’est pas toujours aisé et les dits outils ne sont pour la plupart pas faciles d’utilisation. Ce rapport s’intéresse au développement d’un ensemble de modules visant à améliorer l’ergonomie du logiciel de vérification automatique ProVerif, ainsi qu’à développer l’interaction entre l’utilisateur et le logiciel.
Creation of a simple analyzer in OCaml for a toy language called While. It can compute the Control Flow Graph and a liveness analysis of a program.