{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T10:40:02Z","timestamp":1748601602713,"version":"3.41.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T00:00:00Z","timestamp":1716422400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T00:00:00Z","timestamp":1716422400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"European Union\u2019s Horizon 2020","award":["956123"],"award-info":[{"award-number":["956123"]}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["W1255-N23"],"award-info":[{"award-number":["W1255-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100019180","name":"HORIZON EUROPE European Research Council","doi-asserted-by":"publisher","award":["01020093","ZK-35","10.55776\/F85"],"award-info":[{"award-number":["01020093","ZK-35","10.55776\/F85"]}],"id":[{"id":"10.13039\/100019180","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between <jats:italic>assumptions<\/jats:italic>, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and <jats:italic>guarantees<\/jats:italic>, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an <jats:italic>interface theory<\/jats:italic>, 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 <jats:italic>stateless<\/jats:italic> and <jats:italic>stateful<\/jats:italic> interfaces. Additionally, we introduce information-flow contracts where <jats:italic>assumptions<\/jats:italic> and <jats:italic>guarantees<\/jats:italic> 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.<\/jats:p>","DOI":"10.1007\/s10703-024-00447-0","type":"journal-article","created":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T09:02:12Z","timestamp":1716454932000},"page":"3-48","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Information-flow interfaces"],"prefix":"10.1007","volume":"66","author":[{"given":"Ezio","family":"Bartocci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Ferr\u00e8re","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dejan","family":"Nickovic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8741-5799","authenticated-orcid":false,"given":"Ana","family":"Oliveira da Costa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,23]]},"reference":[{"key":"447_CR1","doi-asserted-by":"publisher","unstructured":"Bartocci E, Ferr\u00e8re T, Henzinger TA, Nickovic D, da Costa AO (2022) Information-flow interfaces. In: Proceedings of FASE 2022: the 25th international conference on fundamental approaches to software engineering. LNCS, vol 13241. pp 3\u201322. https:\/\/doi.org\/10.1007\/978-3-030-99429-7","DOI":"10.1007\/978-3-030-99429-7"},{"key":"447_CR2","doi-asserted-by":"publisher","first-page":"13260","DOI":"10.1109\/ACCESS.2019.2891969","volume":"7","author":"D Ratasich","year":"2019","unstructured":"Ratasich D, Khalid F, Geissler F, Grosu R, Shafique M, Bartocci E (2019) A roadmap toward the resilient internet of things for cyber-physical systems. IEEE Access 7:13260\u201313283. https:\/\/doi.org\/10.1109\/ACCESS.2019.2891969","journal-title":"IEEE Access"},{"key":"447_CR3","doi-asserted-by":"crossref","unstructured":"Mantel H (2002) On the composition of secure systems. In: IEEE Symposium on security and privacy, pp 88\u2013101. 10.1109\/SECPRI.2002.1004364","DOI":"10.1109\/SECPRI.2002.1004364"},{"key":"447_CR4","doi-asserted-by":"crossref","unstructured":"Mantel H, Sands D, Sudbrock H (2011) Assumptions and guarantees for compositional noninterference. In: IEEE Computer security foundations symposium (CSF), pp 218\u2013232. 10.1109\/CSF.2011.22","DOI":"10.1109\/CSF.2011.22"},{"issue":"1","key":"447_CR5","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider FB (2000) Enforceable security policies. ACM Trans Inform Syst Secur 3(1):30\u201350. https:\/\/doi.org\/10.1145\/353323.353382","journal-title":"ACM Trans Inform Syst Secur"},{"issue":"1","key":"447_CR6","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld A, Myers AC (2003) Language-based information-flow security. IEEE J Sel Areas Commun 21(1):5\u201319. https:\/\/doi.org\/10.1109\/JSAC.2002.806121","journal-title":"IEEE J Sel Areas Commun"},{"issue":"6","key":"447_CR7","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C Hammer","year":"2009","unstructured":"Hammer C, Snelting G (2009) Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int J Inf Secur 8(6):399\u2013422. https:\/\/doi.org\/10.1007\/s10207-009-0086-1","journal-title":"Int J Inf Secur"},{"key":"447_CR8","doi-asserted-by":"publisher","first-page":"143","DOI":"10.3233\/978-1-60750-714-7-143","volume":"5","author":"R Focardi","year":"2011","unstructured":"Focardi R, Maffei M (2011) Types for security protocols. Formal Models Tech Anal Secur Protoc 5:143\u2013181. https:\/\/doi.org\/10.3233\/978-1-60750-714-7-143","journal-title":"Formal Models Tech Anal Secur Protoc"},{"key":"447_CR9","doi-asserted-by":"publisher","unstructured":"Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, S\u00e1nchez C (2014) Temporal logics for hyperproperties. In: Principles of security and trust (POST). LNCS, vol 8414. pp 265\u2013284. https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"2","key":"447_CR10","doi-asserted-by":"publisher","first-page":"299","DOI":"10.5755\/j01.itc.48.2.21759","volume":"48","author":"M Mikulcak","year":"2019","unstructured":"Mikulcak M, Herber P, G\u00f6thel T, Glesner S (2019) Information flow analysis of combined simulink\/stateflow models. Inform Technol Control 48(2):299\u2013315. https:\/\/doi.org\/10.5755\/j01.itc.48.2.21759","journal-title":"Inform Technol Control"},{"issue":"6","key":"447_CR11","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson MR, Schneider FB (2010) Hyperproperties. J Comput Secur 18(6):1157\u20131210. https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J Comput Secur"},{"key":"447_CR12","doi-asserted-by":"publisher","unstructured":"Hamilton MD, Tunstall M, Popovici EM, Marnane WP (2008) Side channel analysis of an automotive microprocessor. In: IET Irish signals and systems conference (ISSC), pp 4\u20139. https:\/\/doi.org\/10.1049\/cp:20080630","DOI":"10.1049\/cp:20080630"},{"key":"447_CR13","unstructured":"Verdult R, Garcia FD, Balasch J (2012) Gone in 360 seconds: Hijacking with hitag2. In: 21st USENIX Security symposium, pp 237\u2013252"},{"key":"447_CR14","unstructured":"Benadjila R, Renard M, Lopes-Esteves J, Kasmi C (2017) One car, two frames: attacks on hitag-2 remote keyless entry systems revisited. In: 11th USENIX Workshop on offensive technologies"},{"issue":"2\u20133","key":"447_CR15","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste A, Caillaud B, Nickovic D, Passerone R, Raclet J, Reinkemeier P, Sangiovanni-Vincentelli AL, Damm W, Henzinger TA, Larsen KG (2018) Contracts for system design. Found Trends Electron Des Autom 12(2\u20133):124\u2013400. https:\/\/doi.org\/10.1561\/1000000053","journal-title":"Found Trends Electron Des Autom"},{"key":"447_CR16","doi-asserted-by":"publisher","unstructured":"de Alfaro L, Henzinger TA (2001) Interface theories for component-based design. In: Embedded software. LNCS, vol 2211. pp 148\u2013165. https:\/\/doi.org\/10.1007\/3-540-45449-7_11","DOI":"10.1007\/3-540-45449-7_11"},{"key":"447_CR17","doi-asserted-by":"publisher","unstructured":"de Alfaro L, Henzinger TA (2005) Interface-based design. In: Engineering theories of software intensive systems. NATO science series (Series II: mathematics, physics and chemistry), vol 195, pp 83\u2013104. https:\/\/doi.org\/10.1007\/1-4020-3532-2_3","DOI":"10.1007\/1-4020-3532-2_3"},{"issue":"4","key":"447_CR18","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1985342.1985345","volume":"33","author":"S Tripakis","year":"2011","unstructured":"Tripakis S, Lickly B, Henzinger TA, Lee EA (2011) A theory of synchronous relational interfaces. ACM Trans Progr Lang Syst TOPLAS 33(4):14. https:\/\/doi.org\/10.1145\/1985342.1985345","journal-title":"ACM Trans Progr Lang Syst TOPLAS"},{"key":"447_CR19","doi-asserted-by":"publisher","unstructured":"Chakrabarti A, de Alfaro L, Henzinger TA, Stoelinga M (2003) Resource interfaces. In: Embedded software. LNCS, vol 2855. pp 117\u2013133. https:\/\/doi.org\/10.1007\/978-3-540-45212-6_9","DOI":"10.1007\/978-3-540-45212-6_9"},{"key":"447_CR20","doi-asserted-by":"publisher","unstructured":"de Alfaro L, Henzinger TA, Stoelinga M (2002) Timed interfaces. In: Embedded software. LNCS vol 2491. pp 108\u2013122. https:\/\/doi.org\/10.1007\/3-540-45828-X_9","DOI":"10.1007\/3-540-45828-X_9"},{"key":"447_CR21","doi-asserted-by":"publisher","unstructured":"David A, Larsen KG, Legay A, Nyman U, Wasowski A (2010) Timed I\/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM international conference on hybrid systems: computation and control (HSCC), pp 91\u2013100. https:\/\/doi.org\/10.1145\/1755952.1755967","DOI":"10.1145\/1755952.1755967"},{"key":"447_CR22","doi-asserted-by":"publisher","unstructured":"Larsen KG, Nyman U, Wasowski A (2006) Interface input\/output automata. In: Misra J, Nipkow T, Sekerinski E (eds) International symposium on formal methods (FM). LNCS, vol 4085, pp 82\u201397. https:\/\/doi.org\/10.1007\/11813040_7","DOI":"10.1007\/11813040_7"},{"key":"447_CR23","doi-asserted-by":"publisher","unstructured":"Lemke K, Sadeghi A-R, St\u00fcble C (2005) An open approach for designing secure electronic immobilizers. In: Proceedings of ISPEC 2005. LNCS, vol 3439, pp 230\u2013242. https:\/\/doi.org\/10.1007\/978-3-540-31979-5_20","DOI":"10.1007\/978-3-540-31979-5_20"},{"key":"447_CR24","doi-asserted-by":"publisher","unstructured":"Benveniste A, Caillaud B, Ferrari A, Mangeruca L, Passerone R, Sofronis C (2008) Multiple viewpoint contract-based specification and design. In: Proceedings of FMCO 2007: the 6th International symposium on formal methods for components and objects. lecture notes in computer science, vol 5382. Springer, pp 200\u2013225. https:\/\/doi.org\/10.1007\/978-3-540-92188-2_9","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"447_CR25","doi-asserted-by":"publisher","unstructured":"Alur R, Henzinger TA, Kupferman O, Vardi MY (1998) Alternating refinement relations. In: CONCUR\u201998 Concurrency theory. LNCS, vol 1466. Springer, pp 163\u2013178. https:\/\/doi.org\/10.1007\/BFb0055622","DOI":"10.1007\/BFb0055622"},{"key":"447_CR26","unstructured":"Graf J, Hecker M, Mohr M (2013) Using JOANA for information flow control in Java programs\u2014a practical guide. In: Software engineering 2013 - Workshopband. LNI, vol P-215, pp 123\u2013138. https:\/\/dl.gi.de\/20.500.12116\/17361"},{"key":"447_CR27","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Annual symposium on foundations of computer science (FOCS), pp 46\u201357. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"447_CR28","doi-asserted-by":"publisher","unstructured":"Bozzelli L, Maubert B, Pinchinat S (2015) Unifying hyper and epistemic temporal logics. In: Foundations of software science and computation structures (FoSSaCS). LNCS, vol 9034, pp 167\u2013182. https:\/\/doi.org\/10.1007\/978-3-662-46678-0_11","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"447_CR29","doi-asserted-by":"publisher","unstructured":"Balliu M, Dam M, Le\u00a0Guernic G (2011) Epistemic temporal logic for information flow security. In: Proceedings of the ACM SIGPLAN 6th workshop on programming languages and analysis for security (PLAS), pp 1\u201312. https:\/\/doi.org\/10.1145\/2166956.2166962","DOI":"10.1145\/2166956.2166962"},{"issue":"10","key":"447_CR30","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer B (1992) Applying design by contract. Computer 25(10):40\u201351. https:\/\/doi.org\/10.1109\/2.161279","journal-title":"Computer"},{"key":"447_CR31","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-94-011-1793-7_4","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd RW (1967) Assigning meanings to programs. Proceed Symp Appl Math 19:19\u201332. https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","journal-title":"Proceed Symp Appl Math"},{"issue":"10","key":"447_CR32","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580. https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun ACM"},{"key":"447_CR33","doi-asserted-by":"publisher","unstructured":"de Alfaro L, Henzinger TA (2001) Interface automata. In: European software engineering conference\/foundations on software engineering (ESEC\/FSE), pp 109\u2013120. https:\/\/doi.org\/10.1145\/503209.503226","DOI":"10.1145\/503209.503226"},{"issue":"1","key":"447_CR34","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2010.07.008","volume":"264","author":"M Lee","year":"2010","unstructured":"Lee M, D\u2019Argenio PR (2010) Describing secure interfaces with interface automata. Electron Notes Theor Comput Sci 264(1):107\u2013123. https:\/\/doi.org\/10.1016\/j.entcs.2010.07.008","journal-title":"Electron Notes Theor Comput Sci"},{"key":"447_CR35","doi-asserted-by":"publisher","unstructured":"Incer I, Benveniste A, Sangiovanni-Vincentelli AL, Seshia SA (2022) Hypercontracts. In: Proceedings of NFM 2022: the 14th International symposium. LNCS, vol 13260. pp 674\u2013692. https:\/\/doi.org\/10.1007\/978-3-031-06773-0","DOI":"10.1007\/978-3-031-06773-0"},{"issue":"1\u20132","key":"447_CR36","doi-asserted-by":"publisher","first-page":"119","DOI":"10.3233\/FI-2011-416","volume":"108","author":"J-B Raclet","year":"2011","unstructured":"Raclet J-B, Badouel E, Benveniste A, Caillaud B, Legay A, Passerone R (2011) A modal interface theory for component-based design. Fund Inform 108(1\u20132):119\u2013149. https:\/\/doi.org\/10.3233\/FI-2011-416","journal-title":"Fund Inform"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00447-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00447-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00447-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T10:01:25Z","timestamp":1748599285000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00447-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,23]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,5]]}},"alternative-id":["447"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00447-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2024,5,23]]},"assertion":[{"value":"29 December 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 February 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 May 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}