{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T08:29:03Z","timestamp":1676968143539},"reference-count":32,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,2]]},"abstract":"<jats:p>We propose a framework for reasoning about program security building on language-theoretic and coalgebraic concepts. The behaviour of a system is viewed as a mapping from traces of high (unobservable) events to low (observable) events: the less the degree of dependency of low events on high traces, the more secure the system. We take the abstract view that low events are drawn from a generic <jats:italic>semiring<\/jats:italic>, where they can be combined using product and sum operations; throughout the paper, we provide instances of this framework, obtained by concrete instantiations of the underlying semiring. We specify systems via a simple process calculus, whose semantics is given as the unique homomorphism from the calculus into the set of behaviours, i.e. <jats:italic>formal power series<\/jats:italic>, seen as a final coalgebra. We provide a compositional semantics for the calculus in terms of rational operators on formal power series and show that the final and the compositional semantics coincide. This compositional, syntax-driven framework lays a foundation for automation and abstraction of a quantified approach to flow security of system specifications.<\/jats:p>","DOI":"10.1017\/s0960129513000601","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T17:58:27Z","timestamp":1415642307000},"page":"259-291","source":"Crossref","is-referenced-by-count":3,"title":["A semiring-based trace semantics for processes with applications to information leakage analysis"],"prefix":"10.1017","volume":"25","author":[{"given":"MICHELE","family":"BOREALE","sequence":"first","affiliation":[]},{"given":"DAVID","family":"CLARK","sequence":"additional","affiliation":[]},{"given":"DANIELE","family":"GORLA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129513000601_ref28","first-page":"49","volume-title":"Proceedings of ARES","author":"Mu","year":"2009"},{"key":"S0960129513000601_ref32","first-page":"144","volume-title":"Proceedings of Symposium on Security and Privacy","author":"Wittbold","year":"1990"},{"key":"S0960129513000601_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11145-7_17"},{"key":"S0960129513000601_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.02.007"},{"key":"S0960129513000601_ref15","first-page":"413","volume-title":"Proceedings of LICS","author":"Desharnais","year":"2002"},{"key":"S0960129513000601_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951"},{"key":"S0960129513000601_ref12","first-page":"189","volume-title":"Proceedings of CCS","author":"Chong","year":"2004"},{"key":"S0960129513000601_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.07.003"},{"key":"S0960129513000601_ref25","first-page":"18","volume-title":"Proceedings of CSFW","author":"Lowe","year":"2002"},{"key":"S0960129513000601_ref30","article-title":"Language-based information-flow security","volume":"21","author":"Sabelfeld","year":"2003","journal-title":"IEEE Journal on Selelcted Areas in Communications"},{"key":"S0960129513000601_ref2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2004-12202"},{"key":"S0960129513000601_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48405-1_25"},{"key":"S0960129513000601_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00895-2"},{"key":"S0960129513000601_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/11555827_20"},{"key":"S0960129513000601_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_11"},{"key":"S0960129513000601_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.10.009"},{"key":"S0960129513000601_ref7","first-page":"340","article-title":"A semiring-based trace semantics for processes with applications to information leakage analysis.","volume":"323","author":"Boreale","year":"2010","journal-title":"IFIP AICT"},{"key":"S0960129513000601_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.12.007"},{"key":"S0960129513000601_ref11","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2008-0333"},{"key":"S0960129513000601_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00290-7"},{"key":"S0960129513000601_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.05.030"},{"key":"S0960129513000601_ref14","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2007-15302"},{"key":"S0960129513000601_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003299"},{"key":"S0960129513000601_ref17","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1994\/1995-3103"},{"key":"S0960129513000601_ref18","first-page":"11","volume-title":"Proceedings of Symposium on Security and Privacy","author":"Goguen","year":"1982"},{"key":"S0960129513000601_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"S0960129513000601_ref23","first-page":"3","volume-title":"Proceedings of CSF","author":"K\u00f6pf","year":"2010"},{"key":"S0960129513000601_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69959-7"},{"key":"S0960129513000601_ref31","first-page":"255","volume-title":"Proceedings of CSFW","author":"Sabelfeld","year":"2005"},{"key":"S0960129513000601_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_32"},{"key":"S0960129513000601_ref1","first-page":"1","article-title":"Two formal approaches for approximating noninterference properties.","volume":"2946","author":"Aldini","year":"2002","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"S0960129513000601_ref19","first-page":"261","volume-title":"Proceedings of ACSAC","author":"Heusser","year":"2010"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000601","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T18:58:58Z","timestamp":1555873138000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000601\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["S0960129513000601"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000601","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}