Sécurité du code mobile en terme de types : application au langage JAVA
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
Type safety of a programming language means in particular that no buffer overflow attack ispossible upon software written in that language. Sun proclaimed Java to be typesafe just on it's birthday. From this day forward a lot of efforts were doneto demonstrate formally the type safety property. Various researches in thatdirection proved clearly that the Java type system can not be compromised atcompile time. Nevertheless V. Saraswat showed that (early version of) Java virtualmachine (JVM) may be corrupted at run time. A kind of constraint system wasproposed by S. Liang and G. Bracha to fix the bug, but actually their solutioncan not be taken for granted, notwithstanding the fact that it assures run-time typesafety. Two main aims of the thesis are: first, to make the above mentionedapproach applicable and, second, to generalize the equivalence relation onclasses and to obtain a new compatibility relation that is much more flexibleas far as class replacement is concerned. On the other hand, good semantic properties of Java language give still no guarantee of type safetyif the substitution of compatible but not equivalent classes is permitted. Toget it, one needs to study in depth low level virtual machine properties alongwith memory allocation problems.
Abstract FR:
Pour un langage, possèder la propriété de sûreté du système de typage, c'est contrecarrer d'emblée toutes les attaques basées sur le principe de dépassement de tampon. Dès la naissance du langage {\sc Java}, {\sc sun} a proclamé qu'il possèdait cette propriété. De fait, beaucoup d'études se sont attachées à montrer la sûreté du système de typage de {\sc Java}. Si toutes ces études montrent bien qu'il n'est pas possible d'aboutir à une inconsistance du système de typage lors de la phase de compilation, V. Saraswat a, quant à lui, montré que les premières machines virtuelles permettaient de corrompre le système en phase d'exécution. Suite au bug découvert par Saraswat, Liang et Bracha ont mis en place un système de contraintes permettant d'assurer en temps d'exécution la sûreté du système de typage. Ce système n'est toutefois pas applicable tel quel. L'objectif de cette thèse est dans un premier temps de le rendre applicable, puis dans un deuxième temps, d'élargir la notion d'équivalence entre les classes à une compatibilité. Le passage à une compatibilité entre les classes permet une plus grande souplesse dans le remplacement entre ces dernières. Toutefois, on ne peut alors plus compter sur la sémantique du langage pour assurer la sûureté du système de types. Il faut modifier la machine virtuelle elle-même pour assurer, dans le cadre d'une affectation de classes compatibles mais non équivalentes, la préservation du système de typage physique dans la mémoire.