Préservation des preuves et transformation de programmes.

Accueil || Parcours || Recherche || S'enregistrer || Mon Compte || Contacts || Aide || Langues

Kunz, César (2009) Préservation des preuves et transformation de programmes. Doctorat Informatique temps réel, robotique et automatique, CMA- Centre de mathématiques appliquées, ENSMP p.165.

Plein texte disponible en tant que : - thesis-ckunz.pdf ( 1389 Kb )

Licence: CC NC ND 3.0

Résumé

Le paradigme du code mobile implique la distribution des applications par les producteurs de code à environnements hétérogènes dans lesquels elles sont exécutées. Une pratique étendue de ce paradigme est constituée par le développement d'applications telles que les applets ou les scripts Web, transferés à travers un réseau non sécurisé comme Internet à des systèmes distants, par exemple un ordinateur, un téléphone mobile ou un PDA (Assistant personnel). Naturellement, cet environnement peux ouvrir la porte au déploiement de programmes malveillants dans des plateformes distantes. Dans certains cas, la mauvaise conduite du code mobile ne constitue pas un risque grave, par exemple lorsque l'intégrité des données affectées par l'exécution n'est pas critique ou lorsque l'architecture d'exécution impose de fortes contraintes sur les capacités d'exécution du code non sécurisé. Il y a toujours, toutefois, des situations dans lesquelles il est indispensable de vérifier la correction fonctionnelle du code avant son exécution, par exemple lorsque la confidentialité de données critiques comme l'information des cartes de crédit pourrait être en danger, ou lorsque l'environnement d'exécution ne possède pas un mécanisme spécial pour surveiller la consommation excessive des ressources. George Necula a proposé une technique pour apporter de la confiance aux consommateurs sur la correction du code sans faire confiance aux producteurs. Cette technique, Proof Carrying Code (PCC), consiste à déploier le code avec une preuve formelle de sa correction. La correction est une propriété inhérente du code reçuu qui ne peut pas être directement déduite du producteur du code. Naturellement, cela donne un avantage à PCC quant-aux méthodes basées sur la confiance à l'autorité d'un tiers. En effet, une signature d'une autorité ne suffit pas à fournir une confiance absolue sur l'exécution du code reçu. Depuis les origines du PCC, le type de mécanisme utilisé pour générer des certificats repose sur des analyses statiques qui font partie du compilateur. Par conséquent, en restant automatique, il est intrinsèquement limité à des propriétés très simples. L'augmentation de l'ensemble des propriétés à considerer est difficile et, dans la plupart des cas, cela exige l'interaction humaine. Une possibilité consiste à vérifier directement le code exécutable. Toutefois, l'absence de structure rend la vérification du code de bas niveau moins naturelle, et donc plus laborieuse. Ceci, combiné avec le fait que la plupart des outils de vérification ciblent le code de haut niveau, rend plus appropriée l'idée de transferer la production de certificats au niveau du code source. Le principal inconvénient de produire des certificats pour assurer l'exactitude du code source est que les preuves ne comportent pas la correction du code compilé. Plusieurs techniques peuvent etre proposées pour transférer la preuve de correction d'un programme à sa version exécutable. Cela implique, par exemple, de déployer le programme source et ses certificats originaux (en plus du code exécutable) et de certifier la correction du processus de compilation. Toutefois, cette approche n'est pas satisfaisante, car en plus d'exiger la disponibilité du code source, la longueur du certificat garantissant la correction du compilation peut être prohibitive. Une alternative plus viable consiste à proposer un mécanisme permettant de générer des certificats de code compilé à partir des certificats du programme source. Les compilateurs sont des procédures complexes composées de plusieurs étapes, parmi lesquelles le programme original est progressivement transformé en représentations intermédiaires. Barthe et al. et Pavlova ont montré que les certificats originaux sont conservés, à quelques différences près non significatives, par la première phase de compilation: la compilation non optimale du code source vers une représentation non structurée de niveau intermédiaire. Toutefois, les optimisations des compilateurs sur les représentations intermédiaires représentent un défi, car a priori les certificats ne peuvent pas être réutilisés. Dans cette thèse, nous analysons comment les optimisations affectent la validité des certificats et nous proposons un mécanisme, Certificate Translation, qui rend possible la génération des certificats pour le code mobile exécutable à partir des certificats au niveau du code source. Cela implique transformer les certificats pour surmonter les effets des optimisations de programme.

Références Bibliographiques

1. E. Albert, G. Puebla, and M. V. Hermenegildo. Abstraction-carrying code. In

