Secure Linking: A Logical Framework for Policy-Enforced Component Composition

Abstract:

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.