Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2017

AUTHORS

Frédéric Mangano , Simon Duquennoy , Nikolai Kosmatov

ABSTRACT

Formal verification is still rarely applied to the IoT (Internet of Things) software, whereas IoT applications tend to become increasingly popular and critical. This short paper promotes the usage of formal verification to ensure safety and security of software in this domain. We present a successful case study on deductive verification of a memory allocation module of Contiki, a popular open-source operating system for IoT. We present the target module, describe how the code has been specified and proven using Frama-C, a software analysis platform for C code, and discuss lessons learned. More... »

PAGES

114-120

References to SciGraph publications

  • 2015. A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C in FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS
  • 2015-05. Frama-C: A software analysis perspective in FORMAL ASPECTS OF COMPUTING
  • Book

    TITLE

    Risks and Security of Internet and Systems

    ISBN

    978-3-319-54875-3
    978-3-319-54876-0

    From Grant

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-319-54876-0_9

    DOI

    http://dx.doi.org/10.1007/978-3-319-54876-0_9

    DIMENSIONS

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


    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": [
                "CEA, LIST, Software Reliability Laboratory, PC 174 Gif-sur-Yvette France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Mangano", 
            "givenName": "Fr\u00e9d\u00e9ric", 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Swedish Institute of Computer Science", 
              "id": "https://www.grid.ac/institutes/grid.6383.e", 
              "name": [
                "Inria Lille - Nord Europe Lille France", 
                "SICS Swedish ICT Kista Sweden"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Duquennoy", 
            "givenName": "Simon", 
            "id": "sg:person.016032456145.50", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016032456145.50"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "name": [
                "CEA, LIST, Software Reliability Laboratory, PC 174 Gif-sur-Yvette France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Kosmatov", 
            "givenName": "Nikolai", 
            "id": "sg:person.010500407727.29", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010500407727.29"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/s00165-014-0326-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008245247", 
              "https://doi.org/10.1007/s00165-014-0326-7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-19458-5_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024060118", 
              "https://doi.org/10.1007/978-3-319-19458-5_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/lcn.2004.38", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1094438663"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2017", 
        "datePublishedReg": "2017-01-01", 
        "description": "Formal verification is still rarely applied to the IoT (Internet of Things) software, whereas IoT applications tend to become increasingly popular and critical. This short paper promotes the usage of formal verification to ensure safety and security of software in this domain. We present a successful case study on deductive verification of a memory allocation module of Contiki, a popular open-source operating system for IoT. We present the target module, describe how the code has been specified and proven using Frama-C, a software analysis platform for C code, and discuss lessons learned.", 
        "editor": [
          {
            "familyName": "Cuppens", 
            "givenName": "Fr\u00e9d\u00e9ric", 
            "type": "Person"
          }, 
          {
            "familyName": "Cuppens", 
            "givenName": "Nora", 
            "type": "Person"
          }, 
          {
            "familyName": "Lanet", 
            "givenName": "Jean-Louis", 
            "type": "Person"
          }, 
          {
            "familyName": "Legay", 
            "givenName": "Axel", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-319-54876-0_9", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": true, 
        "isFundedItemOf": [
          {
            "id": "sg:grant.3852912", 
            "type": "MonetaryGrant"
          }
        ], 
        "isPartOf": {
          "isbn": [
            "978-3-319-54875-3", 
            "978-3-319-54876-0"
          ], 
          "name": "Risks and Security of Internet and Systems", 
          "type": "Book"
        }, 
        "name": "Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study", 
        "pagination": "114-120", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-319-54876-0_9"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "229d9d338ed54b9006605676d1a9919a07cf69ae12ff9b795c5ac5e647d7be41"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1084682113"
            ]
          }
        ], 
        "publisher": {
          "location": "Cham", 
          "name": "Springer International Publishing", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-319-54876-0_9", 
          "https://app.dimensions.ai/details/publication/pub.1084682113"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-15T17:23", 
        "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/0000000001_0000000264/records_8678_00000331.jsonl", 
        "type": "Chapter", 
        "url": "http://link.springer.com/10.1007/978-3-319-54876-0_9"
      }
    ]
     

    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-319-54876-0_9'

    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-319-54876-0_9'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-54876-0_9'

    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-319-54876-0_9'


     

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

    111 TRIPLES      23 PREDICATES      30 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-319-54876-0_9 schema:about anzsrc-for:08
    2 anzsrc-for:0803
    3 schema:author Na94d6454174b415c91c7510065d00088
    4 schema:citation sg:pub.10.1007/978-3-319-19458-5_2
    5 sg:pub.10.1007/s00165-014-0326-7
    6 https://doi.org/10.1109/lcn.2004.38
    7 schema:datePublished 2017
    8 schema:datePublishedReg 2017-01-01
    9 schema:description Formal verification is still rarely applied to the IoT (Internet of Things) software, whereas IoT applications tend to become increasingly popular and critical. This short paper promotes the usage of formal verification to ensure safety and security of software in this domain. We present a successful case study on deductive verification of a memory allocation module of Contiki, a popular open-source operating system for IoT. We present the target module, describe how the code has been specified and proven using Frama-C, a software analysis platform for C code, and discuss lessons learned.
    10 schema:editor N1e3e4c5cd4644ecba67e0ef9d6beee29
    11 schema:genre chapter
    12 schema:inLanguage en
    13 schema:isAccessibleForFree true
    14 schema:isPartOf N6de398fe0f1f4dfe925d4004d6e9098c
    15 schema:name Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study
    16 schema:pagination 114-120
    17 schema:productId N489f115448a54bf8aabb8dd9db870916
    18 N6285538794de4c10a0f1b3ad61d18de4
    19 N9cccb084b4c14118b007b4da4d962bc1
    20 schema:publisher N23d160492d2044cc974b76decaea8704
    21 schema:sameAs https://app.dimensions.ai/details/publication/pub.1084682113
    22 https://doi.org/10.1007/978-3-319-54876-0_9
    23 schema:sdDatePublished 2019-04-15T17:23
    24 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    25 schema:sdPublisher N62cb32550e1a47dc89d81e2334ef6aa3
    26 schema:url http://link.springer.com/10.1007/978-3-319-54876-0_9
    27 sgo:license sg:explorer/license/
    28 sgo:sdDataset chapters
    29 rdf:type schema:Chapter
    30 N0f28d627523149a9930680c9dc3338b3 rdf:first sg:person.010500407727.29
    31 rdf:rest rdf:nil
    32 N1e3e4c5cd4644ecba67e0ef9d6beee29 rdf:first N2aaf884b759147b4b4dbb702c75d3b12
    33 rdf:rest Nb4eda9e52e0342068e4374c5a517a75c
    34 N23d160492d2044cc974b76decaea8704 schema:location Cham
    35 schema:name Springer International Publishing
    36 rdf:type schema:Organisation
    37 N2aaf884b759147b4b4dbb702c75d3b12 schema:familyName Cuppens
    38 schema:givenName Frédéric
    39 rdf:type schema:Person
    40 N43bee2f0b9894f01a6f7b97ad4996092 rdf:first sg:person.016032456145.50
    41 rdf:rest N0f28d627523149a9930680c9dc3338b3
    42 N489f115448a54bf8aabb8dd9db870916 schema:name doi
    43 schema:value 10.1007/978-3-319-54876-0_9
    44 rdf:type schema:PropertyValue
    45 N4c15fa39871548edb265d9b8f58cc887 schema:name CEA, LIST, Software Reliability Laboratory, PC 174 Gif-sur-Yvette France
    46 rdf:type schema:Organization
    47 N568e73da3726466286603e880367df57 schema:familyName Legay
    48 schema:givenName Axel
    49 rdf:type schema:Person
    50 N6285538794de4c10a0f1b3ad61d18de4 schema:name readcube_id
    51 schema:value 229d9d338ed54b9006605676d1a9919a07cf69ae12ff9b795c5ac5e647d7be41
    52 rdf:type schema:PropertyValue
    53 N62cb32550e1a47dc89d81e2334ef6aa3 schema:name Springer Nature - SN SciGraph project
    54 rdf:type schema:Organization
    55 N67d8dd3150f14308805cc592bad94a9f schema:affiliation N4c15fa39871548edb265d9b8f58cc887
    56 schema:familyName Mangano
    57 schema:givenName Frédéric
    58 rdf:type schema:Person
    59 N6de398fe0f1f4dfe925d4004d6e9098c schema:isbn 978-3-319-54875-3
    60 978-3-319-54876-0
    61 schema:name Risks and Security of Internet and Systems
    62 rdf:type schema:Book
    63 N80ebc3369ed740f6a1848a753d75c478 rdf:first N568e73da3726466286603e880367df57
    64 rdf:rest rdf:nil
    65 N8f0174abc12f4e52ae595274c4d44b4b schema:familyName Cuppens
    66 schema:givenName Nora
    67 rdf:type schema:Person
    68 N8fdf199e2e02403a9139d53f1606da77 schema:name CEA, LIST, Software Reliability Laboratory, PC 174 Gif-sur-Yvette France
    69 rdf:type schema:Organization
    70 N9068f29ba8c04aa7972d4d7e070cdeb3 rdf:first Nc6e4eff5a43d4deebf96f4cbba11eda2
    71 rdf:rest N80ebc3369ed740f6a1848a753d75c478
    72 N9cccb084b4c14118b007b4da4d962bc1 schema:name dimensions_id
    73 schema:value pub.1084682113
    74 rdf:type schema:PropertyValue
    75 Na94d6454174b415c91c7510065d00088 rdf:first N67d8dd3150f14308805cc592bad94a9f
    76 rdf:rest N43bee2f0b9894f01a6f7b97ad4996092
    77 Nb4eda9e52e0342068e4374c5a517a75c rdf:first N8f0174abc12f4e52ae595274c4d44b4b
    78 rdf:rest N9068f29ba8c04aa7972d4d7e070cdeb3
    79 Nc6e4eff5a43d4deebf96f4cbba11eda2 schema:familyName Lanet
    80 schema:givenName Jean-Louis
    81 rdf:type schema:Person
    82 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    83 schema:name Information and Computing Sciences
    84 rdf:type schema:DefinedTerm
    85 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
    86 schema:name Computer Software
    87 rdf:type schema:DefinedTerm
    88 sg:grant.3852912 http://pending.schema.org/fundedItem sg:pub.10.1007/978-3-319-54876-0_9
    89 rdf:type schema:MonetaryGrant
    90 sg:person.010500407727.29 schema:affiliation N8fdf199e2e02403a9139d53f1606da77
    91 schema:familyName Kosmatov
    92 schema:givenName Nikolai
    93 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010500407727.29
    94 rdf:type schema:Person
    95 sg:person.016032456145.50 schema:affiliation https://www.grid.ac/institutes/grid.6383.e
    96 schema:familyName Duquennoy
    97 schema:givenName Simon
    98 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016032456145.50
    99 rdf:type schema:Person
    100 sg:pub.10.1007/978-3-319-19458-5_2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024060118
    101 https://doi.org/10.1007/978-3-319-19458-5_2
    102 rdf:type schema:CreativeWork
    103 sg:pub.10.1007/s00165-014-0326-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008245247
    104 https://doi.org/10.1007/s00165-014-0326-7
    105 rdf:type schema:CreativeWork
    106 https://doi.org/10.1109/lcn.2004.38 schema:sameAs https://app.dimensions.ai/details/publication/pub.1094438663
    107 rdf:type schema:CreativeWork
    108 https://www.grid.ac/institutes/grid.6383.e schema:alternateName Swedish Institute of Computer Science
    109 schema:name Inria Lille - Nord Europe Lille France
    110 SICS Swedish ICT Kista Sweden
    111 rdf:type schema:Organization
     




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


    ...