Secure linking: A logical framework for policy-enforced component composition

In this thesis I propose a flexible way of allowing software component users to specify their security policies, and to-endow digitally signed certificates with more expressive power at link time. Secure Linking (SL) is more flexible than type-checking or other static checking mechanisms because it allows users the freedom to specify security policies at link time. In addition, Secure Linking is more expressive than simple digital signing by restricting the scope of guarantees made by digitally signed certificates. Secure Linking would not prevent bugs in a software component, but it gives people signing a software component finer-grain control of the meaning of their certificates.; The linking logic in the Secure Linking framework is based on Proof-Carrying Authentication (PCA), a distributed authentication/authorization framework. In Secure Linking, a code consumer establishes a linking policy to protect itself from malicious code from outside. The policy can include certain properties required by the code consumer for system safety, such as software component names, application-specific correctness properties, version information of software components, and so on. In order for a software component to run in the system of a code consumer, there must be a machine-checkable proof that the component has the properties specified in the code consumer's linking policy. This proof might be provided by the code provider, or might be produced by an untrusted proving algorithm that runs on the code consumer's machine. The proof is formed using the logic and inference rules of the framework. After being submitted, the proof is checked by a small trusted proof checker in the code consumer, and if verified, the component is allowed to be linked to other components in the code consumer.; I demonstrate that the Secure Linking logic is flexible enough to interoperate with other application-specific and security-concerned logics. I show that the Secure Linking logic is expressive enough to describe real-world linking systems. I also describe a prototype implementation of Secure Linking for Java components.