F. and A. Voronkov, editors, Logic for Programming Artificial Intel ligence and

Reasoning, number 3452 in Lecture Notes in Computer Science, pages 380–397.

Springer-Verlag, 2005.

2. Alpern, B., Carter, L., and Ferrante, J. Modeling parallel computers as memory

hierarchies. In Proc. Programming Models for Massively Paral lel Computers,

1993.

3. F. Y. Bannwart and P. M¨

uller. A program logic for bytecode. Electronic Notes

in Theoretical Computer Science, 141:255–273, 2005.

4. M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system:

An overview. In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean,

editors, Construction and Analysis of Safe, Secure and Interoperable Smart De-

vices: Proceedings of the International Workshop CASSIS 2004, volume 3362 of

Lecture Notes in Computer Science, pages 151–171. Springer-Verlag, 2005.

5. C. W. Barrett, Y. Fang, B. Goldberg, Y. Hu, A. Pnueli, and L. D. Zuck. Tvoc:

A translation validator for optimizing compilers. In K. Etessami and S. K.

Ra jamani, editors, CAV, number 3576 in Lecture Notes in Computer Science,

pages 291–295. Springer-Verlag, 2005.

6. G. Barthe, B. Gr´egoire, C. Kunz, and T. Rezk. Certificate translation for opti-

mizing compilers. In K. Yi, editor, Static Analysis Symposium, number 4134 in

Lecture Notes in Computer Science, pages 301–317. Springer-Verlag, 2006.

7. G. Barthe, B. Gr´egoire, and M. Pavlova. Preservation of proof obligations for

Java. In International Joint Conference on Automated Reasoning, Lecture Notes

in Computer Science. Springer-Verlag, 2008. To appear.

8. G. Barthe and C. Kunz. Certificate translation in abstract interpretation. In

European Symposium on Programming, number 4960 in Lecture Notes in Com-

puter Science, pages 368–382. Springer-Verlag, 2008.

9. G. Barthe, D. Naumann, and T. Rezk. Deriving an information flow checker

and certifying compiler for Java. In Symposium on Security and Privacy. IEEE

Press, 2006.

10. G. Barthe, T.Rezk, and A. Saabas. Proof obligations preserving compilation.

In T. Dimitrakos, F. Martinelli, P. Ryan, and S. Schneider, editors, Workshop

on Formal Aspects in Security and Trust, number 3866 in Lecture Notes in

Computer Science, pages 112–126. Springer-Verlag, 2005.

11. N. Benton. Simple relational correctness proofs for static analyses and program

transformations. In N. D. Jones and X. Leroy, editors, Principles of Program-

ming Languages, pages 14–25. ACM Press, 2004.

12. Y. Bertot, B. Gr´egoire, and X. Leroy. A structured approach to proving compiler

optimizations based on dataflow analysis. In JC. Filliˆ

atre, C. Paulin-Mohring,

and B. Werner, editors, TYPES, volume 3839 of Lecture Notes in Computer

Science, pages 66–81. Springer, 2004.

13. F. Besson, T. Jensen, and D. Pichardie. Proof-Carrying Code from Certified Ab-

stract Interpretation and Fixpoint Compression. Theoretical Computer Science,

364(3):273–291, 2006. Extended version.

14. F. Besson, T. Jensen, D. Pichardie, and T. Turpin. Result certification for

relational program analysis. Research Report 6333, IRISA, September 2007.

15. Fr´ed´eric Besson, Thomas P. Jensen, and Tiphaine Turpin. Small witnesses for

abstract interpretation-based proofs. In Programming Languages and Systems:

Proceedings of the 16th European Symposium on Programming, ESOP 2007,

number 4421 in Lecture Notes in Computer Science, pages 268–283. Springer-

Verlag, 2007.

16. S. Blazy, Z. Dargaye, and X. Leroy. Formal verification of a c compiler front-end.

In J. Misra, T. Nipkow, and E. Sekerinski, editors, FM, volume 4085 of Lecture

Notes in Computer Science, pages 460–475. Springer, 2006.

17. L. Burdy and M. Pavlova. Java bytecode specification and verification. In

Symposium on Applied Computing, pages 1835–1839. ACM Press, 2006.

18. A. Chaieb. Proof-producing program analysis. In K. Barkaoui, A. Cavalcanti,

and A. Cerone, editors, ICTAC, volume 4281 of Lecture Notes in Computer

Science, pages 287–301. Springer-Verlag, 2006.

19. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for

static analysis of programs by construction or approximation of fixpoints. In

