# Information-flow interfaces

## TL;DR

This paper introduces a new framework for designing secure systems using contracts that manage information flow and ensure security properties.

## Contribution

The paper presents the first interface theory specifically designed to ensure system-wide security properties.

## Key findings

- The framework supports refinement and composition for both stateless and stateful interfaces.
- Information-flow contracts are introduced to enrich interfaces with a semantic view.
- The framework's applicability is demonstrated with examples from the automotive domain.

## Abstract

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 designed to ensure system-wide security properties. 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. Additionally, we introduce information-flow contracts where assumptions and guarantees are sets of flow relations. We use these contracts to illustrate how to enrich information-flow interfaces with a semantic view. We illustrate the applicability of our framework with two examples inspired by the automotive domain.