Secure Linking: a Framework for Trusted Software Components (Extended Version)
Deciding whether or not
to trust a foreign software component is important
for the safety of a host which imports the component.
The decision can be made
in a static situation
where the main concern is building a large software system out of
many components from different parties, as well as
in a dynamic situation where the main concern is executing codes transferred via networks.
Recently some linkers have started concerning about
trusting foreign code at the component level, and
type checking and digital signing are the main ways of achieving the goal.
We propose a way of linking software components with certified assurances (called properties)
and proof-carrying authentication.
We have developed a framework for secure linking systems,
which consists of the logic expressing the linking procedure
and the prover finding proofs for proof-carrying authentication.
The framework is general and expressive enough to represent other exis
ting linking systems
and to help different linking systems interoperate.