View in EDS

Model checking boot code from AWS data centers.

Saved in:
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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 151526932
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Model checking boot code from AWS data centers.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Cook%2C+Byron%22">Cook, Byron</searchLink><relatesTo>1,2</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Khazem%2C+Kareem%22">Khazem, Kareem</searchLink><relatesTo>1,2</relatesTo> (AUTHOR)<i> karkhaz@karkhaz.com</i><br /><searchLink fieldCode="AR" term="%22Kroening%2C+Daniel%22">Kroening, Daniel</searchLink><relatesTo>3</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Tasiran%2C+Serdar%22">Tasiran, Serdar</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Tautschnig%2C+Michael%22">Tautschnig, Michael</searchLink><relatesTo>1,4</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Tuttle%2C+Mark+R%2E%22">Tuttle, Mark R.</searchLink><relatesTo>1</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Formal+Methods+in+System+Design%22">Formal Methods in System Design</searchLink>. Jul2021, Vol. 57 Issue 1, p34-52. 19p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Amazon+Web+Services+Inc%2E%22">Amazon Web Services Inc.</searchLink><br /><searchLink fieldCode="DE" term="%22Web+services%22">Web services</searchLink><br /><searchLink fieldCode="DE" term="%22Data+security%22">Data security</searchLink><br /><searchLink fieldCode="DE" term="%22Data+centers%22">Data centers</searchLink><br /><searchLink fieldCode="DE" term="%22Scripts%22">Scripts</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=151526932
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10703-020-00344-2
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 19
        StartPage: 34
    Subjects:
      – SubjectFull: Amazon Web Services Inc.
        Type: general
      – SubjectFull: Web services
        Type: general
      – SubjectFull: Data security
        Type: general
      – SubjectFull: Data centers
        Type: general
      – SubjectFull: Scripts
        Type: general
    Titles:
      – TitleFull: Model checking boot code from AWS data centers.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Cook, Byron
      – PersonEntity:
          Name:
            NameFull: Khazem, Kareem
      – PersonEntity:
          Name:
            NameFull: Kroening, Daniel
      – PersonEntity:
          Name:
            NameFull: Tasiran, Serdar
      – PersonEntity:
          Name:
            NameFull: Tautschnig, Michael
      – PersonEntity:
          Name:
            NameFull: Tuttle, Mark R.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 07
              Text: Jul2021
              Type: published
              Y: 2021
          Identifiers:
            – Type: issn-print
              Value: 09259856
          Numbering:
            – Type: volume
              Value: 57
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Formal Methods in System Design
              Type: main
ResultId 1