2020/02/15 by Ezio Bartocci, Bartocci, Ezio, Thomas Ferrère +7
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Information and Cyber Security #Logic in Computer Science (cs.LO) #Safety Systems Engineering in Autonomy #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2002.06465
openalex publication_date 2020/02/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.