{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T20:50:29Z","timestamp":1759092629398,"version":"3.38.0"},"reference-count":56,"publisher":"SAGE Publications","issue":"2","license":[{"start":{"date-parts":[[2021,2,17]],"date-time":"2021-02-17T00:00:00Z","timestamp":1613520000000},"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":[[2021,3,29]]},"abstract":"<jats:p> We introduce a novel type system for enforcing secure information flow in an imperative language. Our work is motivated by the problem of statically checking potential information leakage in Android applications. To this end, we design a lightweight type system featuring Android permission model, where the permissions are statically assigned to applications and are used to enforce access control in the applications. We take inspiration from a type system by Banerjee and Naumann to allow security types to be dependent on the permissions of the applications. A\u00a0novel feature of our type system is a typing rule for conditional branching induced by permission testing, which introduces a merging operator on security types, allowing more precise security policies to be enforced. The soundness of our type system is proved with respect to non-interference. A\u00a0type inference algorithm is also presented for the underlying security type system, by reducing the inference problem to a constraint solving problem in the lattice of security types. In addition, a new way to represent our security types as reduced ordered binary decision diagrams is proposed. <\/jats:p>","DOI":"10.3233\/jcs-200036","type":"journal-article","created":{"date-parts":[[2021,2,19]],"date-time":"2021-02-19T17:25:55Z","timestamp":1613755555000},"page":"161-228","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":1,"title":["A permission-dependent type system for secure information flow analysis"],"prefix":"10.1177","volume":"29","author":[{"given":"Zhiwu","family":"Xu","sequence":"first","affiliation":[{"name":"College of Computer Science and Software Engineering, Shenzhen University, China. E-mail:\u00a0"}]},{"given":"Hongxu","family":"Chen","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore. E-mails:\u00a0,\u00a0"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"The Australian National University, Australia. E-mails:\u00a0,\u00a0"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore. E-mails:\u00a0,\u00a0"}]},{"given":"Kunal","family":"Sareen","sequence":"additional","affiliation":[{"name":"The Australian National University, Australia. E-mails:\u00a0,\u00a0"}]}],"member":"179","published-online":{"date-parts":[[2021,2,17]]},"reference":[{"key":"ref001","unstructured":"Android, Requesting permissions at run time. https:\/\/developer.android.com\/training\/permissions\/requesting.html."},{"key":"ref002","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594299"},{"key":"ref003","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005453"},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, D.\u00a0Pichardie and T.\u00a0Rezk, A certified lightweight non-interference Java bytecode verifier, in: Proceedings of the 16th European Symposium on Programming, ESOP\u201907, Berlin, Heidelberg, 2007, pp.\u00a0125\u2013140.","DOI":"10.1007\/978-3-540-71316-6_10"},{"key":"ref005","doi-asserted-by":"publisher","DOI":"10.1145\/1040294.1040304"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, T.\u00a0Rezk and D.A.\u00a0Naumann, Deriving an information flow checker and certifying compiler for Java, in: IEEE Symposium on Security and Privacy, 2006, pp.\u00a0230\u2013242.","DOI":"10.1109\/SP.2006.13"},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref008","doi-asserted-by":"crossref","unstructured":"A.\u00a0Chaudhuri, Language-based security on Android, in: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS \u201909, New York, NY, USA, 2009, pp.\u00a01\u20137.","DOI":"10.1145\/1554339.1554341"},{"key":"ref009","doi-asserted-by":"crossref","unstructured":"H.\u00a0Chen, A.\u00a0Tiu, Z.\u00a0Xu and Y.\u00a0Liu, A permission-dependent type system for secure information flow analysis, in: 31st IEEE Computer Security Foundations Symposium, CSF, IEEE Computer Society, Oxford, United Kingdom, 2018, pp.\u00a0218\u2013232.","DOI":"10.1109\/CSF.2018.00023"},{"key":"ref010","doi-asserted-by":"crossref","unstructured":"E.\u00a0Chin, A.P.\u00a0Felt, K.\u00a0Greenwood and D.\u00a0Wagner, Analyzing inter-application communication in Android, in: Proceedings of the 9th International Conference on Mobile Systems, Applications, and Services, MobiSys \u201911, New York, NY, USA, 2011, pp.\u00a0239\u2013252.","DOI":"10.1145\/1999995.2000018"},{"key":"ref011","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref012","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"ref013","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"ref014","unstructured":"A.\u00a0Developers, Binder, 2017, online, accessed on 07-July-2017."},{"key":"ref015","unstructured":"A.\u00a0Developers, PermissionChecker | Android Developers, 2017, online, accessed on 07-July-2017."},{"key":"ref016","unstructured":"W.\u00a0Enck, P.\u00a0Gilbert, B.\u00a0Chun, L.P.\u00a0Cox, J.\u00a0Jung, P.D.\u00a0McDaniel and A.\u00a0Sheth, TaintDroid: An information-flow tracking system for realtime privacy monitoring on smartphones, in: 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2010), 2010, pp.\u00a0393\u2013407."},{"key":"ref017","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2009.26"},{"key":"ref018","doi-asserted-by":"crossref","unstructured":"M.D.\u00a0Ernst, R.\u00a0Just, S.\u00a0Millstein, W.\u00a0Dietl, S.\u00a0Pernsteiner, F.\u00a0Roesner, K.\u00a0Koscher, P.B.\u00a0Barros, R.\u00a0Bhoraskar, S.\u00a0Han, P.\u00a0Vines and E.X.\u00a0Wu, Collaborative verification of information flow for a high-assurance app store, in: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201914, ACM, New York, NY, USA, 2014, pp.\u00a01092\u20131104. ISBN 978-1-4503-2957-6.","DOI":"10.1145\/2660267.2660343"},{"key":"ref019","unstructured":"A.P.\u00a0Fuchs, A.\u00a0Chaudhuri and J.\u00a0Foster, SCanDroid: Automated security certification of android applications, Technical Report, CS-TR-4991, University of Maryland, 2009."},{"key":"ref020","doi-asserted-by":"crossref","unstructured":"J.A.\u00a0Goguen and J.\u00a0Meseguer, Security policies and security models, in: SOSP, 1982, pp.\u00a011\u201320.","DOI":"10.1109\/SP.1982.10014"},{"key":"ref021","doi-asserted-by":"crossref","unstructured":"M.I.\u00a0Gordon, D.\u00a0Kim, J.\u00a0Perkins, L.\u00a0Gilham, N.\u00a0Nguyen and M.\u00a0Rinard, Information-flow analysis of Android applications in DroidSafe, in: 22nd Annual Network and Distributed System Security Symposium (NDSS 2015), 2015.","DOI":"10.14722\/ndss.2015.23089"},{"key":"ref022","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2015.36"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111045"},{"key":"ref024","unstructured":"D.E.\u00a0Knuth, The Art of Computer Programming, Vol. 4. Fascicle 1, 1st edn, Addison Wesley Longman Publishing Co., Inc., United States, 2009."},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"J.\u00a0Landauer and T.\u00a0Redmond, A lattice of information, in: 6th IEEE Computer Security Foundations Workshop \u2013 CSFW\u201993, Franconia, New Hampshire, USA, June 15\u201317, 1993, Proceedings, IEEE Computer Society, 1993, pp.\u00a065\u201370.","DOI":"10.1109\/CSFW.1993.246638"},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"L.\u00a0Li, A.\u00a0Bartel, T.F.\u00a0Bissyand\u00e9, J.\u00a0Klein, Y.\u00a0Le Traon, S.\u00a0Arzt, S.\u00a0Rasthofer, E.\u00a0Bodden, D.\u00a0Octeau and P.\u00a0McDaniel, IccTA: Detecting inter-component privacy leaks in Android apps, in: Proceedings of the 37th International Conference on Software Engineering \u2013 Volume 1, ICSE \u201915, IEEE Press, Piscataway, NJ, USA, 2015, pp.\u00a0280\u2013291. ISBN 978-1-4799-1934-5.","DOI":"10.1109\/ICSE.2015.48"},{"key":"ref027","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.17"},{"key":"ref028","doi-asserted-by":"crossref","unstructured":"P.\u00a0Li and D.\u00a0Zhang, A derivation framework for dependent security label inference, in: Proc. ACM Program. Lang. 2(OOPSLA), 2018, pp.\u00a0115:1\u2013115:26.","DOI":"10.1145\/3276485"},{"key":"ref029","doi-asserted-by":"crossref","unstructured":"X.\u00a0Li, F.\u00a0Nielson, H.R.\u00a0Nielson and X.\u00a0Feng, Disjunctive information flow for communicating processes, in: TGC, 2015.","DOI":"10.1007\/978-3-319-25527-9_6"},{"key":"ref030","doi-asserted-by":"crossref","unstructured":"X.\u00a0Li, F.\u00a0Nielson and H.\u00a0Riis Nielson, Future-dependent flow policies with prophetic variables, in: The 2016 ACM Workshop, ACM Press, New York, NY, USA, 2016, pp.\u00a029\u201342.","DOI":"10.1145\/2993600.2993603"},{"key":"ref031","doi-asserted-by":"crossref","unstructured":"S.\u00a0Lortz, H.\u00a0Mantel, A.\u00a0Starostin, T.\u00a0Bahr, D.\u00a0Schneider and A.\u00a0Weber, Cassandra: Towards a certifying app store for Android, in: Proceedings of the 4th ACM Workshop on Security and Privacy in Smartphones and Mobile Devices, SPSM \u201914, New York, NY, USA, 2014, pp.\u00a093\u2013104.","DOI":"10.1145\/2666620.2666631"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"L.\u00a0Louren\u00e7o and L.\u00a0Caires, Information flow analysis for valued-indexed data security compartments, in: Trustworthy Global Computing \u2013 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30\u201331, 2013, Revised Selected Papers, Lecture Notes in Computer Science, Vol.\u00a08358, Springer, 2014, pp.\u00a0180\u2013198.","DOI":"10.1007\/978-3-319-05119-2_11"},{"key":"ref033","doi-asserted-by":"crossref","unstructured":"L.\u00a0Louren\u00e7o and L.\u00a0Caires, Dependent information flow types, in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201915, New York, NY, USA, 2015, pp.\u00a0317\u2013328.","DOI":"10.1145\/2676726.2676994"},{"key":"ref034","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.22"},{"key":"ref035","doi-asserted-by":"crossref","unstructured":"T.\u00a0Murray, Short paper: On high-assurance information-flow-secure programming languages, in: Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, 2015.","DOI":"10.1145\/2786558.2786561"},{"key":"ref036","doi-asserted-by":"crossref","unstructured":"T.\u00a0Murray, R.\u00a0Sison, E.\u00a0Pierzchalski and C.\u00a0Rizkallah, Compositional verification and refinement of concurrent value-dependent noninterference, in: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), 2016, pp.\u00a0417\u2013431.","DOI":"10.1109\/CSF.2016.36"},{"key":"ref037","unstructured":"T.\u00a0Murray, R.\u00a0Sison, E.\u00a0Pierzchalski and C.\u00a0Rizkallah, A dependent security type system for concurrent imperative programs, Archive of Formal Proofs (2016), http:\/\/isa-afp.org\/entries\/Dependent_SIFUM_Type_Systems.shtml, Formal proof development."},{"key":"ref038","unstructured":"T.\u00a0Murray, R.\u00a0Sison, E.\u00a0Pierzchalski and C.\u00a0Rizkallah, Compositional security-preserving refinement for concurrent imperative programs, Archive of Formal Proofs (2016), http:\/\/isa-afp.org\/entries\/Dependent_SIFUM_Refinement.shtml, Formal proof development."},{"key":"ref039","unstructured":"A.\u00a0Nadkarni, B.\u00a0Andow, W.\u00a0Enck and S.\u00a0Jha, Practical DIFC enforcement on Android, in: USENIX Security Symposium, 2016."},{"key":"ref040","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.12"},{"key":"ref041","unstructured":"G.C.\u00a0Necula and P.\u00a0Lee, Proof-carrying code, Technical Report, School of Computer Science, Carnegie Mellon University, 1996, CMU-CS-96-165."},{"key":"ref042","unstructured":"B.C.\u00a0Pierce, Types and Programming Languages, MIT Press, 2002. ISBN 978-0-262-16209-8."},{"key":"ref043","unstructured":"N.\u00a0Polikarpova, J.\u00a0Yang, S.\u00a0Itzhaky, T.\u00a0Hance and A.\u00a0Solar-Lezama, Enforcing information flow policies with type-targeted program synthesis, 2018, arXiv preprint arXiv:1607.03445v2."},{"key":"ref044","unstructured":"N.\u00a0Polikarpova, J.\u00a0Yang, S.\u00a0Itzhaky and A.\u00a0Solar-Lezama, Type-driven repair for information flow security, CoRR abs\/1607.03445 (2016). http:\/\/arxiv.org\/abs\/1607.03445."},{"key":"ref045","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"ref046","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref047","doi-asserted-by":"crossref","unstructured":"M.\u00a0Sun, T.\u00a0Wei and J.C.S.\u00a0Lui, TaintART: A practical multi-level information-flow tracking system for Android RunTime, in: Proceedings of the 23rd ACM Conference on Computer and Communications Security, CCS\u201916, 2016.","DOI":"10.1145\/2976749.2978343"},{"key":"ref048","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_9"},{"key":"ref049","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_28"},{"key":"ref050","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000142"},{"key":"ref051","doi-asserted-by":"publisher","DOI":"10.1145\/1290520.1290526"},{"key":"ref052","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"ref053","doi-asserted-by":"crossref","unstructured":"F.\u00a0Wei, S.\u00a0Roy, X.\u00a0Ou and A.\u00a0Robby, A precise and general inter-component data flow analysis framework for security vetting of Android apps, in: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201914, ACM, New York, NY, USA, 2014, pp.\u00a01329\u20131341. ISBN 978-1-4503-2957-6.","DOI":"10.1145\/2660267.2660357"},{"key":"ref054","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103669"},{"key":"ref055","doi-asserted-by":"crossref","unstructured":"D.\u00a0Zhang, Y.\u00a0Wang, G.E.\u00a0Suh and A.C.\u00a0Myers, A hardware design language for timing-sensitive information-flow security, in: The Twentieth International Conference, ACM Press, New York, New York, USA, 2015, pp.\u00a0503\u2013516.","DOI":"10.1145\/2694344.2694372"},{"key":"ref056","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0019-9"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-200036","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-200036","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-200036","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,10]],"date-time":"2025-03-10T12:43:01Z","timestamp":1741610581000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-200036"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,17]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,3,29]]}},"alternative-id":["10.3233\/JCS-200036"],"URL":"https:\/\/doi.org\/10.3233\/jcs-200036","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"type":"print","value":"0926-227X"},{"type":"electronic","value":"1875-8924"}],"subject":[],"published":{"date-parts":[[2021,2,17]]}}}