Security Properties of Typed Applets

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 applets possess, and identify sufficient conditions for the applet execution environment to be safe, such as procedural ation, 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: Conference
• Year: 1999
• Where: ECOOPW
• Authors: Xavier Leroy, François Rouaix
• Keywords: Distributed And Parallel Computing, ECOOPW 1999, Execution Environments, Strongly-typed Applets, Well-typed Applets Possess