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 applets possess, and iden- tify su‐cient conditions for the applet execution environment to be safe, such as procedural encapsulation, type abstraction, and systematic type- based placement of run-time checks. These results are a flrst step towards formal techniques for developing and validating safe execution environ- ments for applets.