article published yes Ezio Bartocci author Thomas Ferrere author 40960E6E-F248-11E8-B48F-1D18A9856A870000-0001-5199-3143 Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Dejan Nickovic author 41BCEE5C-F248-11E8-B48F-1D18A9856A87 Ana Oliveira da Costa author f347ec37-6676-11ee-b395-a888cb7b4fb40000-0002-8741-5799 ToHe department Vigilant Algorithmic Monitoring of Software project Interface Theory for Security and Privacy project 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. https://research-explorer.ista.ac.at/download/17094/20879/2025_FormalMethodsSysDesign_Bartocci.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Springer Nature2025 eng 0925-9856 1572-8102 2002.06465 00123008420000110.1007/s10703-024-00447-0 663-48 https://research-explorer.ista.ac.at/record/11355 Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Information-flow interfaces. Formal Methods in System Design. 66, 3–48. Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Formal Methods in System Design</i>, vol. 66, Springer Nature, 2025, pp. 3–48, doi:<a href="https://doi.org/10.1007/s10703-024-00447-0">10.1007/s10703-024-00447-0</a>. Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Information-flow interfaces. <i>Formal Methods in System Design</i>. Springer Nature. <a href="https://doi.org/10.1007/s10703-024-00447-0">https://doi.org/10.1007/s10703-024-00447-0</a> Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Information-Flow Interfaces.” <i>Formal Methods in System Design</i>. Springer Nature, 2025. <a href="https://doi.org/10.1007/s10703-024-00447-0">https://doi.org/10.1007/s10703-024-00447-0</a>. Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-flow interfaces. <i>Formal Methods in System Design</i>. 2025;66:3-48. doi:<a href="https://doi.org/10.1007/s10703-024-00447-0">10.1007/s10703-024-00447-0</a> E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-flow interfaces,” <i>Formal Methods in System Design</i>, vol. 66. Springer Nature, pp. 3–48, 2025. E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Formal Methods in System Design 66 (2025) 3–48. 170942024-06-02T22:00:57Z2025-12-30T06:50:51Z