Model checking boot code from AWS data centers

Conference item

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.

Authors: Cook, B; Khazem, K; Kroening, D; Tasiran, S; Tautschnig, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer
• Host title: CAV 2018: Computer Aided Verification
• Journal: 30th International Conference on Computer Aided Verification (CAV 2018)
• Volume: 10982
• Pages: 467-486
• Publication date: 2018-07-18
• Acceptance date: 2018-03-31
• DOI: 10.1007/978-3-319-96142-2_28
• ISSN: 0302-9743
• ISBN: 9783319961422