{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:01:44Z","timestamp":1742961704097,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319708478"},{"type":"electronic","value":"9783319708485"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-70848-5_13","type":"book-chapter","created":{"date-parts":[[2017,11,10]],"date-time":"2017-11-10T15:43:26Z","timestamp":1510328606000},"page":"197-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Sound Transpilation from Binary to\u00a0Machine-Independent Code"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Metere","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Lindner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,11]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-87873-5_18","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., Starostin, A.: The verisoft approach to systems verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 209\u2013224. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87873-5_18"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Balliu, M., Dam, M., Guanciale, R.: Automating information flow analysis of low level code. In: SIGSAC Conference on Computer and Communications Security, pp. 1080\u20131091. ACM (2014)","DOI":"10.1145\/2660267.2660322"},{"key":"13_CR3","unstructured":"Beringer, L., Petcher, A., Katherine, Q.Y., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: USENIX Security Symposium, pp. 207\u2013221 (2015)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bletsch, T., Jiang, X., Freeh, V.W., Liang, Z.: Jump-oriented programming: a new class of code-reuse attack. In: Symposium on Information, Computer and Communications Security, pp. 30\u201340. ACM (2011)","DOI":"10.1145\/1966913.1966919"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-25379-9_15","volume-title":"Certified Programs and Proofs","author":"S B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3\u2019s bit-vector proofs in HOL4 and Isabelle\/HOL. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 183\u2013198. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_15"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Boldo, S., Jourdan, J., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: Symposium on Computer Arithmetic, pp. 107\u2013115. IEEE (2013)","DOI":"10.1109\/ARITH.2013.30"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-22110-1_37","volume-title":"Computer Aided Verification","author":"D Brumley","year":"2011","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: a binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 463\u2013469. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_37"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Nemati, H.: Machine code verification of a tiny ARM hypervisor. In: Workshop on Trustworthy Embedded Devices, Co-located with CCS, pp. 3\u201312. ACM (2013)","DOI":"10.1145\/2517300.2517302"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-32347-8_23","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2012","unstructured":"Fox, A.: Directions in ISA specification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 338\u2013344. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_23"},{"key":"13_CR10","unstructured":"Fox, A.: L3: a specification language for instruction set architectures. http:\/\/www.cl.cam.ac.uk\/~acjf3\/l3\/ . Accessed 2015"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-1-4419-1539-9_8","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"AC Fox","year":"2010","unstructured":"Fox, A.C., Gordon, M.J., Myreen, M.O.: Specification and verification of ARM hardware and software. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 221\u2013247. Springer, Boston (2010). https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_8"},{"issue":"2","key":"13_CR12","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1145\/2954680.2872380","volume":"50","author":"N Hasabnis","year":"2016","unstructured":"Hasabnis, N., Sekar, R.: Lifting assembly to intermediate representation: a novel approach leveraging compilers. ACM SIGOPS Oper. Syst. Rev. 50(2), 311\u2013324 (2016)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: Operating systems principles, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"13_CR14","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/2578855.2535841","volume":"49","author":"R Kumar","year":"2014","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. SIGPLAN Not. 49, 179\u2013191 (2014). ACM","journal-title":"SIGPLAN Not."},{"issue":"7","key":"13_CR15","doi-asserted-by":"crossref","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"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-71316-6_15","volume-title":"Programming Languages and Systems","author":"G Li","year":"2007","unstructured":"Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 205\u2013219. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_15"},{"key":"13_CR17","unstructured":"Arm Limited: ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) (2013). http:\/\/infocenter.arm.com\/help\/index.jsp?topic=\/com.arm.doc.ddi0487a.h\/index.html"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-03545-1_5","volume-title":"Certified Programs and Proofs","author":"MO Myreen","year":"2013","unstructured":"Myreen, M.O., Curello, G.: Proof pearl: a verified bignum implementation in x86-64 machine code. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 66\u201381. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_5"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Formal Methods in Computer-Aided Design, pp. 1\u20138. IEEE Press (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"issue":"2","key":"13_CR21","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1016\/S1571-0661(04)81042-9","volume":"89","author":"N Nethercote","year":"2003","unstructured":"Nethercote, N., Seward, J.: Valgrind: a program supervision framework. Electron. Notes Theor. Comput. Sci. 89(2), 44\u201366 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 471\u2013482. ACM (2013)","DOI":"10.1145\/2491956.2462183"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Shacham, H.: The geometry of innocent flesh on the bone: return-into-libc without function calls (on the x86). In: Conference on Computer and Communications Security, pp. 552\u2013561. ACM (2007)","DOI":"10.1145\/1315245.1315313"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Shoshitaishvili, Y., Wang, R., Salls, C., Stephens, N., Polino, M., Dutcher, A., Grosen, J., Feng, S., Hauser, C., Kr\u00fcgel, C., Vigna, G.: SOK: (state of) the art of war: offensive techniques in binary analysis. In: Symposium on Security and Privacy, pp. 138\u2013157. IEEE (2016)","DOI":"10.1109\/SP.2016.17"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-89862-7_1","volume-title":"Information Systems Security","author":"D Song","year":"2008","unstructured":"Song, D., et al.: BitBlaze: a new approach to computer security via binary analysis. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 1\u201325. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89862-7_1"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Vogels, F., Jacobs, B., Piessens, F.: A machine-checked soundness proof for an efficient verification condition generator. In: Symposium on Applied Computing, pp. 2517\u20132522. ACM (2010)","DOI":"10.1145\/1774088.1774610"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70848-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T01:23:43Z","timestamp":1659835423000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70848-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319708478","9783319708485"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70848-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}