Secure component composition with modular behavioral properties

We propose a flexible way of allowing the users of software components to specify their security policies, and 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 with endowing users the freedom to specify security policies at link time, and SL is more expressive than simple digital signing with restricting the scope of guarantees made by digitally signed certificates. SL would not prevent bugs in a software component, but it gives signers of software components finer-grain control of the meaning of their certificates. We implemented a logic-based framework for SL, which consists of the SL logic, a proof verifier, a tactical prover, and user interface languages. The framework of SL encompasses the existing constraint languages, such as OCL and JML, so the security policies and the property statements of software components can be written easily using those popular languages. In this paper, we explain the linking protocol of SL, the SL framework, and the extended user interface languages with OCL and JML. We also discuss the strength of the proposed linking protocol in developing practical software systems.