THÈSE

Sujets

• Michael Essien
• Carte MS
• Dépassement de tampon
• Abstraction (philosophie)
• Crénelage
• Exploits pour une pierre blanche

Informations

• Publié par: Eftau
• Nombre de lectures: 139
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

ORSAY oN d’ordre: 9366 UNIVERSITÉ DE PARIS-SUD 11 CENTRE D’ORSAY THÈSE présentée pour obtenir le grade de docteur en sciences DE L’UNIVERSITÉ PARIS XI PAR Yannick MOY ! SUJET : Preuve automatique et modulaire de la sûreté de fonctionnement des programmes C Automatic Modular Static Safety Checking for C Programs soutenue le 15 janvier 2009 devant la commission d’examen MM. Burkhart Wolff K. Rustan M. Leino Xavier Leroy Michael Norrish Claude Marché Pierre CrégutJ’ai commencé cette thèse, après quatre années à la R&D de PolySpace, parce que je voulais comprendre comment mieux répondre au problème d’analyse et de vérification des programmes informatiques. Ces trois années m’ont largement satisfaites sur ce point, et m’ont permis de connaître des personnes admirables autant du point de vue professionnel que personnel. Je voudrais remercier pour leur fantastique état d’esprit toutes les personnes de l’équipe ProVal, avec une mention spéciale à Évelyne et Jean-Christophe pour leurs gâteaux déli- cieux, et Jean-Christophe et Sylvain pour l’ambiance sonore chaleureuse. Je remercie respectueusement mes deux directeurs de thèse, Claude et Pierre, pour m’avoir accompagné ces trois années sur le dur chemin de la recherche, et je leur dis mon admiration pour leur talent et leur travail. Je veux remercier sincèrement toutes les personnes de mon jury en plus de mes di- recteurs, Burkhart, Rustan, Xavier et Michael, qui sont tous des chercheurs que j’admire profondément. Vos suggestions, vos remarques et vos questions m’ont permis de mieux comprendre mon sujet et d’avancer encore un peu plus. Je décerne la palme du meilleur soutien de thèse à Jean-Christophe, pour m’avoir motivé tous les mercredis (enfin presque) à aller jouer au foot, en plus d’être une source inépuisable d’énergie et d’inventivité, toujours prêt à discuter d’une idée ou d’un problème. J’octroie la coupe du meilleur prof à François pour qui j’ai donné des TD à l’Ecole Polytechnique, c’était un plaisir d’apporter ma présence à un travail aussi magnifiquement présenté. Je veux remercier tous ceux avec qui j’ai travaillé, discuté de problèmes ou partagé des bons moments au travail durant ces trois années: Yves-Marie, Guillaume, Fayçal, Laurent et Cuit aux Orange Labs, Benjamin, Virgile, Julien, Pascal et Patrick au CEA, Dillon à Das- sault Aviation, David à Airbus, Charles et Xavier à EADS, Francesco et Nikolaj à Microsoft Research, Matteo à Google, Sriram aux NEC Labs. Je remercie tout spécialement ces amis qui sont passés ou sont encore à Orsay: Nicolas S., Jean-François, Aurélien, Alexandre, Stéphane, Johannes, Louis. Je réserve une mention spéciale à Florence pour sa bonne humeur contagieuse, en attendant sa soutenance ! Merci à tous mes amis, ceux qui ont pu se déplacer pour la soutenance et tous les autres, votre soutien m’a toujours aidé. Merci papa, maman, Pierre, Jojo et Manue, vous êtes mon public admiratif préféré. Enfin, un million de fois merci ma femme chérie, Alexandra, rien de tout cela n’aurait existé sans toi.4Contents 1 Introduction 15 1.1 Language-Based Dependability of C Programs . . . . . . . . . . . . . . . 16 1.1.1 Problem Statement . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.1.2 Technical Account . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.1.3 Historical . . . . . . . . . . . . . . . . . . . . . . . . . . 19 1.1.4 Work in Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 1.2 C Language Safety Issues . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 1.2.1 Lack of Precise Semantics . . . . . . . . . . . . . . . . . . . . . . 22 1.2.2 Lack of Language-Based Safety Mechanisms . . . . . . . . . . . . 23 1.2.3 Remediation Techniques . . . . . . . . . . . . . . . . . . . . . . . 27 1.2.4 Better C Initiatives . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1.3 Techniques and Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1.3.1 Enumeration Techniques . . . . . . . . . . . . . . . . . . . . . . . 31 1.3.2 Abstraction T . . . . . . . . . . . . . . . . . . . . . . . . 32 1.3.3 Deduction Techniques . . . . . . . . . . . . . . . . . . . . . . . . 33 1.3.4 Combination Thereof . . . . . . . . . . . . . . . . . . . . . . . . . 33 1.4 Statement of Purpose . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1.5 Summary of Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1.6 Organization of This Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . 36 I Integer and Memory Safety Checking 39 2 Intermediate Language Definition 41 2.1 JESSIE Rationale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 2.2 JESSIE Syntax and Operational Semantics . . . . . . . . . . . . . . . . . . 44 2.2.1 Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 2.2.2 Typing Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 2.2.3 Execution Model . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 2.2.4 Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . 56 2.3 C to JESSIE Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 2.3.1 Data Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 2.3.2 Control T . . . . . . . . . . . . . . . . . . . . . . . . . . 70 52.3.3 A Simple Example: Linear Search . . . . . . . . . . . . . . . . . . 70 2.4 JESSIE Annotation Language . . . . . . . . . . . . . . . . . . . . . . . . . 71 2.5 JESSIE to WHY Translation . . . . . . . . . . . . . . . . . . . . . . . . . . 75 2.6 Other Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 2.7 Chapter Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 3 Integer Safety Checking 79 3.1 Assertions for Integer Safety . . . . . . . . . . . . . . . . . . . . . . . . . 80 3.1.1 Integer Checks . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 3.1.2 Integer Safety for Linear Search . . . . . . . . . . . . . . . . . . . 80 3.1.3 Assertions from Annotations . . . . . . . . . . . . . . . . . . . . . 81 3.2 Abstract Interpretation for Integer Programs . . . . . . . . . . . . . . . . . 82 3.2.1 Theory of Abstract Interpretation . . . . . . . . . . . . . . . . . . 82 3.2.2 Practical Domains . . . . . . . . . . . . . . . . . . . . . . 84 3.2.3 Application to JESSIE Integer Programs . . . . . . . . . . . . . . . 86 3.2.4 Illustration on Linear Search . . . . . . . . . . . . . . . . . . . . . 88 3.3 Deductive Verification for Integer Programs . . . . . . . . . . . . . . . . . 89 3.3.1 Hoare Logics and Dijkstra’s Weakest Preconditions . . . . . . . . . 90 3.3.2 Application to JESSIE Integer Programs . . . . . . . . . . . . . . . 91 3.3.3 Illustration on Linear Search . . . . . . . . . . . . . . . . . . . . . 91 3.4 Other Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 3.5 Chapter Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 4 Memory Safety Checking 95 4.1 Assertions for Memory Safety . . . . . . . . . . . . . . . . . . . . . . . . 96 4.1.1 Memory Model Accessors . . . . . . . . . . . . . . . . . . . . . . 96 4.1.2 Checks . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 4.1.3 Memory Safety for Linear Search . . . . . . . . . . . . . . . . . . 100 4.2 Abstract Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 4.2.1 Abstract Memory Locations . . . . . . . . . . . . . . . . . . . . . 102 4.2.2 Logic Function Applications . . . . . . . . . . . . . . . . 105 4.2.3 Overlaps Between Locations . . . . . . . . . . . . . . . . . . . . . 106 4.2.4 Application to Linear Search . . . . . . . . . . . . . . . . . . . . . 107 4.3 Abstract Interpretation for Pointer Programs . . . . . . . . . . . . . . . . . 108 4.3.1 Lifting Abstract Domains . . . . . . . . . . . . . . . . . . . . . . 108 4.3.2 Application to JESSIE Pointer Programs . . . . . . . . . . . . . . . 109 4.3.3 Illustration on Linear Search . . . . . . . . . . . . . . . . . . . . . 109 4.4 Deductive Verification for Pointer Programs . . . . . . . . . . . . . . . . . 112 4.4.1 Lifting Weakest Preconditions . . . . . . . . . . . . . . . . . . . . 112 4.4.2 Application to JESSIE Pointer Programs . . . . . . . . . . . . . . . 114 4.4.3 Illustration on Linear Search . . . . . . . . . . . . . . . . . . . . . 114 4.5 Chapter Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 6II Inference, Separation, Unions and Casts 117 5 Alias-Free Type-Safe Programs 119 5.1 Problem Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 5.1.1 Type Safety Restriction . . . . . . . . . . . . . . . . . . . . . . . . 120 5.1.2 Aliasing Restriction . . . . . . . . . . . . . . . . . . . . . . . . . 123 5.1.3 Without Logic Annotations . . . . . . . . . . . . . . . . . . . . . . 124 5.1.4 Problem Statement . . . . . . . . . . . . . . . . . . . . . . . . . . 125 5.2 Inferring Logic Annotations . . . . . . . . . . . . . . . . . . . . . . . . . 125 5.2.1 Approach by Abstraction . . . . . . . . . . . . . . . . . . . . . . . 126 5.2.2 by Deduction . . . . . . . . . . . . . . . . . . . . . . . 128 5.2.3 Abstraction and Deduction Together . . . . . . . . . . . . . . . . . 132 5.3 Combining and . . . . . . . . . . . . . . . . . . . . 133 5.3.1 Precondition Inference Algorithm . . . . . . . . . . . . . . . . . . 134 5.3.2 Comparing Techniques . . . . . . . . . . . . . . . . . . 137 5.3.3 Taming Time and Space Complexity . . . . . . . . . . . . . . . . . 139 5.4 Other Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 5.5 Chapter Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 6 Type-Safe Programs with Aliasing 143 6.1 Problem Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144 6.1.1 Memory Aliasing and Separation . . . . . . . . . . . . . . . . . . 144 6.1.2 Frame Condition Equivalent Postcondition . . . . . . . . . . . . . 145 6.1.3 Aliasing Considere