{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:59:57Z","timestamp":1755838797698,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171834"},{"type":"electronic","value":"9783030171841"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17184-1_18","type":"book-chapter","created":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T21:34:04Z","timestamp":1554586444000},"page":"499-524","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Compiling Sandboxes: Formally Verified Software Fault Isolation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-0652","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0189-0223","authenticated-orcid":false,"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Dang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9681-644X","authenticated-orcid":false,"given":"Pierre","family":"Wilke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,6]]},"reference":[{"key":"18_CR1","unstructured":"Supplementary material. https:\/\/www.irisa.fr\/celtique\/ext\/compcertsfi"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/10930755_22","volume-title":"Theorem Proving in Higher Order Logics","author":"J Andronick","year":"2003","unstructured":"Andronick, J., Chetali, B., Ly, O.: Using Coq to verify Java CardTM applet isolation properties. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 335\u2013351. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/10930755_22"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Ansel, J., et al.: Language-independent sandboxing of just-in-time compilation and self-modifying code. In: PLDI, pp. 355\u2013366 (2011)","DOI":"10.1145\/1993316.1993540"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-12736-1_24","volume-title":"Programming Languages and Systems","author":"F Besson","year":"2014","unstructured":"Besson, F., Blazy, S., Wilke, P.: A precise and abstract memory model for C using symbolic values. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 449\u2013468. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12736-1_24"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-319-66107-0_6","volume-title":"Interactive Theorem Proving","author":"F Besson","year":"2017","unstructured":"Besson, F., Blazy, S., Wilke, P.: CompCertS: a memory-aware verified C compiler using pointer as integer semantics. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 81\u201397. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_6"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Besson, F., Blazy, S., Wilke, P.: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data. J. Autom. Reasoning (2018, accepted for publication)","DOI":"10.1007\/s10817-017-9439-z"},{"issue":"2","key":"18_CR7","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1017\/S0956796804005465","volume":"15","author":"F Besson","year":"2005","unstructured":"Besson, F., de Grenier de Latour, T., Jensen, T.P.: Interfaces for stack inspection. J. Funct. Program. 15(2), 179\u2013217 (2005)","journal-title":"J. Funct. Program."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: POPL. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243\u2013258. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_18"},{"issue":"6","key":"18_CR10","doi-asserted-by":"publisher","first-page":"793","DOI":"10.3233\/JCS-160558","volume":"24","author":"R Guanciale","year":"2016","unstructured":"Guanciale, R., Nemati, H., Dam, M., Baumann, C.: Provably secure memory isolation for Linux on ARM. J. Comput. Secur. 24(6), 793\u2013837 (2016)","journal-title":"J. Comput. Secur."},{"key":"18_CR11","unstructured":"Guthaus, M., Ringenberg, J., Ernst, D., Austin, T., Mudge, T., Brown, R.: MiBench: a free, commercially representative embedded benchmark suite, pp. 3\u201314. Institute of Electrical and Electronics Engineers Inc., United States (2001)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Hathhorn, C., Ellison, C., Ro\u015fu, G.: Defining the undefinedness of C. In: PLDI, pp. 336\u2013345. ACM, June 2015","DOI":"10.1145\/2813885.2737979"},{"key":"18_CR13","unstructured":"ISO: ISO C Standard 1999. Technical report (1999)"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Kang, J., Kim, Y., Hur, C., Dreyer, D., Vafeiadis, V.: Lightweight verification of separate compilation. In: POPL, pp. 178\u2013190. ACM (2016)","DOI":"10.1145\/2914770.2837642"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL. ACM (2014)","DOI":"10.1145\/2535838.2535878"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Kroll, J.A., Stewart, G., Appel, A.W.: Portable software fault isolation. In: CSF, pp. 18\u201332. IEEE (2014)","DOI":"10.1109\/CSF.2014.10"},{"issue":"8","key":"18_CR17","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1145\/1787234.1787253","volume":"53","author":"JR Larus","year":"2010","unstructured":"Larus, J.R., Hunt, G.C.: The singularity system. Commun. ACM 53(8), 72\u201379 (2010)","journal-title":"Commun. ACM"},{"issue":"7","key":"18_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"4","key":"18_CR19","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Program Logics for Certified Compilers. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781107256552"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-48749-2_7","volume-title":"Secure Internet Programming, Security Issues for Mobile and Distributed Objects","author":"X Leroy","year":"1999","unstructured":"Leroy, X., Rouaix, F.: Security properties of typed applets. In: Vitek, J., Jensen, C.D. (eds.) Secure Internet Programming, Security Issues for Mobile and Distributed Objects. LNCS, vol. 1603, pp. 147\u2013182. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48749-2_7"},{"key":"18_CR22","unstructured":"The Coq development team: The Coq proof assistant reference manual (2017). http:\/\/coq.inria.fr , version 8.7"},{"key":"18_CR23","unstructured":"McCamant, S., Morrisett, G.: Evaluating SFI for a CISC architecture. In: Proceedings of the 15th Conference on USENIX Security Symposium, USENIX-SS 2006, vol. 15. USENIX Association (2006)"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.B., Gan, E.: RockSalt: better, faster, stronger SFI for the x86. In: PLDI, pp. 395\u2013404. ACM (2012)","DOI":"10.1145\/2345156.2254111"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: OSDI, pp. 229\u2013243. ACM (1996)","DOI":"10.1145\/248155.238781"},{"key":"18_CR27","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998)"},{"key":"18_CR28","unstructured":"Put, L.V., Chanet, D., Bus, B.D., Sutter, B.D., Bosschere, K.D.: DIABLO: a reliable, retargetable and extensible link-time rewriting framework. In: In IEEE International Symposium On Signal Processing And Information Technology (2005)"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Richards, G., Hammer, C., Nardelli, F.Z., Jagannathan, S., Vitek, J.: Flexible access control for JavaScript. In: OOPSLA, pp. 305\u2013322. ACM (2013)","DOI":"10.1145\/2544173.2509542"},{"key":"18_CR30","unstructured":"Sehr, D., et al.: Adapting software fault isolation to contemporary CPU architectures. In: 19th USENIX Security Symposium, pp. 1\u201312. USENIX Association (2010)"},{"key":"18_CR31","unstructured":"Sehr, D., et al.: Adapting software fault isolation to contemporary CPU architectures. In: Proceedings of the 19th USENIX Conference on Security, USENIX Security 2010, p. 1. USENIX Association (2010)"},{"issue":"3","key":"18_CR32","doi-asserted-by":"publisher","first-page":"50:1","DOI":"10.1145\/2988545","volume":"49","author":"R Shu","year":"2016","unstructured":"Shu, R., et al.: A study of security isolation techniques. ACM Comput. Surv. 49(3), 50:1\u201350:37 (2016)","journal-title":"ACM Comput. Surv."},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Simon, L., Chisnall, D., Anderson, R.J.: What you get is what you C: controlling side effects in mainstream C compilers. In: EuroS&P, pp. 1\u201315. IEEE (2018)","DOI":"10.1109\/EuroSP.2018.00009"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Sinha, R., et al.: A design and verification methodology for secure isolated regions. In: PLDI, pp. 665\u2013681. ACM (2016)","DOI":"10.1145\/2980983.2908113"},{"key":"18_CR35","doi-asserted-by":"crossref","unstructured":"Wahbe, R., Lucco, S., Anderson, T.E., Graham, S.L.: Efficient software-based fault isolation. In: SOSP, pp. 203\u2013216. ACM (1993)","DOI":"10.1145\/173668.168635"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Wang, X., Chen, H., Cheung, A., Jia, Z., Zeldovich, N., Kaashoek, M.: Undefined behavior: what happened to my code? In: APSYS (2012)","DOI":"10.1145\/2349896.2349905"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"Yee, B., et al.: Native client: a sandbox for portable, untrusted x86 native code. In: S&P, pp. 79\u201393. IEEE (2009)","DOI":"10.1109\/SP.2009.25"},{"issue":"1","key":"18_CR38","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/1629175.1629203","volume":"53","author":"B Yee","year":"2010","unstructured":"Yee, B., et al.: Native client: a sandbox for portable, untrusted x86 native code. Commun. ACM 53(1), 91\u201399 (2010)","journal-title":"Commun. ACM"},{"key":"18_CR39","doi-asserted-by":"crossref","unstructured":"Zhao, L., Li, G., Sutter, B.D., Regehr, J.: ARMor: fully verified software fault isolation. In: EMSOFT, pp. 289\u2013298. ACM (2011)","DOI":"10.1145\/2038642.2038687"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17184-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,15]],"date-time":"2022-09-15T11:33:10Z","timestamp":1663241590000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17184-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171834","9783030171841"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17184-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"6 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/esop","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"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"86","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - 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"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}