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).
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 |
Loading...
Loading...Loading...| 1. |  United States | 7 |
| 2. |  United Kingdom | 1 |
Archive Staff Only
 |
View Item |