Principles of Programming Languages, pages 238–252, 1977.

20. P. Cousot and R. Cousot. Systematic design of program analysis frameworks.

In Principles of Programming Languages, pages 269–282, 1979.

21. W. J. Dally, F. Labonte, A. Das, P. Hanrahan, J. Ho Ahn, J. Gummara ju,

M. Erez, N. Jayasena, I. Buck, T. J. Knight, and U. J. Kapasi. Merrimac:

Supercomputing with streams. In International Conference on Supercomputing,

page 35. ACM, 2003.

22. D. S. Dantas and D. Walker. Harmless advice. In J. Gregory Morrisett and

Simon L. Peyton Jones, editors, Principles of Programming Languages, pages

383–396. ACM Press, 2006.

23. K. Fatahalian, D. R. Horn, T. J. Knight, L. Leem, M. Houston, J. Y. Park,

M. Erez, M. Ren, A. Aiken, W. J. Dally, and P. Hanrahan. Sequoia: program-

ming the memory hierarchy. In Conference on Supercomputing, page 83. ACM

Press, 2006.

24. J. D. Guttman and M. Wand. Special issue on VLISP. Lisp and Symbolic

Computation, 8(1/2), March 1995.

25. Nicolas Halbwachs and Mathias P´eron. Discovering properties about arrays in

simple programs. In R. Gupta and S. P. Amarasinghe, editors, PLDI, pages

339–348. ACM, 2008.

26. M. V. Hermenegildo and F. Rossi. Strict and nonstrict independent and-

parallelism in logic programs: Correctness, efficiency, and compile-time condi-

tions. J. Log. Program., 22(1):1–45, 1995.

27. M. Houston, J. Young Park, M. Ren, T. Knight, K. Fatahalian, A. Aiken, W. J.

Dally, and P. Hanrahan. A portable runtime interface for multi-level memory

hierarchies. In M. L. Scott, editor, PPOPP. ACM, 2008.

28. U. J. Kapasi, S. Rixner, W. J. Dally, B. Khailany, J. Ho Ahn, P. R. Mattson, and

J. D. Owens. Programmable stream processors. IEEE Computer, 36(8):54–62,

2003.

29. T. J. Knight, J. Young Park, M. Ren, M. Houston, M. Erez, K. Fatahalian,

A. Aiken, W. J. Dally, and P. Hanrahan. Compilation for explicitly man-

aged memory hierarchies. In K. A. Yelick and J. M. Mellor-Crummey, editors,

PPOPP, pages 226–236. ACM, 2007.

30. Shriram Krishnamurthi, Kathi Fisler, and Michael Greenberg. Verifying as-

pect advice modularly. In Richard N. Taylor and Matthew B. Dwyer, editors,

SIGSOFT FSE, pages 137–146. ACM, 2004.

31. P. Laud, T. Uustalu, and V. Vene. Type systems equivalent to data-flow analyses

for imperative languages. Theoretical Computer Science, 364(3):292–310, 2006.

32. K. Rustan M. Leino. Specifying and verifying programs in spec#. In I. Virbit-

skaite and A. Voronkov, editors, Ershov Memorial Conference, volume 4378 of

Lecture Notes in Computer Science, page 20. Springer, 2006.

33. K. Rustan M. Leino and W. Schulte. Exception safety for c#. In SEFM, pages

218–227. IEEE Computer Society, 2004.

34. Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers. Automated

soundness proofs for dataflow analyses and transformations via local rules. In

POPL ’05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on

Principles of programming languages, pages 364–377, New York, NY, USA, 2005.

ACM.

35. X. Leroy. Coinductive big-step operational semantics. In Programming Lan-

guages and Systems: Proceedings of the 15th European Symposium on Program-

ming, ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages

54–68. Springer-Verlag, 2006.

36. X. Leroy. Formal certification of a compiler back-end or: programming a com-

piler with a proof assistant. In J. G. Morrisett and S. L. Peyton Jones, editors,

Principles of Programming Languages, pages 42–54. ACM Press, 2006.

37. Francesco Logozzo and Manuel F¨

ahndrich. On the relative completeness of

bytecode analysis versus source code analysis. In Laurie Hendren, editor, CC,

volume 4959 of Lecture Notes in Computer Science, pages 197–212. Springer,

2008.

38. A. Min´e. Weakly Relational Numerical Abstract Domains. PhD thesis, ´

Ecole

Polytechnique, Palaiseau, France, December 2004. http://www.di.ens.fr/

~mine/these/these- color.pdf.

39. P. M¨

