| Programming language-based security provides applications programmers with greater control and flexibility for specifying and enforcing security policies. As computing environments distribute and diversify, and demands for program mobility increase, this power allows programmers to adapt software to developing needs, while still protecting resources. This thesis advocates the use of static type disciplines for expressing and enforcing programming language-based security. We develop type systems for two popular security models: the Access Control model with Stack Inspection , and the Object Confinement model. Type safety proofs demonstrate that these type systems reliably enforce security statically, and imply that certain run-time optimizations may be effected for programs. The declarative nature of our type terms also provide programmers with useful and understandable descriptions of security properties. To formally develop these type systems, a transformational approach is used, where source languages are embedded in a target language, containing sets of atomic elements and associated operations, which is pre-equipped with a sound type system. This target language and type system is developed using the type constraint framework HM(X). The transformational approach and HM(X) both allow the re-use of existing theory and implementations, easing proof effort, inspiring design, and providing greater confidence in the correctness of results. |
