  Contract-based design is a promising methodology for taming the complexity of
developing sophisticated systems. A formal contract distinguishes between
assumptions, which are constraints that the designer of a component puts on the
environments in which the component can be used safely, and guarantees, which
are promises that the designer asks from the team that implements the
component. A theory of formal contracts can be formalized as an interface
theory, which supports the composition and refinement of both assumptions and
guarantees. Although there is a rich landscape of contract-based design methods
that address functional and extra-functional properties, we present the first
interface theory that is designed for ensuring system-wide security properties,
thus paving the way for a science of safety and security co-engineering. Our
framework provides a refinement relation and a composition operation that
support both incremental design and independent implementability. We develop
our theory for both stateless and stateful interfaces. We illustrate the
applicability of our framework with an example inspired from the automotive
domain. Finally, we provide three plausible trace semantics to stateful
information-flow interfaces and we show that only two correspond to temporal
logics for specifying hyperproperties, while the third defines a new class of
hyperproperties that lies between the other two classes.