uller and M. Nordio. Proof-transforming compilation of programs with

abrupt termination. In SAVCBS ’07: Proceedings of the 2007 conference on

Specification and verification of component-based systems, pages 39–46, New

York, NY, USA, 2007. ACM.

40. G. C. Necula. Proof-carrying code. In Principles of Programming Languages,

pages 106–119, New York, NY, USA, 1997. ACM Press.

41. G. C. Necula and P. Lee. Safe kernel extensions without run-time checking.

In Operating Systems Design and Implementation, pages 229–243, Seattle, WA,

October 1996. USENIX Assoc.

42. G. C. Necula and P. Lee. The design and implementation of a certifying com-

piler. In Programming Languages Design and Implementation, volume 33, pages

333–344, New York, NY, USA, 1998. ACM Press.

43. G.C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University,

October 1998. Available as Technical Report CMU-CS-98-154.

44. George C. Necula. Translation validation for an optimizing compiler. ACM

SIGPLAN Notices, 35(5):83–94, 2000.

45. M. Nordio, P. M¨

uller, and B. Meyer. Formalizing proof-transforming compila-

tion of eiffel programs. Technical Report 587, ETH Zurich, 2008.

46. M. Nordio, P. M¨

uller, and B. Meyer. Proof-transforming compilation of eiffel

programs. In R. Paige, editor, TOOLS-EUROPE, Lecture Notes in Business

and Information Processing. Springer-Verlag, 2008.

47. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs.

Acta Informatica Journal, 6:319–340, 1975.

48. M. Pavlova. Java bytecode verification and its applications. Th´ese de doctorat,

sp´ecialit´e informatique, Universit´e Nice Sophia Antipolis, France, January 2007.

49. A. Pnueli, E. Singerman, and M. Siegel. Translation validation. In B. Steffen,

editor, Tools and Algorithms for the Construction and Analysis of Systems,

volume 1384 of Lecture Notes in Computer Science, pages 151–166. Springer-

Verlag, 1998.

50. X. Rival. Symbolic Transfer Functions-based Approaches to Certified Compila-

tion. In Principles of Programming Languages, pages 1–13. ACM Press, 2004.

51. A. Saabas and T. Uustalu. A compositional natural semantics and Hoare logic

for low-level languages. Theoretical Computer Science, 373(3):273–302, 2007.

52. A. Saabas and T. Uustalu. Type systems for optimizing stack-based code. In

M. Huisman and F. Spoto, editors, Bytecode Semantics, Verification, Analysis

and Transformation, volume 190(1) of Electronic Notes in Theoretical Computer

Science, pages 103–119. Elsevier, 2007.

53. A. Saabas and T. Uustalu. Program and proof optimizations with type systems.

Journal of Logic and Algebraic Programming, 77(1–2):131–154, 2008.

54. S. Seo, H. Yang, and K. Yi. Automatic Construction of Hoare Proofs from

Abstract Interpretation Results. In A. Ohori, editor, Asian Programming Lan-

guages and Systems Symposium, volume 2895 of Lecture Notes in Computer

Science, pages 230–245. Springer-Verlag, 2003.

55. Z. Shao, V. Trifonov, B. Saha, and N. Papaspyrou. A type system for certified

binaries. ACM Trans. Program. Lang. Syst., 27(1):1–45, 2005.

56. M. Strecker. Formal Verification of a Java Compiler in Isabelle. In A. Voronkov,

editor, Conference on Automated Deduction, volume 2392 of Lecture Notes in

Computer Science, pages 63–77, London, UK, 2002. Springer-Verlag.

57. D. Tarditi, J. Gregory Morrisett, Perry Cheng, Chris Stone, Robert Harper, and

Peter Lee. TIL: A type-directed optimizing compiler for ML. In Programming

Languages Design and Implementation, pages 181–192. Association of Comput-

ing Machinery, 1996.

58. J. Tristan and X. Leroy. Formal verification of translation validators: a case

study on instruction scheduling optimizations. SIGPLAN Not., 43(1):17–27,

2008.

59. M. Wildmoser, A. Chaieb, and T. Nipkow. Bytecode analysis for proof carry-

ing code. In F. Spoto, editor, Bytecode Semantics, Verification, Analysis and

Transformation, volume 141 of Electronic Notes in Theoretical Computer Sci-

ence. Elsevier, 2005.

60. M. Wildmoser, T. Nipkow, G. Klein, and S. Nanz. Prototyping proof carrying

code. In J-J. Levy, E. W. Mayr, and J. C. Mitchell, editors, Theoretical Computer

