The security of static typing with dynamic linking

Abstract

Dynamic linking is a requirement for portable executable content. Executable content cannot know, ahead of time, where it is going to be executed, nor know the proper operating system interface. This imposes a requirement for dynamic linking. At the same time, we would like languages supporting executable content to be statically typable, for increased efficiency and security. Static typing and dynamic linking interact in a security-relevant way. This interaction is the subject of this paper. One solution is modeled in PVS, and formally proven to be safe.