Journal
FORMAL METHODS IN SYSTEM DESIGN
Volume 57, Issue 1, Pages 34-52Publisher
SPRINGER
DOI: 10.1007/s10703-020-00344-2
Keywords
Formal verification; Model checking; CBMC; Boot code; Firmware; Linker script; Amazon Web Services (AWS)
Categories
Ask authors/readers for more resources
This paper describes our experience with symbolic model checking in an industrial setting, proving the memory safety of the initial boot code running in Amazon Web Services data centers and addressing issues faced by standard static analysis tools in handling boot code.
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
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available