{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:55:57Z","timestamp":1773654957697,"version":"3.50.1"},"reference-count":91,"publisher":"SAGE Publications","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCS"],"published-print":{"date-parts":[[2016,12,1]]},"DOI":"10.3233\/jcs-15784","type":"journal-article","created":{"date-parts":[[2016,10,18]],"date-time":"2016-10-18T14:34:09Z","timestamp":1476801249000},"page":"689-734","source":"Crossref","is-referenced-by-count":9,"title":["A verified information-flow architecture"],"prefix":"10.1177","volume":"24","author":[{"given":"Arthur","family":"Azevedo de Amorim","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Nathan","family":"Collins","sequence":"additional","affiliation":[{"name":"Galois Inc, Portland, OR, USA"}]},{"given":"Andr\u00e9","family":"DeHon","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Delphine","family":"Demange","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Rennes 1\/IRISA, Rennes, France"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"INRIA, Paris, France"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"ENS Rennes\/IRISA, Rennes, France"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Randy","family":"Pollack","sequence":"additional","affiliation":[{"name":"Harvard University, Boston, MA, USA"}]},{"given":"Andrew","family":"Tolmach","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, OR, USA"}]}],"member":"179","reference":[{"key":"10.3233\/JCS-15784_ref1","doi-asserted-by":"crossref","unstructured":"A.\u00a0Askarov, S.\u00a0Hunt, A.\u00a0Sabelfeld and D.\u00a0Sands, Termination-insensitive noninterference leaks more than just a bit, in: 13th European Symposium on Research in Computer Security (ESORICS), Malaga, Spain, October 2008, LNCS, Vol.\u00a05283, Springer-Verlag, 2008.","DOI":"10.1007\/978-3-540-88313-5_22"},{"key":"10.3233\/JCS-15784_ref2","doi-asserted-by":"crossref","unstructured":"A.\u00a0Askarov and A.\u00a0Sabelfeld, Tight enforcement of information-release policies for dynamic languages, in: 22nd IEEE Computer Security Foundations Symposium (CSF), IEEE Computer Society, 2009, pp.\u00a043\u201359.","DOI":"10.1109\/CSF.2009.22"},{"key":"10.3233\/JCS-15784_ref3","doi-asserted-by":"crossref","unstructured":"A.\u00a0Askarov, D.\u00a0Zhang and A.C.\u00a0Myers, Predictive black-box mitigation of timing channels, in: 17th ACM Conference on Computer and Communications Security, ACM, 2010, pp.\u00a0297\u2013307.","DOI":"10.1145\/1866307.1866341"},{"key":"10.3233\/JCS-15784_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554353"},{"key":"10.3233\/JCS-15784_ref5","doi-asserted-by":"crossref","unstructured":"T.H.\u00a0Austin and C.\u00a0Flanagan, Permissive dynamic information flow analysis, in: Proceedings of the 5th Workshop on Programming Languages and Analysis for Security, PLAS, ACM, 2010, pp.\u00a03:1\u20133:12.","DOI":"10.1145\/1814217.1814220"},{"key":"10.3233\/JCS-15784_ref6","doi-asserted-by":"crossref","unstructured":"T.H.\u00a0Austin and C.\u00a0Flanagan, Multiple facets for dynamic information flow, in: Proceedings of the 39th Symposium on Principles of Programming Languages, POPL, 2012, pp.\u00a0165\u2013178.","DOI":"10.1145\/2103656.2103677"},{"key":"10.3233\/JCS-15784_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_4"},{"key":"10.3233\/JCS-15784_ref8","doi-asserted-by":"crossref","unstructured":"A.\u00a0Azevedo de Amorim, N.\u00a0Collins, A.\u00a0DeHon, D.\u00a0Demange, C.\u00a0Hri\u0163cu, D.\u00a0Pichardie, B.C.\u00a0Pierce, R.\u00a0Pollack and A.\u00a0Tolmach, A verified information-flow architecture, in: Proceedings of the 41st Symposium on Principles of Programming Languages, POPL, ACM, 2014, pp.\u00a0165\u2013178.","DOI":"10.1145\/2535838.2535839"},{"key":"10.3233\/JCS-15784_ref9","doi-asserted-by":"crossref","unstructured":"A.\u00a0Azevedo de Amorim, M.\u00a0D\u00e9n\u00e8s, N.\u00a0Giannarakis, C.\u00a0Hri\u0163cu, B.C.\u00a0Pierce, A.\u00a0Spector-Zabusky and A.\u00a0Tolmach, Micro-policies: Formally verified, tag-based security monitors, in: 36th IEEE Symposium on Security and Privacy (Oakland S&P), IEEE Computer Society, 2015, pp.\u00a0813\u2013830.","DOI":"10.1109\/SP.2015.55"},{"key":"10.3233\/JCS-15784_ref10","doi-asserted-by":"crossref","unstructured":"M.\u00a0Balliu, M.\u00a0Dam and R.\u00a0Guanciale, Automating information flow analysis of low level code, in: ACM SIGSAC Conference on Computer and Communications Security, CCS, G.\u00a0Ahn, M.\u00a0Yung and N.\u00a0Li, eds, ACM, 2014, pp.\u00a01080\u20131091.","DOI":"10.1145\/2660267.2660322"},{"issue":"2","key":"10.3233\/JCS-15784_ref11","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","article-title":"Stack-based access control and secure information flow","volume":"15","author":"Banerjee","year":"2005","journal-title":"Journal of Functional Programming"},{"key":"10.3233\/JCS-15784_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92188-2_1"},{"key":"10.3233\/JCS-15784_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_10"},{"key":"10.3233\/JCS-15784_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_5"},{"key":"10.3233\/JCS-15784_ref15","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bichhawat, V.\u00a0Rajani, D.\u00a0Garg and C.\u00a0Hammer, Generalizing permissive-upgrade in dynamic information flow analysis, in: 9th Workshop on Programming Languages and Analysis for Security (PLAS), ACM, 2014, p.\u00a015.","DOI":"10.1145\/2637113.2637116"},{"key":"10.3233\/JCS-15784_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05119-2_12"},{"key":"10.3233\/JCS-15784_ref18","doi-asserted-by":"crossref","unstructured":"S.\u00a0Chen, M.\u00a0Kozuch, T.\u00a0Strigkos, B.\u00a0Falsafi, P.B.\u00a0Gibbons, T.C.\u00a0Mowry, V.\u00a0Ramachandran, O.\u00a0Ruwase, M.P.\u00a0Ryan and E.\u00a0Vlachos, Flexible hardware acceleration for instruction-grain program monitoring, in: 35th International Symposium on Computer Architecture (ISCA), IEEE, 2008, pp.\u00a0377\u2013388.","DOI":"10.1145\/1394608.1382153"},{"key":"10.3233\/JCS-15784_ref19","unstructured":"S.\u00a0Chen, J.\u00a0Xu, N.\u00a0Nakka, Z.\u00a0Kalbarczyk and R.\u00a0Iyer, Defeating memory corruption attacks via pointer taintedness detection, in: International Conference on Dependable Systems and Networks (DSN), 2005, pp.\u00a0378\u2013387."},{"key":"10.3233\/JCS-15784_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"10.3233\/JCS-15784_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"issue":"6","key":"10.3233\/JCS-15784_ref22","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","article-title":"Hyperproperties","volume":"18","author":"Clarkson","year":"2010","journal-title":"Journal of Computer Security"},{"key":"10.3233\/JCS-15784_ref23","doi-asserted-by":"crossref","unstructured":"J.A.\u00a0Clause, W.\u00a0Li and A.\u00a0Orso, Dytan: A generic dynamic taint analysis framework, in: ACM\/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), ACM, 2007, pp.\u00a0196\u2013206.","DOI":"10.1145\/1273463.1273490"},{"key":"10.3233\/JCS-15784_ref24","doi-asserted-by":"crossref","unstructured":"D.\u00a0Cock, Q.\u00a0Ge, T.C.\u00a0Murray and G.\u00a0Heiser, The last mile: An empirical study of timing channels on seL4, in: ACM SIGSAC Conference on Computer and Communications Security, G.\u00a0Ahn, M.\u00a0Yung and N.\u00a0Li, eds, ACM, 2014, pp.\u00a0570\u2013581.","DOI":"10.1145\/2660267.2660294"},{"key":"10.3233\/JCS-15784_ref25","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2004.26"},{"key":"10.3233\/JCS-15784_ref26","doi-asserted-by":"crossref","unstructured":"M.\u00a0Dalton, H.\u00a0Kannan and C.\u00a0Kozyrakis, Raksha: A flexible information flow architecture for software security, in: International Symposium on Computer Architecture (ISCA), 2007, pp.\u00a0482\u2013493.","DOI":"10.1145\/1273440.1250722"},{"key":"10.3233\/JCS-15784_ref27","doi-asserted-by":"crossref","unstructured":"M.\u00a0Dam, R.\u00a0Guanciale, N.\u00a0Khakpour, H.\u00a0Nemati and O.\u00a0Schwarz, Formal verification of information flow security for a simple ARM-based separation kernel, in: ACM Conference on Computer and Communications Security, ACM, 2013, pp.\u00a0223\u2013234.","DOI":"10.1145\/2508859.2516702"},{"key":"10.3233\/JCS-15784_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2517300.2517302"},{"key":"10.3233\/JCS-15784_ref29","unstructured":"A.\u00a0DeHon, E.\u00a0Boling, R.\u00a0Nikhil, D.\u00a0Rad, J.\u00a0Schwarz, N.\u00a0Sharma, J.\u00a0Stoy, G.\u00a0Sullivan and A.\u00a0Sutherland, DOVER: A\u00a0Metadata-Extended RISC-V, in: RISC-V Workshop, 2016, Accompanying talk at http:\/\/youtu.be\/r5dIS1kDars."},{"key":"10.3233\/JCS-15784_ref30","doi-asserted-by":"crossref","unstructured":"A.\u00a0DeHon, B.\u00a0Karel, T.F.\u00a0Knight Jr., G.\u00a0Malecha, B.\u00a0Montagu, R.\u00a0Morisset, G.\u00a0Morrisett, B.C.\u00a0Pierce, R.\u00a0Pollack, S.\u00a0Ray, O.\u00a0Shivers, J.M.\u00a0Smith and G.\u00a0Sullivan, Preliminary design of the SAFE platform, in: 6th Workshop on Programming Languages and Operating Systems, PLOS, 2011.","DOI":"10.1145\/2039239.2039245"},{"key":"10.3233\/JCS-15784_ref31","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2010.17"},{"key":"10.3233\/JCS-15784_ref32","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2012.6263925"},{"key":"10.3233\/JCS-15784_ref33","doi-asserted-by":"crossref","unstructured":"U.\u00a0Dhawan and A.\u00a0DeHon, Area-efficient near-associative memories on FPGAs, in: International Symposium on Field-Programmable Gate Arrays (FPGA2013), 2013.","DOI":"10.1145\/2435264.2435298"},{"key":"10.3233\/JCS-15784_ref34","doi-asserted-by":"crossref","unstructured":"U.\u00a0Dhawan, C.\u00a0Hri\u0163cu, R.\u00a0Rubin, N.\u00a0Vasilakis, S.\u00a0Chiricescu, J.M.\u00a0Smith, T.F.\u00a0Knight Jr., B.C.\u00a0Pierce and A.\u00a0DeHon, Architectural support for software-defined metadata processing, in: International Conference on Architectural Support for Programming Languages and Operating Systems, 2015, pp.\u00a0487\u2013502.","DOI":"10.1145\/2694344.2694383"},{"key":"10.3233\/JCS-15784_ref35","doi-asserted-by":"crossref","unstructured":"U.\u00a0Dhawan, A.\u00a0Kwon, E.\u00a0Kadric, C.\u00a0Hri\u0163cu, B.C.\u00a0Pierce, J.M.\u00a0Smith, A.\u00a0DeHon, G.\u00a0Malecha, G.\u00a0Morrisett, T.F.\u00a0Knight Jr., A.\u00a0Sutherland, T.\u00a0Hawkins, A.\u00a0Zyxnfryx, D.\u00a0Wittenberg, P.\u00a0Trei, S.\u00a0Ray and G.\u00a0Sullivan, Hardware support for safety interlocks and introspection, in: SASO Workshop on Adaptive Host and Network Security, 2012.","DOI":"10.1109\/SASOW.2012.11"},{"key":"10.3233\/JCS-15784_ref36","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 Symposium on Operating Systems Principles, SOSP, ACM, 2005, pp.\u00a017\u201330.","DOI":"10.1145\/1095809.1095813"},{"key":"10.3233\/JCS-15784_ref37","doi-asserted-by":"crossref","unstructured":"J.A.\u00a0Goguen and J.\u00a0Meseguer, Unwinding and inference control, in: IEEE Symposium on Security and Privacy, IEEE Computer Society, 1984, pp.\u00a075\u201387.","DOI":"10.1109\/SP.1984.10019"},{"key":"10.3233\/JCS-15784_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"10.3233\/JCS-15784_ref40","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.10"},{"key":"10.3233\/JCS-15784_ref41","doi-asserted-by":"crossref","unstructured":"G.L.\u00a0Guernic, A.\u00a0Banerjee, T.P.\u00a0Jensen and D.A.\u00a0Schmidt, Automata-based confidentiality monitoring, in: 11th Asian Computing Science Conference, Springer, 2006, pp.\u00a075\u201389.","DOI":"10.1007\/978-3-540-77505-8_7"},{"issue":"6","key":"10.3233\/JCS-15784_ref42","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","article-title":"Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs","volume":"8","author":"Hammer","year":"2009","journal-title":"International Journal of Information Security"},{"key":"10.3233\/JCS-15784_ref43","unstructured":"D.\u00a0Hedin and A.\u00a0Sabelfeld, A Perspective on Information-Flow Control, Marktoberdorf Summer School, IOS Press, 2011."},{"key":"10.3233\/JCS-15784_ref44","doi-asserted-by":"crossref","unstructured":"D.\u00a0Hedin and A.\u00a0Sabelfeld, Information-flow security for a core of JavaScript, in: 25th IEEE Computer Security Foundations Symposium (CSF), CSF, IEEE, 2012, pp.\u00a03\u201318.","DOI":"10.1109\/CSF.2012.19"},{"key":"10.3233\/JCS-15784_ref45","doi-asserted-by":"crossref","unstructured":"C.\u00a0Hri\u0163cu, M.\u00a0Greenberg, B.\u00a0Karel, B.C.\u00a0Pierce and G.\u00a0Morrisett, All your IFCException are belong to us, in: 34th IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2013, pp.\u00a03\u201317.","DOI":"10.1109\/SP.2013.10"},{"key":"10.3233\/JCS-15784_ref46","doi-asserted-by":"crossref","unstructured":"C.\u00a0Hri\u0163cu, J.\u00a0Hughes, B.C.\u00a0Pierce, A.\u00a0Spector-Zabusky, D.\u00a0Vytiniotis, A.\u00a0Azevedo de Amorim and L.\u00a0Lampropoulos, Testing noninterference, quickly, in: 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2013.","DOI":"10.1145\/2500365.2500574"},{"key":"10.3233\/JCS-15784_ref48","doi-asserted-by":"crossref","unstructured":"J.\u00a0Jacob, On the derivation of secure components, in: IEEE Symposium on Security and Privacy, IEEE Computer Society, 1989, pp.\u00a0242\u2013247.","DOI":"10.1109\/SECPRI.1989.36298"},{"key":"10.3233\/JCS-15784_ref49","unstructured":"K.\u00a0Jee, G.\u00a0Portokalidis, V.P.\u00a0Kemerlis, S.\u00a0Ghosh, D.I.\u00a0August and A.D.\u00a0Keromytis, A general approach for efficiently accelerating software-based dynamic data flow tracking on commodity hardware, in: Network and Distributed System Security Symposium (NDSS), The Internet Society, 2012."},{"key":"10.3233\/JCS-15784_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"10.3233\/JCS-15784_ref51","doi-asserted-by":"crossref","unstructured":"A.C.\u00a0Myers, Jflow: Practical mostly-static information flow control, in: Proceedings of the 26th Symposium on Principles of Programming Languages (POPL), ACM, 1999, pp.\u00a0228\u2013241.","DOI":"10.1145\/292540.292561"},{"key":"10.3233\/JCS-15784_ref52","unstructured":"M.G.\u00a0Kang, S.\u00a0McCamant, P.\u00a0Poosankam and D.\u00a0Song, DTA++: Dynamic taint analysis with targeted control-flow propagation, in: Network and Distributed System Security Symposium (NDSS), The Internet Society, 2011."},{"key":"10.3233\/JCS-15784_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_18"},{"key":"10.3233\/JCS-15784_ref54","doi-asserted-by":"crossref","unstructured":"G.\u00a0Klein, K.\u00a0Elphinstone, G.\u00a0Heiser, J.\u00a0Andronick, D.\u00a0Cock, P.\u00a0Derrin, D.\u00a0Elkaduwe, K.\u00a0Engelhardt, R.\u00a0Kolanski, M.\u00a0Norrish, T.\u00a0Sewell, H.\u00a0Tuch and S.\u00a0Winwood, seL4: Formal verification of an OS kernel, in: Proceedings of the Symposium on Operating Systems Principles, ACM, 2009, pp.\u00a0207\u2013220.","DOI":"10.1145\/1629575.1629596"},{"key":"10.3233\/JCS-15784_ref55","doi-asserted-by":"crossref","unstructured":"M.N.\u00a0Krohn and E.\u00a0Tromer, Noninterference for a practical DIFC-based operating system, in: 30th IEEE Symposium on Security and Privacy, IEEE Computer Society, 2009, pp.\u00a061\u201376.","DOI":"10.1109\/SP.2009.23"},{"key":"10.3233\/JCS-15784_ref56","doi-asserted-by":"crossref","unstructured":"M.N.\u00a0Krohn, A.\u00a0Yip, M.Z.\u00a0Brodsky, N.\u00a0Cliffer, M.F.\u00a0Kaashoek, E.\u00a0Kohler and R.\u00a0Morris, Information flow control for standard OS abstractions, in: Proceedings of the Symposium on Operating Systems Principles, SOSP, ACM, 2007, pp.\u00a0321\u2013334.","DOI":"10.1145\/1323293.1294293"},{"key":"10.3233\/JCS-15784_ref57","doi-asserted-by":"crossref","unstructured":"A.\u00a0Kwon, U.\u00a0Dhawan, J.M.\u00a0Smith, T.F.\u00a0Knight Jr. and A.\u00a0DeHon, Low-fat pointers: Compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security, in: ACM SIGSAC Conference on Computer and Communications Security (CCS), ACM, 2013, pp.\u00a0721\u2013732.","DOI":"10.1145\/2508859.2516713"},{"issue":"4","key":"10.3233\/JCS-15784_ref58","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","article-title":"A formally verified compiler back-end","volume":"43","author":"Leroy","year":"2009","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"10.3233\/JCS-15784_ref59","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","article-title":"Formal verification of a C-like memory model and its uses for verifying program transformations","volume":"41","author":"Leroy","year":"2008","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/JCS-15784_ref60","doi-asserted-by":"crossref","unstructured":"C.\u00a0Mann and A.\u00a0Starostin, A framework for static detection of privacy leaks in Android applications, in: ACM Symposium on Applied Computing (SAC), ACM, 2012, pp.\u00a01457\u20131462.","DOI":"10.1145\/2245276.2232009"},{"key":"10.3233\/JCS-15784_ref61","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2004.17"},{"key":"10.3233\/JCS-15784_ref62","doi-asserted-by":"crossref","unstructured":"R.\u00a0Medel, A.B.\u00a0Compagnoni and E.\u00a0Bonelli, A typed assembly language for non-interference, in: 9th Italian Conference on Theoretical Computer Science (ICTCS), Lecture Notes in Computer Science, Vol.\u00a03701, Springer, 2005, pp.\u00a0360\u2013374.","DOI":"10.1007\/11560586_29"},{"key":"10.3233\/JCS-15784_ref63","doi-asserted-by":"crossref","unstructured":"B.\u00a0Montagu, B.C.\u00a0Pierce and R.\u00a0Pollack, A theory of information-flow labels, in: 26th IEEE Computer Security Foundations Symposium (CSF), IEEE, 2013, pp.\u00a03\u201317.","DOI":"10.1109\/CSF.2013.8"},{"key":"10.3233\/JCS-15784_ref64","doi-asserted-by":"crossref","unstructured":"S.\u00a0Moore and S.\u00a0Chong, Static analysis for efficient hybrid information-flow control, in: Proceedings of the 24th Computer Security Foundations Symposium, CSF, IEEE Computer Society, 2011, pp.\u00a0146\u2013160.","DOI":"10.1109\/CSF.2011.17"},{"key":"10.3233\/JCS-15784_ref65","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"10.3233\/JCS-15784_ref66","doi-asserted-by":"crossref","unstructured":"T.C.\u00a0Murray, D.\u00a0Matichuk, M.\u00a0Brassil, P.\u00a0Gammie, T.\u00a0Bourke, S.\u00a0Seefried, C.\u00a0Lewis, X.\u00a0Gao and G.\u00a0Klein, seL4: From general purpose to a proof of information flow enforcement, in: 34th IEEE Symposium on Security and Privacy, IEEE, 2013, pp.\u00a0415\u2013429.","DOI":"10.1109\/SP.2013.35"},{"key":"10.3233\/JCS-15784_ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"10.3233\/JCS-15784_ref69","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/363516.363526","article-title":"Protecting privacy using the decentralized label model","volume":"9","author":"Myers","year":"2000","journal-title":"Transactions on Software Engineering And Methodology (TOSEM)"},{"key":"10.3233\/JCS-15784_ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"10.3233\/JCS-15784_ref71","doi-asserted-by":"crossref","unstructured":"Z.\u00a0Ni and Z.\u00a0Shao, Certified assembly programming with embedded code pointers, in: Symposium on Principles of Programming Languages (POPL), ACM, 2006, pp.\u00a0320\u2013333.","DOI":"10.1145\/1111320.1111066"},{"key":"10.3233\/JCS-15784_ref72","doi-asserted-by":"crossref","unstructured":"M.\u00a0Pistoia, A.\u00a0Banerjee and D.A.\u00a0Naumann, Beyond stack inspection: A unified access-control and information-flow security model, in: Proceedings of the Symposium on Security and Privacy, SP, IEEE Computer Society, 2007, pp.\u00a0149\u2013163.","DOI":"10.1109\/SP.2007.10"},{"issue":"1","key":"10.3233\/JCS-15784_ref73","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","article-title":"Information flow inference for ML","volume":"25","author":"Pottier","year":"2003","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.3233\/JCS-15784_ref74","doi-asserted-by":"crossref","unstructured":"F.\u00a0Qin, C.\u00a0Wang, Z.\u00a0Li, H.\u00a0Kim, Y.\u00a0Zhou and Y.\u00a0Wu, LIFT: A low-overhead practical information flow tracking system for detecting security attacks, in: 39th IEEE\/ACM International Symposium on Microarchitecture (MICRO-39), 2006, pp.\u00a0135\u2013148.","DOI":"10.1109\/MICRO.2006.29"},{"key":"10.3233\/JCS-15784_ref75","doi-asserted-by":"crossref","unstructured":"A.\u00a0Russo and A.\u00a0Sabelfeld, Dynamic vs. static flow-sensitive security analysis, in: 23rd Computer Security Foundations Symposium (CSF), CSF, IEEE Computer Society, 2010, pp.\u00a0186\u2013199.","DOI":"10.1109\/CSF.2010.20"},{"key":"10.3233\/JCS-15784_ref76","doi-asserted-by":"crossref","unstructured":"O.\u00a0Ruwase, P.B.\u00a0Gibbons, T.C.\u00a0Mowry, V.\u00a0Ramachandran, S.\u00a0Chen, M.\u00a0Kozuch and M.P.\u00a0Ryan, Parallelizing dynamic information flow tracking, in: 20th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), ACM, 2008, pp.\u00a035\u201345.","DOI":"10.1145\/1378533.1378538"},{"issue":"1","key":"10.3233\/JCS-15784_ref77","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","article-title":"Language-based information-flow security","volume":"21","author":"Sabelfeld","year":"2003","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"10.3233\/JCS-15784_ref78","doi-asserted-by":"crossref","unstructured":"A.\u00a0Sabelfeld and A.\u00a0Russo, From dynamic to static and back: Riding the roller coaster of information-flow control research, in: Ershov Memorial Conference, Springer, 2009, pp.\u00a0352\u2013365.","DOI":"10.1007\/978-3-642-11486-1_30"},{"key":"10.3233\/JCS-15784_ref79","doi-asserted-by":"crossref","unstructured":"A.\u00a0Sabelfeld and D.\u00a0Sands, Dimensions and principles of declassification, in: Computer Security Foundations 18th Workshop, IEEE, 2005, pp.\u00a0255\u2013269.","DOI":"10.1109\/CSFW.2005.15"},{"issue":"1","key":"10.3233\/JCS-15784_ref80","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","article-title":"Enforceable security policies","volume":"3","author":"Schneider","year":"2000","journal-title":"ACM Transactions of Information Systems Security"},{"key":"10.3233\/JCS-15784_ref81","doi-asserted-by":"crossref","unstructured":"J.\u00a0Sevc\u00edk, V.\u00a0Vafeiadis, F.Z.\u00a0Nardelli, S.\u00a0Jagannathan and P.\u00a0Sewell, Relaxed-memory concurrency and verified compilation, in: Symposium on Principles of Programming Languages (POPL), ACM, 2011, pp.\u00a043\u201354.","DOI":"10.1145\/1925844.1926393"},{"key":"10.3233\/JCS-15784_ref82","doi-asserted-by":"crossref","unstructured":"Z.\u00a0Shao, Clean-slate development of certified OS kernels, in: Conference on Certified Programs and Proofs, X.\u00a0Leroy and A.\u00a0Tiu, eds, ACM, 2015, pp.\u00a095\u201396.","DOI":"10.1145\/2676724.2693180"},{"key":"10.3233\/JCS-15784_ref83","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554354"},{"key":"10.3233\/JCS-15784_ref85","doi-asserted-by":"crossref","unstructured":"D.\u00a0Stefan, P.\u00a0Buiras, E.Z.\u00a0Yang, A.\u00a0Levy, D.\u00a0Terei, A.\u00a0Russo and D.\u00a0Mazi\u00e8res, Eliminating cache-based timing attacks with instruction-based scheduling, in: 18th European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, Vol.\u00a08134, Springer, 2013, pp.\u00a0718\u2013735.","DOI":"10.1007\/978-3-642-40203-6_40"},{"key":"10.3233\/JCS-15784_ref86","doi-asserted-by":"crossref","unstructured":"D.\u00a0Stefan, A.\u00a0Russo, P.\u00a0Buiras, A.\u00a0Levy, J.C.\u00a0Mitchell and D.\u00a0Mazi\u00e8res, Addressing covert termination and timing channels in concurrent information flow systems, in: Proceedings of the International Conference on Functional Programming (ICFP), ACM, 2012.","DOI":"10.1145\/2364527.2364557"},{"key":"10.3233\/JCS-15784_ref87","doi-asserted-by":"crossref","unstructured":"D.\u00a0Stefan, A.\u00a0Russo, D.\u00a0Mazi\u00e8res and J.C.\u00a0Mitchell, Disjunction category labels, in: 16th Nordic Conference on Secure IT Systems, NordSec, Springer, 2011, pp.\u00a0223\u2013239.","DOI":"10.1007\/978-3-642-29615-4_16"},{"key":"10.3233\/JCS-15784_ref88","doi-asserted-by":"crossref","unstructured":"D.\u00a0Stefan, A.\u00a0Russo, J.C.\u00a0Mitchell and D.\u00a0Mazi\u00e8res, Flexible dynamic information flow control in Haskell, in: 4th Symposium on Haskell, ACM, 2011, pp.\u00a095\u2013106.","DOI":"10.1145\/2034675.2034688"},{"key":"10.3233\/JCS-15784_ref89","doi-asserted-by":"crossref","unstructured":"G.E.\u00a0Suh, J.W.\u00a0Lee, D.\u00a0Zhang and S.\u00a0Devadas, Secure program execution via dynamic information flow tracking, in: International Conference on Architectural Support for Programming Languages and Operating Systems, 2004, pp.\u00a085\u201396.","DOI":"10.1145\/1024393.1024404"},{"key":"10.3233\/JCS-15784_ref91","unstructured":"N.\u00a0Vachharajani, M.J.\u00a0Bridges, J.\u00a0Chang, R.\u00a0Rangan, G.\u00a0Ottoni, J.A.\u00a0Blome, G.A.\u00a0Reis, M.\u00a0Vachharajani and D.I.\u00a0August, RIFLE: An architectural framework for user-centric information-flow security, in: 37th International Symposium on Microarchitecture, 2004."},{"key":"10.3233\/JCS-15784_ref92","doi-asserted-by":"crossref","unstructured":"G.\u00a0Venkataramani, I.\u00a0Doudalis, Y.\u00a0Solihin and M.\u00a0Prvulovic, FlexiTaint: A programmable accelerator for dynamic taint propagation, in: 14th International Symposium on High Performance Computer Architecture (HPCA), 2008, pp.\u00a0173\u2013184.","DOI":"10.1109\/HPCA.2008.4658637"},{"issue":"3","key":"10.3233\/JCS-15784_ref93","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","article-title":"A sound type system for secure flow analysis","volume":"4","author":"Volpano","year":"1996","journal-title":"Journal of Computer Security"},{"key":"10.3233\/JCS-15784_ref94","doi-asserted-by":"crossref","unstructured":"D.\u00a0Yu and N.\u00a0Islam, A typed assembly language for confidentiality, in: 15th European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol.\u00a03924, Springer, 2006, pp.\u00a0162\u2013179.","DOI":"10.1007\/11693024_12"},{"key":"10.3233\/JCS-15784_ref95","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_7"},{"issue":"11","key":"10.3233\/JCS-15784_ref97","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/2018396.2018419","article-title":"Making information flow explicit in HiStar","volume":"54","author":"Zeldovich","year":"2011","journal-title":"Communications of the ACM"},{"key":"10.3233\/JCS-15784_ref98","doi-asserted-by":"crossref","unstructured":"D.\u00a0Zhang, A.\u00a0Askarov and A.C.\u00a0Myers, Predictive mitigation of timing channels in interactive systems, in: 18th ACM Conference on Computer and Communications Security, ACM, 2011, pp.\u00a0563\u2013574.","DOI":"10.1145\/2046707.2046772"}],"container-title":["Journal of Computer Security"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JCS-15784","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T16:34:04Z","timestamp":1749659644000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/JCS-15784"}},"subtitle":["Submission to special issue on Verified Information Flow Security"],"short-title":[],"issued":{"date-parts":[[2016,12,1]]},"references-count":91,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.3233\/jcs-15784","relation":{},"ISSN":["1875-8924","0926-227X"],"issn-type":[{"value":"1875-8924","type":"electronic"},{"value":"0926-227X","type":"print"}],"subject":[],"published":{"date-parts":[[2016,12,1]]}}}