{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T07:32:14Z","timestamp":1790667134264,"version":"4.1.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030393212","type":"print"},{"value":"9783030393229","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-39322-9_1","type":"book-chapter","created":{"date-parts":[[2020,1,14]],"date-time":"2020-01-14T19:03:59Z","timestamp":1579028639000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Witnessing Secure Compilation"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lucas M.","family":"Tabajara","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,1,13]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48749-2_2","volume-title":"Secure Internet Programming","author":"M Abadi","year":"1999","unstructured":"Abadi, M.: Protection in programming-language translations. In: Vitek, J., Jensen, C.D. (eds.) Secure Internet Programming. LNCS, vol. 1603, pp. 19\u201334. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48749-2_2"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: LICS 1988, pp. 165\u2013175 (1988). https:\/\/doi.org\/10.1109\/LICS.1988.5115","DOI":"10.1109\/LICS.1988.5115"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"de Amorim, A.A., et al.: A verified information-flow architecture. In: POPL 2014, pp. 165\u2013178 (2014). https:\/\/doi.org\/10.1145\/2535838.2535839","DOI":"10.1145\/2535838.2535839"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Laporte, V.: Secure compilation of side-channel countermeasures: the case of cryptographic \u201cconstant-time\u201d. In: CSF 2018, pp. 328\u2013343 (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00031","DOI":"10.1109\/CSF.2018.00031"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115\u2013131 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90098-9","journal-title":"Theor. Comput. Sci."},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: CSF 2008, pp. 51\u201365 (2008). https:\/\/doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-662-53413-7_9","volume-title":"Static Analysis","author":"C Deng","year":"2016","unstructured":"Deng, C., Namjoshi, K.S.: Securing a compiler transformation. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 170\u2013188. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_9"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Devriese, D., Patrignani, M., Piessens, F.: Fully-abstract compilation by approximate back-translation. In: POPL 2016, pp. 164\u2013177 (2016). https:\/\/doi.org\/10.1145\/2837614.2837618","DOI":"10.1145\/2837614.2837618"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"D\u2019Silva, V., Payer, M., Song, D.X.: The correctness-security gap in compiler optimization. In: SPW 2015, pp. 73\u201387 (2015). https:\/\/doi.org\/10.1109\/SPW.2015.33","DOI":"10.1109\/SPW.2015.33"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Fournet, C., Guernic, G.L., Rezk, T.: A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms. In: CCS 2009, pp. 432\u2013441 (2009). https:\/\/doi.org\/10.1145\/1653662.1653715","DOI":"10.1145\/1653662.1653715"},{"key":"1_CR12","unstructured":"Howard, M.: When scrubbing secrets in memory doesn\u2019t work (2002). http:\/\/archive.cert.uni-stuttgart.de\/bugtraq\/2002\/11\/msg00046.html. Also https:\/\/cwe.mitre.org\/data\/definitions\/14.html"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: PLDI 2014, pp. 216\u2013226 (2014). https:\/\/doi.org\/10.1145\/2594291.2594334","DOI":"10.1145\/2594291.2594334"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354 (2006). https:\/\/doi.org\/10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/3-540-51803-7_24","volume-title":"Temporal Logic in Specification","author":"Z Manna","year":"1989","unstructured":"Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by $${\\forall }$$-automata. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 124\u2013164. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51803-7_24"},{"key":"1_CR16","unstructured":"Marinov, D.: Credible compilation. Ph.D. thesis, Massachusetts Institute of Technology (2000)"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Murray, T.C., Sison, R., Engelhardt, K.: COVERN: a logic for compositional verification of information flow control. In: EuroS&P 2018, pp. 16\u201330 (2018). https:\/\/doi.org\/10.1109\/EuroSP.2018.00010","DOI":"10.1109\/EuroSP.2018.00010"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"KS Namjoshi","year":"1997","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 284\u2013296. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0058037"},{"key":"1_CR19","unstructured":"Namjoshi, K.S.: Witnessing an SSA transformation. In: VeriSure Workshop, CAV (2014). https:\/\/kedar-namjoshi.github.io\/papers\/Namjoshi-VeriSure-CAV-2014.pdf"},{"key":"1_CR20","unstructured":"Namjoshi, K.S., Tabajara, L.M.: Witnessing Secure Compilation (2019). https:\/\/arxiv.org\/abs\/1911.05866"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-38856-9_17","volume-title":"Static Analysis","author":"KS Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 304\u2013323. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_17"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Necula, G.: Translation validation of an optimizing compiler. In: (PLDI) 2000, pp. 83\u201395 (2000)","DOI":"10.1145\/349299.349314"},{"issue":"6","key":"1_CR23","doi-asserted-by":"publisher","first-page":"125:1","DOI":"10.1145\/3280984","volume":"51","author":"M Patrignani","year":"2019","unstructured":"Patrignani, M., Ahmed, A., Clarke, D.: Formal approaches to secure compilation: a survey of fully abstract compilation and related work. ACM Comput. Surv. 51(6), 125:1\u2013125:36 (2019). https:\/\/doi.org\/10.1145\/3280984","journal-title":"ACM Comput. Surv."},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Patrignani, M., Garg, D.: Secure compilation and hyperproperty preservation. In: CSF 2017, pp. 392\u2013404 (2017). https:\/\/doi.org\/10.1109\/CSF.2017.13","DOI":"10.1109\/CSF.2017.13"},{"issue":"2","key":"1_CR25","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.: The Code Validation Tool (CVT)- automatic verification of a compilation process. Softw. Tools Technol. Transf. 2(2), 192\u2013201 (1998)","journal-title":"Softw. Tools Technol. Transf."},{"key":"1_CR26","unstructured":"Rinard, M.: Credible compilation. Technical report. In: Proceedings of CC 2001: International Conference on Compiler Construction (1999)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_24"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI 2011, pp. 283\u2013294 (2011). https:\/\/doi.org\/10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"1_CR29","unstructured":"Yang, Z., Johannesmeyer, B., Olesen, A.T., Lerner, S., Levchenko, K.: Dead store elimination (still) considered harmful. In: USENIX Security 2017, pp. 1025\u20131040 (2017). https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/yang"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: PLDI 2013, pp. 175\u2013186 (2013). https:\/\/doi.org\/10.1145\/2491956.2462164","DOI":"10.1145\/2491956.2462164"},{"issue":"3","key":"1_CR31","first-page":"223","volume":"9","author":"LD Zuck","year":"2003","unstructured":"Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223\u2013247 (2003)","journal-title":"J. UCS"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-39322-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T18:43:27Z","timestamp":1710269007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-39322-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030393212","9783030393229"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-39322-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Orleans, LA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2020a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl20.sigplan.org\/home\/VMCAI-2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}