Science, pages 333–347. Kluwer Academic Publishing, August 2004.

61. H. Xi and S. Xia. Towards array bound check elimination in java tm virtual

machine language. In CASCON ’99: Proceedings of the 1999 conference of the

Centre for Advanced Studies on Col laborative research, page 14. IBM Press,

1999.

62. L. D. Zuck, A. Pnueli, Y. Fang, and B. Goldberg. Voc: A translation validator

for optimizing compilers. Electronic Notes in Theoretical Computer Science,

65(2), 2002.

Table des Matières

Part I Foundations of Certificate Translation

1 Certificate Translation alongside Standard RTL

Optimizations - 3

1.0.1 Contents - 6

1.1 PCC Setting - 7

1.1.1 RTL Language - 7

1.1.2 Operational Semantics - 9

1.1.3 Verification Condition Generator - 9

1.1.4 Certified Programs - 11

1.1.5 Soundness of PCC Infrastructure - 12

1.2 Preservation of Proof Obligations - 14

1.2.1 Source Language - 14

1.2.2 Compilation - 16

1.2.3 Preservation of Proof Obligations - 17

1.3 Certificate Translation for Common Optimizations - 18

1.3.1 Overview - 18

1.3.2 Constant Propagation - 22

Description - 22

Certifying analyzer - 22

Certificate translation - 23

1.3.3 Loop Induction Variable Strength Reduction - 25

Description - 25

Certifying analyzer - 26

Certificate translation - 27

1.3.4 Common Subexpression Elimination - 29

Description - 29

1.3.5 Copy Propagation - 30

Description - 30

Certificate translation - 31

1.3.6 Dead Register Elimination - 32

Description - 32

Certificate translation - 34

1.3.7 Unreachable Code Elimination - 36

Description - 36

Certificate translation - 37

1.3.8 Register Allocation - 37

Description - 37

Certificate translation - 38

1.3.9 Function Inlining - 39

Description - 39

Certificate translation - 40

1.3.10 Summary - 41

2 An Abstract Interpretation Model of Certificate Translation 43

2.1 Introduction - 43

2.2 Program, Semantics, Abstract Interpretation - 45

2.2.1 Program, Semantics - 45

2.2.2 Abstract Interpretations of Program Semantics - 46

Solutions - 49

2.2.3 Certified Solutions - 50

2.3 Certifying Analyzers - 53

2.4 Certificate Translation - 56

2.4.1 Code Duplication - 56

2.4.2 Edge Transformation - 58

2.4.3 Program Representation Abstraction - 63

2.4.4 Second-Order Analysis-Based Optimizations - 68

2.4.5 Concurrency - 71

2.4.6 Example - 77

Part II Case Studies

3 Specification Preserving Advice Weaving - 87

3.1 Introduction - 87

3.2 A basic motivating example - 87

3.3 A simple AOP language - 89

3.3.1 Syntax - 89

3.3.2 Semantics - 89

3.4 Verification of baseline code - 91

3.5 Verifying AOP programs - 92

3.5.1 Specification-preserving advices - 92

3.5.2 Example - 93

3.5.3 Harmless advices - 94

3.5.4 Beyond harmless advices - 94

3.6 Compiling advices - 95

3.6.1 Target language - 95

3.6.2 Compiler - 96

3.7 Certificate translation - 97

3.7.1 Verification of SBL programs - 98

3.7.2 Preservation of validity - 99

3.8 Increasing the Power of Verification - 100

4 Preservation of Proof Obligations in Hybrid

Verification Environments - 105

4.1 Setting - 106

4.2 Preservation of solutions - 108

4.3 Preservation of proof obligations - 115

4.4 From hybrid VCgen to VCgen - 120

5 Certified Analysis in Hierarchical Memory Models - 123

5.1 A primer on Sequoia - 123

5.2 Analyzing and reasoning about Sequoia programs - 127

5.2.1 Program Analysis - 127

5.2.2 Program Safety - 129

5.2.3 Program Verification - 132

5.2.4 Example Program - 135

5.3 Certificate translation - 135

5.4 General framework - 137

5.4.1 Certifying analyzers - 137

5.4.2 Certificate translation - 139

5.4.3 Copy propagation for arrays - 140

5.5 Sequoia Specific Optimizations - 141

5.5.1 SPMD Distribution - 141

5.5.2 Exec Grouping - 143

5.5.3 Copy Grouping - 145

Part III Related Work and Conclusion

References - 161

Statistiques de consultation

Administrateurs de l'archive uniquement : éditer cet enregistrement