Technologies des programmes accompagnés de preuves Hoang Minh Tien 13 septembre, 2009 Sous la direction de Professeur. Danny Dubé Département d’informatique et de génie logiciel Faculté des sciences et de génie Université Laval Copyright © 2009 Hoang Minh Tien LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Mot clés : programme accompagné de preuves, condition de vérification, programme accompagné de preuves étendues, programme accompagné de preuves d’oracle, logique de premier ordre, lambda calcul, consommateur de code, producteur de code. Keywords: proof carrying code, verification condition, extended proof carrying code, oracle based proof carrying code, foundational proof carrying code, type safe, logical framework, first order logic, lambda calculus, code consumer, code producer. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Remerciements Je tiens à remercier vivement Monsieur Danny Dubé, professeur de l’Université Laval, de m’avoir accueilli au sein de son équipe de recherche, de m’avoir toujours encouragé, de m’avoir donné des suggestions précieuses dans la recherche.
Je lui en suis très reconnaissant. Je tiens à remercier également les professeurs et les personnels de l’Institut de la Francophonie pour l’Informatique, des professeurs invités de m’avoir donné des cours de haut qualité et pour leur soutien tout au long de mes études. Je voudrais remercier mes amis dans mon laboratoire de recherche, Bui Nguyen Minh, Haythem Kefi, Joseph Assouramou, Marieme Doua, Ishagh Mayouf de m’avoir donnée leurs conseils, leurs commentaires et leurs soutiens pendant le temps j’effectuais ma recherche. J’adresse un grande merci à ma famille pour leur soutien et leur encouragement de toute l’instance.
LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Table des matières List des figures. Contexte du stage. Principes d’assurer la sécurité pour le consommateur. Structure du rapport.
4 Techniques principales de PCC. Technique PCC traditionnel .1 Architecture du système PCC traditionnel .2 Protocole de PCC traditionnel.3 Implémentation du technique PCC traditionnel .4 Contributions du technique PCC traditionnel .1 Architecture du système OPCC .2 Contribution du technique OPCC .1 Architecture du système FPCC .2 Implémentation de technique FPCC .3 Contribution de technique FPCC .16 -i- LUAN VAN CHAT LUONG download : add luanvanchat@agmail.1 Architecture du technique EPCC .2 Contribution de technique EPCC .18 Vérification de la sécurité du machine virtuelle d’EPCC. Présentation de la machine virtuelle VEP .2 Gestion de mémoire .3 Ensemble des instructions de VEP .4 Assurance la sécurité de VEP. Vérification de la sécurité de la VEP .1 Vérification manuelle de la VEP .2 Vérification automatique de la VEP .34 Conclusion et perspectives.
Outil pour le prouveur de théorème. Utilisation de Frama-C. Spécification de sécurité du tas dans la VEP .42 -ii- LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com List des figures Figure 1. Architecture du système PCC [6].
Représentation des axiomes et règles d’inférence. Spécification de la fonction inc. Une condition de vérification. La machine abstraite DEC Alpha [9].
Calcule de condition de vérification [9]. Architecture de technique OPCC. Architecture de technique FPCC. Instructions sont encodées avec un mot 32-bit [16].
EPCC pour le PCC traditionnel [2]. Architecture de la VEP. Représentation de données dans la VEP. Stockage des paires dans le tas.
Algorithme pour récupérer automatiquement la mémoire. Problème de référence cyclique [3]. Ensemble des instructions de la VEP [19]. Sémantiques des instructions de VEP [3].
Assurance de sécurité sur la VEP [3]. Tests de la sécurité sur la VEP [3]. Architecture de Frama-C [20]. Catégoriser l’ensemble des instructions de la VEP.
Vérifier l’instruction BAND. Structure du tas. Paires libres forment une liste chainée. Algorithme non-récursif de récupérateur de mémoire.33 -iii- LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Résumé La technologie des programmes accompagnés de preuves (Proof Carrying Code, PCC) a été introduite pour la première fois en Novembre 1996 dans le projet de recherche de George Necula et Peter Lee [1] de l’université Carnegie Melon.
Cette méthode est pour but de vérifier la sécurité d’un programme inéprouvé sur le consommateur de code en utilisant des preuves générées par le producteur de codes. Car la vérification entre les codes et les preuves est effectuée une seule fois dès le premier démarrage du programme, sa performance est donc préservée. La méthode est connu aussi par sa simplifié, sa flexibilité dans le déploiement. Pourtant il existe encore des points faibles qui empêche l’application de PCC en réalité, en basant sur les points de vue différents, les chercheurs ont donné leur façon d’améliorer le modèle primitif comme limiter la taille de l’infrastructure présumée fiable (dans le modèle FPCC [5], Andrew W.
Appel), réduire la taille des preuves (dans le modèle OPCC[4], Necula) … Ce mémoire vise à réaliser une recherche sur les techniques principales de programmes accompagnés de preuves, à analyser ses avantages et aussi ses inconvénients. On se concentrera sur la méthode programmes accompagnés de preuves étendu (EPCC [2]) proposé par Danny Dubé et Heidar Pirzadeh Tabari de l’Université Laval. On discutera également l’architecture d’une machine virtuelle (VEP [3]), le cœur du EPCC, et proposer un prototype pour prouver automatiquement la sécurité de cette machine. -iv- LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Abstract Introduced for the first time in November 1996 by George Necula and Peter Lee [1] from university Carnegie Melon, proof carrying code (PCC) is a promising method for verifying the security of an untrusted program executed on a code consumer by using proofs generated by code producer.
The verification is performed only for the first run of the program so the performance of program is not affected. This technique is also attractive for the simplicity and flexibility in the deployment process. However, there are still some disadvantages that make it difficult to apply the model widely in reality. Some of them are solved in the research of Andrew W.
Appel et al (FPCC [5], reducing the trusted computing based), of George Necula (OPCC [4], reducing the size of proof) … This thesis aims to carry out a research on major techniques of proof carrying code, to analyse the advantages and disadvantage of each technique. An important part in this thesis concentrates on the framework EPCC (Extended framework for Proof Carrying Code) proposed by Danny Dubé and Heidar Pirzadeh Tabari from University Laval, the architecture of the virtual machine for EPCC (VEP [3]), the heart of EPCC as well as some propositions for proving automatically its security. -v- LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Chapitre I Introduction 1. Contexte du stage Le stage est réalisé au sein de l’équipe LSFM (Langages, Sémantique et Méthodes formelles) de l’Université Laval.
Le thème du stage est la sécurité informatique, surtout la technique de programme accompagné de preuves et ses variantes. Ce sont des méthodes formelles qui permettent de représenter les politiques de sécurité d’un système et le logiciel sous forme d’une formule logique, la satisfaisant de cette formule assure que le logiciel est sécuritaire. Dans l’extension EPCC proposée par cette équipe (Danny Dubé et Heidar Pirzadeh[2]), une version d’une machine virtuelle a été développé et prouvé manuellement. Pour convaincre l’utilisateur de absolument se fier à la sécurité de cette extension il faut que la machine soit automatiquement prouvée.
Dans le cadre du stage, on propose des changements nécessaires de la machine virtuelle pour que sa sécurité soit automatiquement prouvée. Problématique Le rôle important des logiciels dans tous les domaines de la vie est une réalité indéniable. On peut voir leur utilisation sur des systèmes de haute capacité sur lesquels on peut appliquer plusieurs politiques de sécurité. Dans les années récentes, on les utilise de plus en plus sur divers systèmes de capacité limitée comme le micro contrôleur, la carte à puce … On ne peut pas prendre des mesures de sécurité comme dans le grand système, on ne peut non plus le laisser non-vérifié, spécialement dans le cas on fournit une solution complète dans laquelle il y a des coopérations de tous les ensembles mentionnés.
C’est à cause d’une vérité : si la sécurité d’un système est considérée comme une chaine, elle dépende toujours au nœud le plus faible. Comment pourrait-on alors construire un cadre pour assurer la sécurité des systèmes de capacité limitée ? Il existe une contradiction, les producteurs de logiciel prétendent toujours que leurs logiciels sont sécuritaires tandis que leurs clients doivent régulièrement mettre à jour les correctifs afin de prévenir les failles de sécurité. Les géants dans l’industrie de 1 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Chapitre I - Introduction logiciel ne sont pas exceptions. En effet, le correctif le plus récent de Microsoft (8- Sep-2009) corrige 31 failles de sécurité dans lesquelles 5 failles sont classées dans la catégorie des failles critiques.
Dans l’attente du prochain correctif, comment le client pourrait-il se protéger contre des attaques? Il faudrait par conséquent disposer d'un moyen simple, mais assez forge pour contrer les actions qui violent les politiques de sécurité au niveau du client. Avec l’aide de technique programme accompagné des preuves (Proof Carrying Code, PCC) le consommateur peut vérifier est ce que le logiciel fournit par le producteur est conforme à sa politique de sécurité ou non. D’ailleurs, l’application de PCC ne diminue pas la performance de programme et la consommation de ressources (mémoire, processeur) de PCC sur le consommateur est limitée au maximum. En basant sur les principes d’assurer la sécurité, on analysera les points forts, points faibles de chaque technique PCC et leurs applications en réalité et fournit un prototype pour vérifier la sécurité de la machine virtuelle.
Principes d’assurer la sécurité pour le consommateur Pour le consommateur, en général, on est capable de contrôler la sécurité d’un logiciel avant ou pendant son exécution. Pour assurer la sécurité avant l’exécution, on effectue une analyse statique sur le code en utilisant un outil qui décompose le programme sans l’exécuter et analyse tous les comportements possibles pour prouver que le programme soit sécurité. Les implémentations en réalité de ce type d’assurance sont le « Model checking » [24], analyser flux de donnée [25], interprétation abstraite [14]. Pendant l’exécution, on a l’analyse dynamique, où on fait marcher le programme et utilise un « runtime monitor » pour l’observer, et l’arrêter si dans l’étape suivante, le programme causera une violation.
Toutes les mesures de sécurité sur le client suivent un principe de base: minimiser l’infrastructure présumée fiable (Trusted Computing Based, TCB [15]), le TCB d'un système est l'ensemble des matériaux, des microprogrammes et des logiciels qui se font confiance entre eux et auxquels le client fait confiance, s’il existe des bugs à l'intérieur du TCB, la sécurité du système pourrait être compromise. Par contre, les autres composants en dehors du TCB ne pourront jamais toucher sa sécurité. 2 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Chapitre I - Introduction 4. Contributions Il y a deux contributions principales dans le cadre du stage : Analyser des techniques principales de PCC dans la pointe de vue de l’utilisateur, ses avantages et aussi des inconvénients dans l’application en réalité.
Proposer un changement dans l’algorithme de récupérateur de mémoire de la machine virtuelle d’EPCC et un prototype pour prouver sa sécurité automatiquement. Structure du rapport La suite de ce mémoire se compose de quatre parties Chapitre II – Techniques principales de PCC : présenter l’idée principale de trois techniques de programme accompagné de preuves, leurs forces et faiblesses, spécialement le cadre EPCC. Chapitre III – Vérification de la machine virtuelle d’EPCC : Introduire en détail l’architecture de la VEP, proposer un algorithme pour le récupérateur de mémoire et un prototype pour prouver automatiquement la sécurité de VEP. Chapitre IV – Conclusion et perspectives : Remarques dans l’application de technique PCC en réalité et quelques l’extension de recherche.
Appendice : Informations supplémentaires de l’utilisation d’interface graphique pour le prouveur de théorème, l’utilisation de Frama-C et un exemple des spécifications pour prouver une partie de VEP. 3 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Chapitre II Techniques principales de PCC 1. Technique PCC traditionnel 1.