End-to-end availability policies and noninterference

This paper introduces the use of static information flow analysis for the specification and enforcement of end-to-end availability policies in programs. We generalize the decentralized label model, which is about confidentiality and integrity, to also include security policies for availability. These policies characterize acceptable risks by representing them as principals. We show that in this setting, a suitable extension of noninterference corresponds to a strong, end-to-end availability guarantee. This approach provides a natural way to specify availability policies and enables existing static dependency analysis techniques to be adapted for availability. The paper presents a simple language in which fine-grained information security policies can be specified as type annotations. These annotations can include requirements for all three major security properties: confidentiality, integrity, and availability. The type system for the language provably guarantees that any well-typed program has the desired noninterference properties, ensuring confidentiality, integrity, and availability.