Security properties of typed applets

Abstract : This paper formalizes the folklore result that strongly-typed applets are more secure than untyped ones. We formulate and prove several security properties that all well-typed ap-plets possess, and identify sufficient conditions for the ap-plet execution environment to be safe, such as procedural encapsulation, type abstraction, and systematic type-based placement of run-time checks. These results are a first step towards formal techniques for developing and validating safe execution environments for applets.
Type de document :
Communication dans un congrès
POPL 1998: 25th symposium Principles of Programming Languages, Jan 1998, San Diego, United States. ACM, pp.391-403, 〈10.1145/268946.268979〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01499963
Contributeur : Xavier Leroy <>
Soumis le : samedi 1 avril 2017 - 19:19:29
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : dimanche 2 juillet 2017 - 13:00:48

Fichier

typed-applets.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy, François Rouaix. Security properties of typed applets. POPL 1998: 25th symposium Principles of Programming Languages, Jan 1998, San Diego, United States. ACM, pp.391-403, 〈10.1145/268946.268979〉. 〈hal-01499963〉

Partager

Métriques

Consultations de la notice

309

Téléchargements de fichiers

50