Bibliographic Details
| Title: |
Model checking boot code from AWS data centers. |
| Authors: |
Cook, Byron1,2 (AUTHOR), Khazem, Kareem1,2 (AUTHOR) karkhaz@karkhaz.com, Kroening, Daniel3 (AUTHOR), Tasiran, Serdar1 (AUTHOR), Tautschnig, Michael1,4 (AUTHOR), Tuttle, Mark R.1 (AUTHOR) |
| Source: |
Formal Methods in System Design. Jul2021, Vol. 57 Issue 1, p34-52. 19p. |
| Subjects: |
Amazon Web Services Inc., Web services, Data security, Data centers, Scripts |
| Abstract: |
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. [ABSTRACT FROM AUTHOR] |
|
Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
