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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/hal-01499963
Contributor : Xavier Leroy <>
Submitted on : Saturday, April 1, 2017 - 7:19:29 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on : Sunday, July 2, 2017 - 1:00:48 PM

File

typed-applets.pdf
Files produced by the author(s)

Identifiers

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. pp.391-403, ⟨10.1145/268946.268979⟩. ⟨hal-01499963⟩

Share

Metrics

Record views

334

Files downloads

127