{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:43:06Z","timestamp":1774946586320,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T00:00:00Z","timestamp":1389139200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,1,8]]},"DOI":"10.1145\/2535838.2535839","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T08:40:06Z","timestamp":1389688806000},"page":"165-178","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["A verified information-flow architecture"],"prefix":"10.1145","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":"Portland State University, 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":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"University of Pennsylvania and INRIA, Philadelphia, PA, USA"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"Harvard University and INRIA, Cambridge, MA, USA"}]},{"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, Cambridge, MA, USA"}]},{"given":"Andrew","family":"Tolmach","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, OR, USA"}]}],"member":"320","published-online":{"date-parts":[[2014,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_22"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.22"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554353"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005453"},{"key":"e_1_3_2_2_5_1","volume-title":"A certified lightweight noninterference Java bytecode verifier. ESOP","author":"Barthe G.","year":"2007","unstructured":"G. Barthe , D. Pichardie , and T. Rezk . A certified lightweight noninterference Java bytecode verifier. ESOP . 2007 . G. Barthe, D. Pichardie, and T. Rezk. A certified lightweight noninterference Java bytecode verifier. ESOP. 2007."},{"key":"e_1_3_2_2_6_1","volume-title":"End-to-end multilevel hybrid information flow control. APLAS","author":"Beringer L.","year":"2012","unstructured":"L. Beringer . End-to-end multilevel hybrid information flow control. APLAS . 2012 . L. Beringer. End-to-end multilevel hybrid information flow control. APLAS. 2012."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1394608.1382153"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500592"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273463.1273490"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273440.1250722"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516702"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2039239.2039245"},{"key":"e_1_3_2_2_15_1","volume-title":"High-performance parallel accelerator for flexible and efficient run-time monitoring. DSN","author":"Deng D. Y.","year":"2012","unstructured":"D. Y. Deng and G. E. Suh . High-performance parallel accelerator for flexible and efficient run-time monitoring. DSN . 2012 . D. Y. Deng and G. E. Suh. High-performance parallel accelerator for flexible and efficient run-time monitoring. DSN. 2012."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2435264.2435298"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SASOW.2012.11"},{"key":"e_1_3_2_2_18_1","volume-title":"Unwinding and inference control","author":"Goguen J. A.","year":"1984","unstructured":"J. A. Goguen and J. Meseguer . Unwinding and inference control . IEEE S &P. 1984 . J. A. Goguen and J. Meseguer. Unwinding and inference control. IEEE S&P. 1984."},{"key":"e_1_3_2_2_19_1","volume-title":"A perspective on information-flow control. Marktoberdorf Summer School","author":"Hedin D.","year":"2011","unstructured":"D. Hedin and A. Sabelfeld . A perspective on information-flow control. Marktoberdorf Summer School . IOS Press , 2011 . D. Hedin and A. Sabelfeld. A perspective on information-flow control. Marktoberdorf Summer School. IOS Press, 2011."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.19"},{"key":"e_1_3_2_2_21_1","volume-title":"All your IFCException are belong to us","author":"Hri\u0163cu C.","year":"2013","unstructured":"C. Hri\u0163cu , M. Greenberg , B. Karel , B. C. Pierce , and G. Morrisett . All your IFCException are belong to us . IEEE S &P. 2013 . C. Hri\u0163cu, M. Greenberg, B. Karel, B. C. Pierce, and G. Morrisett. All your IFCException are belong to us. IEEE S&P. 2013."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500574"},{"key":"e_1_3_2_2_23_1","volume-title":"On the derivation of secure components","author":"Jacob J.","year":"1989","unstructured":"J. Jacob . On the derivation of secure components . IEEE S &P. 1989 . J. Jacob. On the derivation of secure components. IEEE S&P. 1989."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_3_2_2_25_1","volume-title":"DTA++: Dynamic taint analysis with targeted control-flow propagation. NDSS","author":"Kang M. G.","year":"2011","unstructured":"M. G. Kang , S. McCamant , P. Poosankam , and D. Song . DTA++: Dynamic taint analysis with targeted control-flow propagation. NDSS . 2011 . M. G. Kang, S. McCamant, P. Poosankam, and D. Song. DTA++: Dynamic taint analysis with targeted control-flow propagation. NDSS. 2011."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_18"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.23"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516713"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2004.17"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560586_29"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.8"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"e_1_3_2_2_37_1","volume-title":"Hoare logic for realistically modelled machine code. TACAS","author":"Myreen M. O.","year":"2007","unstructured":"M. O. Myreen and M. J. C. Gordon . Hoare logic for realistically modelled machine code. TACAS . 2007 . M. O. Myreen and M. J. C. Gordon. Hoare logic for realistically modelled machine code. TACAS. 2007."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.20"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_30"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926393"},{"key":"e_1_3_2_2_43_1","volume-title":"Trust-management, intrusion-tolerance, accountability, and reconstitution architecture (TIARA)","author":"Shrobe H.","year":"2009","unstructured":"H. Shrobe , A. DeHon , and T. F. Knight , Jr . Trust-management, intrusion-tolerance, accountability, and reconstitution architecture (TIARA) , 2009 . H. Shrobe, A. DeHon, and T. F. Knight, Jr. Trust-management, intrusion-tolerance, accountability, and reconstitution architecture (TIARA), 2009."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034688"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024404"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2004.31"},{"key":"e_1_3_2_2_47_1","volume-title":"HPCA","author":"Doudalis I.","year":"2008","unstructured":"Venkataramani, I. Doudalis , Y. Solihin , and M. Prvulovic . FlexiTaint: A programmable accelerator for dynamic taint propagation . HPCA , 2008 . Venkataramani, I. Doudalis, Y. Solihin, and M. Prvulovic. FlexiTaint: A programmable accelerator for dynamic taint propagation. HPCA, 2008."}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535839","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2535838.2535839","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:39:24Z","timestamp":1750221564000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535839"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,8]]},"references-count":46,"alternative-id":["10.1145\/2535838.2535839","10.1145\/2535838"],"URL":"https:\/\/doi.org\/10.1145\/2535838.2535839","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2578855.2535839","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,1,8]]},"assertion":[{"value":"2014-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}