{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:54Z","timestamp":1740122694149,"version":"3.37.3"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,1,15]],"date-time":"2018-01-15T00:00:00Z","timestamp":1515974400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,1,15]],"date-time":"2018-01-15T00:00:00Z","timestamp":1515974400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-C-0166"],"award-info":[{"award-number":["FA8750-12-C-0166"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10703-017-0313-8","type":"journal-article","created":{"date-parts":[[2018,1,15]],"date-time":"2018-01-15T10:51:12Z","timestamp":1516013472000},"page":"166-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Securing a compiler transformation"],"prefix":"10.1007","volume":"53","author":[{"given":"Chaoqiang","family":"Deng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,1,15]]},"reference":[{"key":"313_CR1","doi-asserted-by":"publisher","unstructured":"Abadi M (1998) Protection in programming-language translations. In: Larsen KG, Skyum S, Winskel G (eds) Automata, languages and programming, 25th international colloquium, ICALP\u201998, Aalborg, Denmark, July 13\u201317, 1998, Proceedings. Lecture notes in computer science, vol 1443. Springer, pp 868\u2013883. \n                    https:\/\/doi.org\/10.1007\/BFb0055109","DOI":"10.1007\/BFb0055109"},{"key":"313_CR2","unstructured":"Almeida JB, Barbosa M, Barthe G, Dupressoir F, Emmi M (2016) Verifying constant-time implementations. In: Holz T, Savage S (eds) 25th USENIX security symposium, USENIX security 16, Austin, TX, USA, August 10\u201312, 2016. USENIX Association, pp 53\u201370. \n                    https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida"},{"key":"313_CR3","unstructured":"Bell D, LaPadula L (1973) Secure computer systems: mathematical foundations, vol 1-III. Technical Report of ESD-TR-73-278, The MITRE Corporation"},{"key":"313_CR4","doi-asserted-by":"publisher","unstructured":"Ceara D, Mounier L, Potet M (2010) Taint dependency sequences: a characterization of insecure execution paths based on input-sensitive cause sequences. In: Third international conference on software testing, verification and validation, ICST 2010, Paris, France, April 7\u20139, 2010. Workshops Proceedings, pp 371\u2013380. \n                    https:\/\/doi.org\/10.1109\/ICSTW.2010.28","DOI":"10.1109\/ICSTW.2010.28"},{"key":"313_CR5","doi-asserted-by":"publisher","unstructured":"de Amorim AA, Collins N, DeHon A, Demange D, Hritcu C, Pichardie D, Pierce BC, Pollack R, Tolmach A (2014) A verified information-flow architecture. In: Jagannathan S, Sewell P (eds) The 41st annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL \u201914, San Diego, CA, USA, January 20\u201321, 2014. ACM, pp 165\u2013178. \n                    https:\/\/doi.org\/10.1145\/2535838.2535839","DOI":"10.1145\/2535838.2535839"},{"key":"313_CR6","doi-asserted-by":"publisher","unstructured":"Deng C, Namjoshi KS (2016) Securing a compiler transformation. In: Rival X (Ed) Static analysis: 23rd international symposium, SAS 2016, Edinburgh, UK, September 8\u201310, 2016, Proceedings. Lecture notes in computer science, vol 9837. Springer, pp 170\u2013188. \n                    https:\/\/doi.org\/10.1007\/978-3-662-53413-7_9","DOI":"10.1007\/978-3-662-53413-7_9"},{"key":"313_CR7","doi-asserted-by":"publisher","unstructured":"Deng C, Namjoshi KS (2017) Securing the SSA transform. In: Ranzato F (Ed) Static analysis: 24th international symposium, SAS 2017, New York, NY, USA, August 30\u2013September 1, 2017, Proceedings. Lecture notes in computer science, vol 10422. Springer, pp 88\u2013105. \n                    https:\/\/doi.org\/10.1007\/978-3-319-66706-5_5","DOI":"10.1007\/978-3-319-66706-5_5"},{"key":"313_CR8","unstructured":"Denning DE (May 1975) Secure information flow in computer systems. Ph.D. Thesis, Purdue University"},{"issue":"7","key":"313_CR9","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning DE, Denning PJ (1977) Certification of programs for secure information flow. Commun ACM 20(7):504\u2013513. \n                    https:\/\/doi.org\/10.1145\/359636.359712","journal-title":"Commun ACM"},{"key":"313_CR10","doi-asserted-by":"publisher","unstructured":"D\u2019Silva V, Payer M, Song DX (2015) The correctness-security gap in compiler optimization. In: 2015 IEEE symposium on security and privacy workshops, SPW 2015, San Jose, CA, USA, May 21\u201322, 2015. IEEE Computer Society, pp 73\u201387. \n                    https:\/\/doi.org\/10.1109\/SPW.2015.33","DOI":"10.1109\/SPW.2015.33"},{"key":"313_CR11","doi-asserted-by":"publisher","unstructured":"Fournet C, Swamy N, Chen J, Dagand P, Strub P, Livshits B (2013) Fully abstract compilation to JavaScript. In: Giacobazzi R, Cousot R (eds) The 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL \u201913, Rome, Italy, January 23\u201325, 2013. ACM, pp 371\u2013384. \n                    https:\/\/doi.org\/10.1145\/2429069.2429114","DOI":"10.1145\/2429069.2429114"},{"key":"313_CR12","doi-asserted-by":"publisher","unstructured":"Gondi K, Bisht P, Venkatachari P, Sistla AP, Venkatakrishnan VN (2012) SWIPE: eager erasure of sensitive data in large scale systems software. In: Bertino E, Sandhu RS (eds) Second ACM conference on data and application security and privacy, CODASPY 2012, San Antonio, TX, USA, February 7\u20139, 2012. ACM, pp 295\u2013306. \n                    https:\/\/doi.org\/10.1145\/2133601.2133638","DOI":"10.1145\/2133601.2133638"},{"key":"313_CR13","unstructured":"Howard M (2002) When scrubbing secrets in memory doesn\u2019t work. \n                    http:\/\/archive.cert.uni-stuttgart.de\/bugtraq\/2002\/11\/msg00046.html\n                    \n                  . Also \n                    https:\/\/cwe.mitre.org\/data\/definitions\/14.html"},{"key":"313_CR14","doi-asserted-by":"publisher","unstructured":"Namjoshi KS, Zuck LD (2013) Witnessing program transformations. In: Logozzo F, F\u00e4hndrich M (eds) Static analysis: 20th international symposium, SAS 2013, Seattle, WA, USA, June 20\u201322, 2013. Proceedings. Lecture notes in computer science, vol 7935. Springer, pp 304\u2013323. \n                    https:\/\/doi.org\/10.1007\/978-3-642-38856-9_17","DOI":"10.1007\/978-3-642-38856-9_17"},{"key":"313_CR15","doi-asserted-by":"crossref","unstructured":"Necula G (2000) Translation validation of an optimizing compiler. In: Proceedings of the ACM SIGPLAN conference on principles of programming languages design and implementation (PLDI). pp 83\u201395","DOI":"10.1145\/349299.349314"},{"key":"313_CR16","volume-title":"Computational complexity","author":"CH Papadimitriou","year":"1994","unstructured":"Papadimitriou CH (1994) Computational complexity. Addison-Wesley, Reading, MA"},{"issue":"2","key":"313_CR17","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2699503","volume":"37","author":"M Patrignani","year":"2015","unstructured":"Patrignani M, Agten P, Strackx R, Jacobs B, Clarke D, Piessens F (2015) Secure compilation to protected module architectures. ACM Trans Program Lang Syst 37(2):6. \n                    https:\/\/doi.org\/10.1145\/2699503","journal-title":"ACM Trans Program Lang Syst"},{"issue":"2","key":"313_CR18","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/s100090050027","volume":"2","author":"A Pnueli","year":"1998","unstructured":"Pnueli A, Shtrichman O, Siegel M (1998) The code validation tool (CVT)\u2014automatic verification of a compilation process. Softw Tools Technol Transf 2(2):192\u2013201","journal-title":"Softw Tools Technol Transf"},{"key":"313_CR19","doi-asserted-by":"publisher","unstructured":"Smith G (2015) Recent developments in quantitative information flow (invited tutorial). In: 30th Annual ACM\/IEEE symposium on logic in computer science, LICS 2015, Kyoto, Japan, July 6\u201310, 2015. IEEE, pp 23\u201331. \n                    https:\/\/doi.org\/10.1109\/LICS.2015.13","DOI":"10.1109\/LICS.2015.13"},{"issue":"2\/3","key":"313_CR20","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"DM Volpano","year":"1996","unstructured":"Volpano DM, Irvine CE, Smith G (1996) A sound type system for secure flow analysis. J Comput Secur 4(2\/3):167\u2013188. \n                    https:\/\/doi.org\/10.3233\/JCS-1996-42-304","journal-title":"J Comput Secur"},{"key":"313_CR21","unstructured":"Yang Z, Johannesmeyer B, Olesen AT, Lerner S, Levchenko K (2017) Dead store elimination (still) considered harmful. In: Kirda E, Ristenpart T (eds) 26th USENIX security symposium, USENIX security 2017, Vancouver, BC, Canada, August 16\u201318, 2017. USENIX Association, pp 1025\u20131040. \n                    https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/yang"},{"issue":"3","key":"313_CR22","first-page":"223","volume":"9","author":"LD Zuck","year":"2003","unstructured":"Zuck LD, Pnueli A, Goldberg B (2003) VOC: A methodology for the translation validation of optimizing compilers. J. UCS 9(3):223\u2013247","journal-title":"J. UCS"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0313-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0313-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0313-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:45:42Z","timestamp":1589730342000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0313-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,15]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["313"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0313-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2018,1,15]]},"assertion":[{"value":"15 January 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}