Model Checking Boot Code from AWS Data Centers
- Submitting institution
-
Queen Mary University of London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 544
- Type
- D - Journal article
- DOI
-
10.1007/s10703-020-00344-2
- Title of journal
- Formal Methods in System Design
- Article number
- -
- First page
- 1
- Volume
- 0
- Issue
- -
- ISSN
- 0925-9856
- Open access status
- Compliant
- Month of publication
- July
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
5
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Extensions to and application of C Bounded Model Checker (Tautschnig is co-lead of project) to verify boot code deployed on 300,000+ servers in Amazon data centres. Proof that initial stages of system boot cannot have memory safety errors, which proves that the systems cannot be forced to boot in an attacker-modified state. Informal feedback by CAV2018 (Computer Aided Verification) steering committee that this is the best paper seen in 10 years. Among most prestigious academic publication as part of Amazon Web Services' provable security initiative: https://aws.amazon.com/security/provable-security/. Contact at AWS: Byron Cook, byron@amazon.com. This is the extended journal version.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -