UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Model checking boot code from AWS data centers

Cook, B; Khazem, K; Kroening, D; Tasiran, S; Tautschnig, M; Tuttle, MR; (2020) Model checking boot code from AWS data centers. Formal Methods in System Design 10.1007/s10703-020-00344-2. (In press). Green open access

[thumbnail of Cook_Model checking boot code from AWS data centers_AOP.pdf]
Preview
Text
Cook_Model checking boot code from AWS data centers_AOP.pdf - Published version

Download (550kB) | Preview

Abstract

© 2020, The Author(s). 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.

Type: Article
Title: Model checking boot code from AWS data centers
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/s10703-020-00344-2
Publisher version: https://doi.org/10.1007/s10703-020-00344-2
Language: English
Additional information: © 2020 Springer Nature. This article is licensed under a Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/).
Keywords: Formal verification, Model checking, CBMC, Boot code, Firmware, Linker script, Amazon Web Services (AWS)
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10096782
Downloads since deposit
24Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item