{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:28Z","timestamp":1776305248863,"version":"3.50.1"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T00:00:00Z","timestamp":1586908800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T00:00:00Z","timestamp":1586908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100009148","name":"Queen Mary University of London","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100009148","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper describes our experience with symbolic model checking in an industrial setting. We have proved that the initial boot code running in data centers at Amazon Web Services is memory safe, an essential step in establishing the security of any data center. Standard static analysis tools cannot be easily used on boot code without modification owing to issues not commonly found in higher-level code, including memory-mapped device interfaces, byte-level memory access, and linker scripts. This paper describes automated solutions to these issues and their implementation in the C Bounded Model Checker (CBMC). CBMC is now the first source-level static analysis tool to extract the memory layout described in a linker script for use in its analysis.<\/jats:p>","DOI":"10.1007\/s10703-020-00344-2","type":"journal-article","created":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T13:03:42Z","timestamp":1586955822000},"page":"34-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Model checking boot code from AWS data centers"],"prefix":"10.1007","volume":"57","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kareem","family":"Khazem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark R.","family":"Tuttle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,15]]},"reference":[{"key":"344_CR1","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-70545-1_33","volume-title":"Computer aided verification","author":"PA Abdulla","year":"2008","unstructured":"Abdulla PA, Bouajjani A, Cederberg J, Haziza F, Rezine A (2008) Monotonic abstraction for programs with dynamic memory heaps. In: Gupta A, Malik S (eds) Computer aided verification. Springer, Berlin, pp 341\u2013354"},{"key":"344_CR2","unstructured":"AFL: American fuzzy lop. http:\/\/lcamtuf.coredump.cx\/afl. Accessed 6 Apr 2020"},{"key":"344_CR3","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer aided verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi A, Li Y, Gurfinkel A, Chechik M (2012) Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan P, Seshia SA (eds) Computer aided verification. Springer, Berlin, pp 672\u2013678"},{"key":"344_CR4","doi-asserted-by":"crossref","unstructured":"Arbaugh WA, Farber DJ, Smith JM (1997) A secure and reliable bootstrap architecture. In: 1997 IEEE symposium on security and privacy. IEEE Computer Society, pp 65\u201371","DOI":"10.1109\/SECPRI.1997.601317"},{"key":"344_CR5","unstructured":"Bazhaniuk O, Loucaides J, Rosenbaum L, Tuttle MR, Zimmer V (2015) Symbolic execution for BIOS security. In: 9th USENIX workshop on offensive technologies. USENIX Association, Washington, DC"},{"key":"344_CR6","unstructured":"Bellard F (2005) QEMU, a fast and portable dynamic translator. In: USENIX Annual Technical Conference, USENIX Association, Berkeley, CA, pp 41\u201346"},{"key":"344_CR7","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer aided verification","author":"J Berdine","year":"2007","unstructured":"Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW, Wies T, Yang H (2007) Shape analysis for composite data structures. In: Damm W, Hermanns H (eds) Computer aided verification. Springer, Berlin, pp 178\u2013192"},{"key":"344_CR8","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-31984-9_2","volume-title":"Fundamental approaches to software engineering","author":"D Beyer","year":"2005","unstructured":"Beyer D, Henzinger TA, Jhala R, Majumdar R (2005) Checking memory safety with blast. In: Cerioli M (ed) Fundamental approaches to software engineering. Springer, Berlin, pp 2\u201318"},{"key":"344_CR9","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer aided verification","author":"D Beyer","year":"2011","unstructured":"Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification. Springer, Berlin, pp 184\u2013190"},{"key":"344_CR10","unstructured":"Bovet DP (2013) Special sections in Linux binaries. https:\/\/lwn.net\/Articles\/531148\/. Accessed 6 Apr 2020"},{"key":"344_CR11","unstructured":"Burton RA (2017) rBoot: an open source boot loader for the ESP8266. https:\/\/github.com\/raburton\/rboot. Accessed 6 Apr 2020"},{"key":"344_CR12","unstructured":"Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Operating systems design and implementation. USENIX Association, Washington, DC, pp 209\u2013224"},{"key":"344_CR13","unstructured":"C bounded model checker github repository. https:\/\/github.com\/diffblue\/cbmc. Accessed 6 Apr 2020"},{"key":"344_CR14","unstructured":"Chamberlain S (1994) Using ld. https:\/\/sourceware.org\/binutils\/docs-2.27\/ld\/. Accessed 6 Apr 2020"},{"issue":"1","key":"344_CR15","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2110356.2110358","volume":"30","author":"V Chipounov","year":"2012","unstructured":"Chipounov V, Kuznetsov V, Candea G (2012) The S2E platform: design, implementation, and applications. ACM Trans Comput Syst 30(1):2:1\u20132:49","journal-title":"ACM Trans Comput Syst"},{"key":"344_CR16","doi-asserted-by":"crossref","unstructured":"Cho CY, D\u2019Silva V, Song D (2013) Blitz: compositional bounded model checking for real-world programs. In: 2013 28th IEEE\/ACM international conference on automated software engineering. IEEE, pp 136\u2013146","DOI":"10.1109\/ASE.2013.6693074"},{"key":"344_CR17","doi-asserted-by":"crossref","unstructured":"Christ J, Hoenicke J (2015) Weakly equivalent arrays. In: Lutz C, Ranise S (eds) Frontiers of combining systems. Springer, Berlin, pp 119\u2013134","DOI":"10.1007\/978-3-319-24246-0_8"},{"key":"344_CR18","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer aided verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti A, Griggio A (2012) Software model checking via IC3. In: Madhusudan P, Seshia SA (eds) Computer aided verification. Springer, Berlin, pp 277\u2013293"},{"key":"344_CR19","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"E Clarke","year":"2005","unstructured":"Clarke E, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs N, Zuck LD (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 570\u2013574"},{"key":"344_CR20","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"344_CR21","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem proving in higher order logics","author":"E Cohen","year":"2009","unstructured":"Cohen E, Dahlweid M, Hillebrand M, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S (2009) VCC: a practical system for verifying concurrent C. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Theorem proving in higher order logics. Springer, Berlin, pp 23\u201342"},{"key":"344_CR22","doi-asserted-by":"crossref","unstructured":"Condit J, Hackett B, Lahiri SK, Qadeer S (2009) Unifying type checking and property checking for low-level code. In: 36th annual ACM SIGPLANSIGACT symposium on principles of programming languages. ACM, New York, pp 302\u2013314","DOI":"10.1145\/1594834.1480921"},{"key":"344_CR23","first-page":"264","volume-title":"Taint analysis of security code in the KLEE symbolic execution engine","author":"R Corin","year":"2012","unstructured":"Corin R, Manzano FA (2012) Taint analysis of security code in the KLEE symbolic execution engine. Springer, Berlin, pp 264\u2013275"},{"key":"344_CR24","unstructured":"Synopsys static analysis (Coverity). http:\/\/coverity.com. Accessed 6 Apr 2020"},{"key":"344_CR25","unstructured":"Davidson D, Moench B, Ristenpart T, Jha S (2013) FIE on firmware: finding vulnerabilities in embedded systems using symbolic execution. In: USENIX security symposium. USENIX, Washington, DC, pp 463\u2013478"},{"key":"344_CR26","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-319-08867-9_32","volume-title":"Computer aided verification","author":"T Dillig","year":"2014","unstructured":"Dillig T, Dillig I, Chaudhuri S (2014) Optimal guard synthesis for memory safety. In: Biere A, Bloem R (eds) Computer aided verification. Springer, Berlin, pp 491\u2013507"},{"issue":"2","key":"344_CR27","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/1055218.1055226","volume":"39","author":"C Dodge","year":"2005","unstructured":"Dodge C, Irvine C, Nguyen T (2005) A study of initialization in Linux and OpenBSD. SIGOPS Oper Syst Rev 39(2):79\u201393","journal-title":"SIGOPS Oper Syst Rev"},{"key":"344_CR28","unstructured":"Engblom J (2016) Finding BIOS vulnerabilities with symbolic execution and virtual platforms. https:\/\/software.intel.com\/en-us\/blogs\/2017\/06\/06\/finding-bios-vulnerabilities-with-excite. Accessed 6 Apr 2020"},{"issue":"4","key":"344_CR29","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s10009-014-0307-4","volume":"16","author":"JF Ferreira","year":"2014","unstructured":"Ferreira JF, Gherghina C, He G, Qin S, Chin WN (2014) Automated verification of the FreeRTOS scheduler in hip\/sleek. Int J Softw Tools Technol Transf 16(4):381\u2013397","journal-title":"Int J Softw Tools Technol Transf"},{"key":"344_CR30","unstructured":"Fortify static code analyzer. https:\/\/software.microfocus.com\/en-us\/products\/static-code-analysis-sast\/overview. Accessed 6 Apr 2020"},{"key":"344_CR31","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-662-46681-0_42","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"A Haran","year":"2015","unstructured":"Haran A, Carter M, Emmi M, Lal A, Qadeer S, Rakamari\u0107 Z (2015) SMACK+Corral: a modular verifier. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 451\u2013454"},{"key":"344_CR32","unstructured":"Harrison J, HOL Light theorem prover. http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light. Accessed 6 Apr 2020"},{"key":"344_CR33","unstructured":"ISO\/IEC 9899:2011(E): Information technology\u2014Programming languages\u2014C. Standard, International Organization for Standardization, Geneva, CH (Dec 2011)"},{"issue":"3","key":"344_CR34","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F Ivan\u010di\u0107","year":"2008","unstructured":"Ivan\u010di\u0107 F, Yang Z, Ganai MK, Gupta A, Ashar P (2008) Efficient SAT-based bounded model checking for software verification. Theor Comput Sci 404(3):256\u2013274","journal-title":"Theor Comput Sci"},{"key":"344_CR35","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, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In: 22nd ACM SIGOPS symposium on operating system principles. ACM, New York, pp 207\u2013220","DOI":"10.1145\/1629575.1629596"},{"key":"344_CR36","unstructured":"Klocwork static code analyzer. https:\/\/www.klocwork.com\/. Accessed 6 Apr 2020"},{"key":"344_CR37","doi-asserted-by":"publisher","unstructured":"Kroening D, Strichman O (2016) Decision procedures\u2014an algorithmic point of view. Texts in theoretical computer science. An EATCS series, 2nd edn. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-662-50497-0","DOI":"10.1007\/978-3-662-50497-0"},{"key":"344_CR38","unstructured":"Kuznetsov V, Chipounov V, Candea G (2010) Testing closed-source binary device drivers with DDT. In: USENIX annual technical conference. USENIX Association, Berkeley, CA"},{"key":"344_CR39","doi-asserted-by":"crossref","unstructured":"Lal A, Qadeer S (2014) Powering the static driver verifier using Corral. In: 22nd ACM SIGSOFT international symposium on foundations of software engineering. ACM, New York, pp 202\u2013212","DOI":"10.1145\/2635868.2635894"},{"key":"344_CR40","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer aided verification","author":"A Lal","year":"2012","unstructured":"Lal A, Qadeer S, Lahiri SK (2012) A solver for reachability modulo theories. In: Madhusudan P, Seshia SA (eds) Computer aided verification. Springer, Berlin, pp 427\u2013443"},{"key":"344_CR41","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-1-4020-8157-6_28","volume-title":"Building the information society","author":"T Lev-Ami","year":"2004","unstructured":"Lev-Ami T, Manevich R, Sagiv M (2004) TVLA: a system for generating abstract interpreters. In: Jacquart R (ed) Building the information society. Springer, Boston, pp 367\u2013375"},{"key":"344_CR42","volume-title":"Linkers and loaders","author":"JR Levine","year":"1999","unstructured":"Levine JR (1999) Linkers and loaders. Morgan Kaufmann, Burlington"},{"key":"344_CR43","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer aided verification","author":"KL McMillan","year":"2006","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: Ball T, Jones RB (eds) Computer aided verification. Springer, Berlin, pp 123\u2013136"},{"key":"344_CR44","unstructured":"Moser JR (2006) Optimizing linker load times. https:\/\/lwn.net\/Articles\/192624\/. Accessed 6 Apr 2020"},{"key":"344_CR45","unstructured":"Moser JR (2006) Prelink and address space randomization. https:\/\/lwn.net\/Articles\/190139\/. Accessed 6 Apr 2020"},{"key":"344_CR46","unstructured":"Parvez R, Ward PAS, Ganesh V (2016) Combining static analysis and targeted symbolic execution for scalable bug-finding in application binaries. In: 26th annual international conference on computer science and software engineering. IBM Corp., Riverton, pp 116\u2013127"},{"key":"344_CR47","unstructured":"Pitre N (2017) Shrinking the kernel with link-time garbage collection. https:\/\/lwn.net\/Articles\/741494\/. Accessed 6 Apr 2020"},{"key":"344_CR48","unstructured":"Pitre N (2017) Shrinking the kernel with link-time optimization. https:\/\/lwn.net\/Articles\/744507\/. Accessed 6 Apr 2020"},{"key":"344_CR49","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer aided verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107 Z, Emmi M (2014) Smack: decoupling source language details from verifier implementations. In: Biere A, Bloem R (eds) Computer aided verification. Springer, Berlin, pp 106\u2013113"},{"key":"344_CR50","first-page":"290","volume-title":"Verification, model checking, and abstract interpretation","author":"Z Rakamari\u0107","year":"2009","unstructured":"Rakamari\u0107 Z, Hu AJ (2009) A scalable memory model for low-level code. In: Jones ND, M\u00fcller-Olm M (eds) Verification, model checking, and abstract interpretation. Springer, Berlin, pp 290\u2013304"},{"key":"344_CR51","unstructured":"Redini N, Machiry A, Das D, Fratantonio Y, Bianchi A, Gustafson E, Shoshitaishvili Y, Kruegel C, Vigna G (2017) BootStomp: on the security of bootloaders in mobile devices. In: Kirda E, Ristenpart T (eds) 26th USENIX security symposium USENIX Association Berkeley, CA, pp 781\u2013798"},{"key":"344_CR52","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: 17th annual IEEE symposium on logic in computer science. IEEE, pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"344_CR53","unstructured":"Santa Cruz Operation (SCO): System V Application Binary Interface (1997). www.sco.com\/developers\/devspecs\/gabi41.pdf. Accessed 6 Apr 2020"},{"key":"344_CR54","doi-asserted-by":"crossref","unstructured":"Sen K (2015) Automated test generation using concolic testing. In: 8th India software engineering conference. ACM, New York, p 9","DOI":"10.1145\/2723742.2723768"},{"key":"344_CR55","unstructured":"Sinz C, Falke S, Merz F (2010) A precise memory model for low-level bounded model checking. In: 5th international workshop on systems software verification, USENIX Association, Berkeley, CA"},{"key":"344_CR56","unstructured":"Unified extensible firmware interface forum. http:\/\/www.uefi.org\/. Accessed 6 Apr 2020"},{"key":"344_CR57","doi-asserted-by":"crossref","unstructured":"Wang F, Shoshitaishvili Y (2017) Angr\u2014the next generation of binary analysis. In: 2017 IEEE cybersecurity development. IEEE, pp 8\u20139","DOI":"10.1109\/SecDev.2017.14"},{"key":"344_CR58","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-54013-4_9","volume-title":"Verification, model checking, and abstract interpretation","author":"W Wang","year":"2014","unstructured":"Wang W, Barrett C, Wies T (2014) Cascade 2.0. In: McMillan KL, Rival X (eds) Verification, model checking, and abstract interpretation. Springer, Berlin, pp 142\u2013160"},{"key":"344_CR59","doi-asserted-by":"crossref","unstructured":"Zaddach J, Bruno L, Francillon A, Balzarotti D (2014) AVATAR: a framework to support dynamic security analysis of embedded systems\u2019 firmwares. In: 21st network and distributed system security symposium. The Internet Society","DOI":"10.14722\/ndss.2014.23229"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00344-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00344-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00344-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,22]],"date-time":"2021-07-22T08:36:57Z","timestamp":1626943017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00344-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,15]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,7]]}},"alternative-id":["344"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00344-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,15]]},"assertion":[{"value":"15 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}