- Drew Dean
- 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.
Fourth ACM Conference on Computer and Communications Security,
- GZip'ed Postscript (49k)
PDF (Adobe Acrobat 2.1) (154k)