Development of Security Software: A High Assurance Methodology View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2009

AUTHORS

David Hardin , T. Douglas Hiratzka , D. Randolph Johnson , Lucas Wagner , Michael Whalen

ABSTRACT

This paper reports on a project to exercise, evaluate and enhance a methodology for developing high assurance software for an embedded system controller. In this approach, researchers at the National Security Agency capture system requirements precisely and unambiguously through functional specifications in Z. Rockwell Collins then implements these requirements using an integrated, model-based software development approach. The development effort is supported by a tool chain that provides automated code generation and support for formal verification. The specific system is a prototype high speed encryption system, although the controller could be adapted for use in a variety of critical systems in which very high assurance of correctness, reliability, and security or safety properties is essential. More... »

PAGES

266-285

References to SciGraph publications

  • 2008. Integration of Formal Analysis into a Model-Based Software Development Process in FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS
  • 1997. The Z/EVES system in ZUM '97: THE Z FORMAL SPECIFICATION NOTATION
  • 2006. Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices in FORMAL METHODS AND SOFTWARE ENGINEERING
  • Book

    TITLE

    Formal Methods and Software Engineering

    ISBN

    978-3-642-10372-8
    978-3-642-10373-5

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-642-10373-5_14

    DOI

    http://dx.doi.org/10.1007/978-3-642-10373-5_14

    DIMENSIONS

    https://app.dimensions.ai/details/publication/pub.1020658567


    Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
    Incoming Citations Browse incoming citations for this publication using opencitations.net

    JSON-LD is the canonical representation for SciGraph data.

    TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

    [
      {
        "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
        "about": [
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computer Software", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "name": [
                "Rockwell Collins, Inc."
              ], 
              "type": "Organization"
            }, 
            "familyName": "Hardin", 
            "givenName": "David", 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "name": [
                "Rockwell Collins, Inc."
              ], 
              "type": "Organization"
            }, 
            "familyName": "Hiratzka", 
            "givenName": "T. Douglas", 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "National Security Agency", 
              "id": "https://www.grid.ac/institutes/grid.482831.4", 
              "name": [
                "National Security Agency"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Johnson", 
            "givenName": "D. Randolph", 
            "id": "sg:person.014671060017.63", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014671060017.63"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "name": [
                "Rockwell Collins, Inc."
              ], 
              "type": "Organization"
            }, 
            "familyName": "Wagner", 
            "givenName": "Lucas", 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "name": [
                "Rockwell Collins, Inc."
              ], 
              "type": "Organization"
            }, 
            "familyName": "Whalen", 
            "givenName": "Michael", 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-3-540-79707-4_7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1020357405", 
              "https://doi.org/10.1007/978-3-540-79707-4_7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11901433_34", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022271686", 
              "https://doi.org/10.1007/11901433_34"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11901433_34", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022271686", 
              "https://doi.org/10.1007/11901433_34"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0027284", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1046642040", 
              "https://doi.org/10.1007/bfb0027284"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/fmcad.2008.ecp.5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1093483464"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2009", 
        "datePublishedReg": "2009-01-01", 
        "description": "This paper reports on a project to exercise, evaluate and enhance a methodology for developing high assurance software for an embedded system controller. In this approach, researchers at the National Security Agency capture system requirements precisely and unambiguously through functional specifications in Z. Rockwell Collins then implements these requirements using an integrated, model-based software development approach. The development effort is supported by a tool chain that provides automated code generation and support for formal verification. The specific system is a prototype high speed encryption system, although the controller could be adapted for use in a variety of critical systems in which very high assurance of correctness, reliability, and security or safety properties is essential.", 
        "editor": [
          {
            "familyName": "Breitman", 
            "givenName": "Karin", 
            "type": "Person"
          }, 
          {
            "familyName": "Cavalcanti", 
            "givenName": "Ana", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-642-10373-5_14", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-642-10372-8", 
            "978-3-642-10373-5"
          ], 
          "name": "Formal Methods and Software Engineering", 
          "type": "Book"
        }, 
        "name": "Development of Security Software: A High Assurance Methodology", 
        "pagination": "266-285", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1020658567"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-642-10373-5_14"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "626ea69b1f334d9e8bd1c31d82a285274185f26c6f35c1d6c289835fa21a1a38"
            ]
          }
        ], 
        "publisher": {
          "location": "Berlin, Heidelberg", 
          "name": "Springer Berlin Heidelberg", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-642-10373-5_14", 
          "https://app.dimensions.ai/details/publication/pub.1020658567"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-16T07:26", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000355_0000000355/records_52997_00000000.jsonl", 
        "type": "Chapter", 
        "url": "https://link.springer.com/10.1007%2F978-3-642-10373-5_14"
      }
    ]
     

    Download the RDF metadata as:  json-ld nt turtle xml License info

    HOW TO GET THIS DATA PROGRAMMATICALLY:

    JSON-LD is a popular format for linked data which is fully compatible with JSON.

    curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-10373-5_14'

    N-Triples is a line-based linked data format ideal for batch operations.

    curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-10373-5_14'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-10373-5_14'

    RDF/XML is a standard XML format for linked data.

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-10373-5_14'


     

    This table displays all metadata directly associated to this object as RDF triples.

    117 TRIPLES      23 PREDICATES      31 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-642-10373-5_14 schema:about anzsrc-for:08
    2 anzsrc-for:0803
    3 schema:author N4fcf6173381447d1a061ed567d6e8223
    4 schema:citation sg:pub.10.1007/11901433_34
    5 sg:pub.10.1007/978-3-540-79707-4_7
    6 sg:pub.10.1007/bfb0027284
    7 https://doi.org/10.1109/fmcad.2008.ecp.5
    8 schema:datePublished 2009
    9 schema:datePublishedReg 2009-01-01
    10 schema:description This paper reports on a project to exercise, evaluate and enhance a methodology for developing high assurance software for an embedded system controller. In this approach, researchers at the National Security Agency capture system requirements precisely and unambiguously through functional specifications in Z. Rockwell Collins then implements these requirements using an integrated, model-based software development approach. The development effort is supported by a tool chain that provides automated code generation and support for formal verification. The specific system is a prototype high speed encryption system, although the controller could be adapted for use in a variety of critical systems in which very high assurance of correctness, reliability, and security or safety properties is essential.
    11 schema:editor N9656e1232f24442ba9d2d43b88dd8040
    12 schema:genre chapter
    13 schema:inLanguage en
    14 schema:isAccessibleForFree false
    15 schema:isPartOf N2f25a49474164c78948e82278cdbd1ba
    16 schema:name Development of Security Software: A High Assurance Methodology
    17 schema:pagination 266-285
    18 schema:productId N20f562d24afc45ba9cb44114a5881f4c
    19 N5dff5c54cffc40e28f3a7172986dd9be
    20 N8fa63a154ce944d3b505b309cd971bee
    21 schema:publisher N84e6b2f31075466393bb4f6328e409f2
    22 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020658567
    23 https://doi.org/10.1007/978-3-642-10373-5_14
    24 schema:sdDatePublished 2019-04-16T07:26
    25 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    26 schema:sdPublisher Nd9dd397f4d3a4e928f2a240cfa734b98
    27 schema:url https://link.springer.com/10.1007%2F978-3-642-10373-5_14
    28 sgo:license sg:explorer/license/
    29 sgo:sdDataset chapters
    30 rdf:type schema:Chapter
    31 N055eae954f774ab88c02a22c5e5f0f88 rdf:first Nf520353e062445dc9520f2cf0fc76dd6
    32 rdf:rest rdf:nil
    33 N0c0f46f17ee54db2acf5caf7023e807f schema:affiliation N6aa36e4c46e244f89ded577b368ef7f9
    34 schema:familyName Wagner
    35 schema:givenName Lucas
    36 rdf:type schema:Person
    37 N0d1969c46de64fdb87c2703d9e2be2bd schema:name Rockwell Collins, Inc.
    38 rdf:type schema:Organization
    39 N20f562d24afc45ba9cb44114a5881f4c schema:name dimensions_id
    40 schema:value pub.1020658567
    41 rdf:type schema:PropertyValue
    42 N2f25a49474164c78948e82278cdbd1ba schema:isbn 978-3-642-10372-8
    43 978-3-642-10373-5
    44 schema:name Formal Methods and Software Engineering
    45 rdf:type schema:Book
    46 N4fcf6173381447d1a061ed567d6e8223 rdf:first Nc509c25faf414963a499ab45ed3461d6
    47 rdf:rest Nee929832b22c47c5a45648962d403b8a
    48 N4fd5d79eda5f492398435f11d53adf66 rdf:first N83449265e1af49ebb71891f70f372dd7
    49 rdf:rest rdf:nil
    50 N5dff5c54cffc40e28f3a7172986dd9be schema:name readcube_id
    51 schema:value 626ea69b1f334d9e8bd1c31d82a285274185f26c6f35c1d6c289835fa21a1a38
    52 rdf:type schema:PropertyValue
    53 N6aa36e4c46e244f89ded577b368ef7f9 schema:name Rockwell Collins, Inc.
    54 rdf:type schema:Organization
    55 N7491e75bf4f1455796288183b92e9b68 schema:name Rockwell Collins, Inc.
    56 rdf:type schema:Organization
    57 N7e282b05b5c343f392c0d98ffb1b46ba rdf:first sg:person.014671060017.63
    58 rdf:rest Nc87181a6aaa44515bb0e0d990cf4cef2
    59 N83449265e1af49ebb71891f70f372dd7 schema:familyName Cavalcanti
    60 schema:givenName Ana
    61 rdf:type schema:Person
    62 N84e6b2f31075466393bb4f6328e409f2 schema:location Berlin, Heidelberg
    63 schema:name Springer Berlin Heidelberg
    64 rdf:type schema:Organisation
    65 N8b8101e362fd4ce0abf4e59bfadbaf80 schema:name Rockwell Collins, Inc.
    66 rdf:type schema:Organization
    67 N8fa63a154ce944d3b505b309cd971bee schema:name doi
    68 schema:value 10.1007/978-3-642-10373-5_14
    69 rdf:type schema:PropertyValue
    70 N9656e1232f24442ba9d2d43b88dd8040 rdf:first Nb6c87fb2261e43a3b4b8c5bae782256e
    71 rdf:rest N4fd5d79eda5f492398435f11d53adf66
    72 Nb6c87fb2261e43a3b4b8c5bae782256e schema:familyName Breitman
    73 schema:givenName Karin
    74 rdf:type schema:Person
    75 Nc0e01ea885314341ab22bf707be80644 schema:affiliation N8b8101e362fd4ce0abf4e59bfadbaf80
    76 schema:familyName Hiratzka
    77 schema:givenName T. Douglas
    78 rdf:type schema:Person
    79 Nc509c25faf414963a499ab45ed3461d6 schema:affiliation N0d1969c46de64fdb87c2703d9e2be2bd
    80 schema:familyName Hardin
    81 schema:givenName David
    82 rdf:type schema:Person
    83 Nc87181a6aaa44515bb0e0d990cf4cef2 rdf:first N0c0f46f17ee54db2acf5caf7023e807f
    84 rdf:rest N055eae954f774ab88c02a22c5e5f0f88
    85 Nd9dd397f4d3a4e928f2a240cfa734b98 schema:name Springer Nature - SN SciGraph project
    86 rdf:type schema:Organization
    87 Nee929832b22c47c5a45648962d403b8a rdf:first Nc0e01ea885314341ab22bf707be80644
    88 rdf:rest N7e282b05b5c343f392c0d98ffb1b46ba
    89 Nf520353e062445dc9520f2cf0fc76dd6 schema:affiliation N7491e75bf4f1455796288183b92e9b68
    90 schema:familyName Whalen
    91 schema:givenName Michael
    92 rdf:type schema:Person
    93 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    94 schema:name Information and Computing Sciences
    95 rdf:type schema:DefinedTerm
    96 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
    97 schema:name Computer Software
    98 rdf:type schema:DefinedTerm
    99 sg:person.014671060017.63 schema:affiliation https://www.grid.ac/institutes/grid.482831.4
    100 schema:familyName Johnson
    101 schema:givenName D. Randolph
    102 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014671060017.63
    103 rdf:type schema:Person
    104 sg:pub.10.1007/11901433_34 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022271686
    105 https://doi.org/10.1007/11901433_34
    106 rdf:type schema:CreativeWork
    107 sg:pub.10.1007/978-3-540-79707-4_7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020357405
    108 https://doi.org/10.1007/978-3-540-79707-4_7
    109 rdf:type schema:CreativeWork
    110 sg:pub.10.1007/bfb0027284 schema:sameAs https://app.dimensions.ai/details/publication/pub.1046642040
    111 https://doi.org/10.1007/bfb0027284
    112 rdf:type schema:CreativeWork
    113 https://doi.org/10.1109/fmcad.2008.ecp.5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1093483464
    114 rdf:type schema:CreativeWork
    115 https://www.grid.ac/institutes/grid.482831.4 schema:alternateName National Security Agency
    116 schema:name National Security Agency
    117 rdf:type schema:Organization
     




    Preview window. Press ESC to close (or click here)


    ...