THÈSE

THÈSE

Documents
249 pages
Lire
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

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 ...

Sujets

Informations

Publié par
Nombre de visites sur la page 139
Langue English
Signaler un problème
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 Considered Harmful . . . . . . . . . . . . . . . . . . . . 147 6.1.4 as a Programming Discipline . . . . . . . . . . . . . . . . 148 6.1.5 Problems with Alias Analyses . . . . . . . . . . . . . . . . . . . . 150 6.1.6 with Alias Control Techniques . . . . . . . . . . . . . . 151 6.1.7 Problem Statement . . . . . . . . . . . . . . . . . . . . . . . . . . 151 6.2 Inferring Regions: Existing Type-Based Approaches . . . . . . . . . . . . 152 6.2.1 Steensgaard’s Region Inference . . . . . . . . . . . . . . . . . . . 152 6.2.2 Talpin’s Region Inference . . . . . . . . . . . . . . . . . . . . . . 154 6.3 Refining Regions: a New Type-and-Effect Approach . . . . . . . . . . . . 156 6.3.1 Equivalence of Paths and Regions . . . . . . . . . . . . . . . . . . 156 6.3.2 Modular Region Inference . . . . . . . . . . . . . . . . . . . . . . 156 6.3.3 Complete Region for Interference-Free Programs . . . . . 160 6.3.4 Refined Region Inference . . . . . . . . . . . . . . . . . . . . . . 162 6.3.5 Incompleteness of Refined Region Inference . . . . . . . . . . . . 164 6.4 Other Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164 6.5 Chapter Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165 7 Programs with Unions and Casts 167 7.1 Prefix Casts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 7.1.1 Extending JESSIE with Subtyping . . . . . . . . . . . . . . . . . . 168 7.1.2 Crawling the Type Hierarchy . . . . . . . . . . . . . . . . . . . . . 169 7 7.2 Moderated Unions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171 7.2.1 Discriminated Unions in JESSIE . . . . . . . . . . . . . . . . . . . 171 7.2.2 Byte-Level Unions in JESSIE . . . . . . . . . . . . . . . . . . . . . 175 7.2.3 Choice of Union in JESSIE . . . . . . . . . . . . . . . . . . . . . . 177 7.3 Other Unions and Casts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 7.4 Other Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180 7.5 Chapter Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181 III Experiments 183 8 on Real C Programs 185 8.1 Notes of Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . 186 8.1.1 Logical Model of Strings . . . . . . . . . . . . . . . . . . . . . . . 186 8.1.2 Preprocessing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 8.1.3 Filtering Results . . . . . . . . . . . . . . . . . . . . . . . . . . . 189 8.2 String Libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189 8.2.1 MINIX 3 Standard String Library . . . . . . . . . . . . . . . . . . 189 8.2.2 CERT Managed String Library . . . . . . . . . . . . . . . . . . . . 195 8.2.3 Related Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 8.3 Benchmarks of Vulnerabilities . . . . . . . . . . . . . . . . . . . . . . . . 202 8.3.1 Verisec Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203 8.3.2 Zitser’s Benchmark . . . . . . . . . . . . . . . . . . . . . . . . . . 206 8.3.3 Related Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206 8.4 Chapter Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207 Conclusion 211 A Résumé en Français 217 A.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218 A.2 Opérations entières et accès mémoire . . . . . . . . . . . . . . . . . . . . . 220 A.2.1 Définition d’un langage intermédiaire . . . . . . . . . . . . . . . . 220 A.2.2 Preuve de la sûreté des opérations entières . . . . . . . . . . . . . . 221 A.2.3 Preuve de la sûreté des accès mémoire . . . . . . . . . . . . . . . . 221 A.3 Inférence, séparation, unions et casts . . . . . . . . . . . . . . . . . . . . . 222 A.3.1 Programmes typés sans partage mémoire . . . . . . . . . . . . . . 222 A.3.2 typés avec . . . . . . . . . . . . . . 223 A.3.3 avec unions et casts . . . . . . . . . . . . . . . . . . . 225 A.4 Expériences sur des programmes C réels . . . . . . . . . . . . . . . . . . . 226 A.4.1 Bibliothèques de chaînes de caractères . . . . . . . . . . . . . . . . 226 A.4.2 Jeux de tests de vulnérabilités . . . . . . . . . . . . . . . . . . . . 228 A.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230 Index 232 8 Bibliography 235 9 10