{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:01:41Z","timestamp":1777806101705,"version":"3.51.4"},"reference-count":28,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2019,12,6]],"date-time":"2019-12-06T00:00:00Z","timestamp":1575590400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2020,2,4]]},"abstract":"<jats:p>Information Flow Control (IFC) is a form of dependence analysis that tracks and prohibits dependence of public outputs on secret inputs. Such a dependence analysis is often carried out using a type system. IFC type systems can track dependence (via confidentiality labels) at varying levels of granularity. On one extreme, there are fine-grained type systems that track dependence at the level of individual values. They label individual values. On the other extreme, there are coarse-grained type systems that track dependence at the level of entire computations. These type systems do not label individual values but instead label entire sub-computations.<\/jats:p>\n                  <jats:p>An important foundational question is one of the relative expressiveness of these two classes of IFC type systems. In this paper we show that, despite the glaring differences in how they track dependence, the two classes of type systems are actually equally expressive. We do this by showing translations from FG, a fine-grained IFC type system derived from SLAM (In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (1998)), to [Formula: see text], a coarse-grained IFC type system derived from HLIO (In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP) (2015)), and vice-versa. The translation from [Formula: see text] to FG is straightforward since FG tracks dependence at a granularity finer than [Formula: see text] does. However, the translation from FG to [Formula: see text] is quite involved and relies extensively on label quantification. We further examine the reason for this complexity using a slight variant of [Formula: see text], called CG, to which FG can be translated more easily.<\/jats:p>\n                  <jats:p>As a separate, more foundational contribution we show how to extend logical relation models of information flow to languages with higher-order state. Specifically, we build world-indexed (Kripke) logical relations for FG, [Formula: see text] and CG, which we use to prove these type systems sound and also to prove the translations between them correct.<\/jats:p>","DOI":"10.3233\/jcs-191382","type":"journal-article","created":{"date-parts":[[2019,12,6]],"date-time":"2019-12-06T11:22:10Z","timestamp":1575631330000},"page":"129-156","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":5,"title":["On the expressiveness and semantics of information flow types"],"prefix":"10.1177","volume":"28","author":[{"given":"Vineet","family":"Rajani","sequence":"first","affiliation":[{"name":"Max Planck Institute for Software Systems, Germany. E-mails:\u00a0,\u00a0"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Germany. E-mails:\u00a0,\u00a0"}]}],"member":"179","published-online":{"date-parts":[[2019,12,6]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"M.\u00a0Abadi, A.\u00a0Banerjee, N.\u00a0Heintze and J.G.\u00a0Riecke, A core calculus of dependency, in: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 1999.","DOI":"10.1145\/292540.292555"},{"key":"ref002","doi-asserted-by":"crossref","unstructured":"A.\u00a0Ahmed, D.\u00a0Dreyer and A.\u00a0Rossberg, State-dependent representation independence, in: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2009.","DOI":"10.1145\/1480881.1480925"},{"key":"ref003","doi-asserted-by":"crossref","unstructured":"A.J.\u00a0Ahmed, Step-indexed syntactic logical relations for recursive and quantified types, in: Proceedings of the European Symposium on Programming Languages and Systems (ESOP), 2006.","DOI":"10.1007\/11693024_6"},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"M.\u00a0Algehed and A.\u00a0Russo, Encoding DCC in Haskell, in: Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), 2017.","DOI":"10.1145\/3139337.3139338"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"T.H.\u00a0Austin and C.\u00a0Flanagan, Efficient purely-dynamic information flow analysis, in: Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), 2009.","DOI":"10.1145\/1554339.1554353"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"T.H.\u00a0Austin and C.\u00a0Flanagan, Permissive dynamic information flow analysis, in: Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), 2010.","DOI":"10.1145\/1814217.1814220"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, T.\u00a0Rezk and A.\u00a0Basu, Security types preserving compilation, Computer Languages, Systems & Structures (CLSS) 33(2) (2007).","DOI":"10.1016\/j.cl.2005.05.002"},{"key":"ref008","doi-asserted-by":"crossref","unstructured":"G.\u00a0Boudol, Secure information flow as a safety property, in: International Workshop on Formal Aspects in Security and Trust (FAST), 2008.","DOI":"10.1007\/978-3-642-01465-9_2"},{"key":"ref009","doi-asserted-by":"crossref","unstructured":"N.\u00a0Broberg, B.\u00a0Delft and D.\u00a0Sands, Paragon for practical programming with information-flow control, in: Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), 2013.","DOI":"10.1007\/978-3-319-03542-0_16"},{"key":"ref010","doi-asserted-by":"crossref","unstructured":"P.\u00a0Buiras, D.\u00a0Vytiniotis and A.\u00a0Russo, HLIO: Mixing static and dynamic typing for information-flow control in Haskell, in: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP), 2015.","DOI":"10.1145\/2784731.2784758"},{"key":"ref011","doi-asserted-by":"crossref","unstructured":"E.\u00a0\u00c7i\u00e7ek, Z.\u00a0Paraskevopoulou and D.\u00a0Garg, A type theory for incremental computational complexity with control flow changes, in: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP), 2016.","DOI":"10.1145\/2951913.2951950"},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"P.\u00a0Efstathopoulos, M.\u00a0Krohn, S.\u00a0VanDeBogart, C.\u00a0Frey, D.\u00a0Ziegler, E.\u00a0Kohler, D.\u00a0Mazi\u00e8res, F.\u00a0Kaashoek and R.\u00a0Morris, Labels and event processes in the asbestos operating system, in: Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2005.","DOI":"10.1145\/1095810.1095813"},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"C.\u00a0Fournet and T.\u00a0Rezk, Cryptographically sound implementations for typed information-flow security, in: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2008.","DOI":"10.1145\/1328438.1328478"},{"key":"ref014","doi-asserted-by":"crossref","unstructured":"J.A.\u00a0Goguen and J.\u00a0Meseguer, Security policies and security models, in: Proceedings of the IEEE Symposium on Security and Privacy, 1982.","DOI":"10.1109\/SP.1982.10014"},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"N.\u00a0Heintze and J.G.\u00a0Riecke, The SLam calculus: Programming with secrecy and integrity, in: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 1998.","DOI":"10.1145\/268946.268976"},{"key":"ref016","doi-asserted-by":"crossref","unstructured":"S.\u00a0Hunt and D.\u00a0Sands, On flow-sensitive security types, in: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2006.","DOI":"10.1145\/1111037.1111045"},{"key":"ref017","doi-asserted-by":"crossref","unstructured":"M.\u00a0Krohn, A.\u00a0Yip, M.\u00a0Brodsky, N.\u00a0Cliffer, M.F.\u00a0Kaashoek, E.\u00a0Kohler and R.\u00a0Morris, Information flow control for standard OS abstractions, in: Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2007.","DOI":"10.1145\/1294261.1294293"},{"key":"ref018","doi-asserted-by":"crossref","unstructured":"H.\u00a0Mantel, D.\u00a0Sands and H.\u00a0Sudbrock, Assumptions and guarantees for compositional noninterference, in: Proceedings of the IEEE Computer Security Foundations Symposium (CSF), 2011.","DOI":"10.1109\/CSF.2011.22"},{"key":"ref019","doi-asserted-by":"crossref","unstructured":"A.A.\u00a0Matos and G.\u00a0Boudol, On declassification and the non-disclosure policy, Journal of Computer Security (JCS) 17(5) (2009).","DOI":"10.3233\/JCS-2009-0355"},{"key":"ref020","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363526"},{"key":"ref021","doi-asserted-by":"crossref","unstructured":"A.\u00a0Nanevski, G.\u00a0Morrisett and L.\u00a0Birkedal, Polymorphism and separation in hoare type theory, in: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP), 2006.","DOI":"10.1145\/1159803.1159812"},{"key":"ref022","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"ref023","doi-asserted-by":"crossref","unstructured":"V.\u00a0Rajani, I.\u00a0Bastys, W.\u00a0Rafnsson and D.\u00a0Garg, Type systems for information flow control: The question of granularity, SIGLOG News 4(1) (2017).","DOI":"10.1145\/3051528.3051531"},{"key":"ref024","doi-asserted-by":"crossref","unstructured":"V.\u00a0Rajani and D.\u00a0Garg, Types for information flow control: Labeling granularity and semantic models, in: Proc. of the 31st IEEE Computer Security Foundations Symposium (CSF), 2018.","DOI":"10.1109\/CSF.2018.00024"},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"A.\u00a0Sabelfeld and D.\u00a0Sands, A PER model of secure information flow in sequential programs, in: Proceedings of the European Symposium on Programming Languages and Systems (ESOP), 1999.","DOI":"10.1007\/3-540-49099-X_4"},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"D.\u00a0Stefan, A.\u00a0Russo, J.C.\u00a0Mitchell and D.\u00a0Mazi\u00e8res, Flexible dynamic information flow control in Haskell, in: Proceedings of the ACM Symposium on Haskell (Haskell), 2011.","DOI":"10.1145\/2034675.2034688"},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"D.M.\u00a0Volpano, C.E.\u00a0Irvine and G.\u00a0Smith, A sound type system for secure flow analysis, Journal of Computer Security (JCS) 4(2\u20133) (1996).","DOI":"10.3233\/JCS-1996-42-304"},{"key":"ref028","unstructured":"N.\u00a0Zeldovich, S.\u00a0Boyd-Wickizer, E.\u00a0Kohler and D.\u00a0Mazi\u00e8res, Making information flow explicit in HiStar, in: Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2006."}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-191382","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-191382","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-191382","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:21Z","timestamp":1777495521000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-191382"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,6]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,2,4]]}},"alternative-id":["10.3233\/JCS-191382"],"URL":"https:\/\/doi.org\/10.3233\/jcs-191382","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,6]]}}}