Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2022-05-27

AUTHORS

Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi

ABSTRACT

A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature. More... »

PAGES

507-540

References to SciGraph publications

  • 2020-08-13. Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts in FORMAL METHODS. FM 2019 INTERNATIONAL WORKSHOPS
  • 2011. Lem: A Lightweight Tool for Heavyweight Semantics in INTERACTIVE THEOREM PROVING
  • 2008. Z3: An Efficient SMT Solver in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2005. A Typed, Compositional Logic for a Stack-Based Abstract Machine in PROGRAMMING LANGUAGES AND SYSTEMS
  • 2017-11-19. Defining the Ethereum Virtual Machine for Interactive Theorem Provers in FINANCIAL CRYPTOGRAPHY AND DATA SECURITY
  • 2013. Compositional and Lightweight Dependent Type Inference for ML in VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s00354-022-00167-1

    DOI

    http://dx.doi.org/10.1007/s00354-022-00167-1

    DIMENSIONS

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


    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/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Kyoto University, Kyoto, Japan", 
              "id": "http://www.grid.ac/institutes/grid.258799.8", 
              "name": [
                "Kyoto University, Kyoto, Japan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Nishida", 
            "givenName": "Yuki", 
            "id": "sg:person.012737271257.12", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012737271257.12"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Kyoto University, Kyoto, Japan", 
              "id": "http://www.grid.ac/institutes/grid.258799.8", 
              "name": [
                "Kyoto University, Kyoto, Japan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Saito", 
            "givenName": "Hiromasa", 
            "id": "sg:person.011513617427.45", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011513617427.45"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Kyoto University, Kyoto, Japan", 
              "id": "http://www.grid.ac/institutes/grid.258799.8", 
              "name": [
                "Kyoto University, Kyoto, Japan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Chen", 
            "givenName": "Ran", 
            "id": "sg:person.013106560427.03", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013106560427.03"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Kyoto University, Kyoto, Japan", 
              "id": "http://www.grid.ac/institutes/grid.258799.8", 
              "name": [
                "Kyoto University, Kyoto, Japan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Kawata", 
            "givenName": "Akira", 
            "id": "sg:person.013704141027.24", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013704141027.24"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "DaiLambda, Inc., Kyoto, Japan", 
              "id": "http://www.grid.ac/institutes/None", 
              "name": [
                "DaiLambda, Inc., Kyoto, Japan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Furuse", 
            "givenName": "Jun", 
            "id": "sg:person.015277102027.97", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015277102027.97"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Kyoto University, Kyoto, Japan", 
              "id": "http://www.grid.ac/institutes/grid.258799.8", 
              "name": [
                "Kyoto University, Kyoto, Japan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Suenaga", 
            "givenName": "Kohei", 
            "id": "sg:person.016612020443.35", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016612020443.35"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Kyoto University, Kyoto, Japan", 
              "id": "http://www.grid.ac/institutes/grid.258799.8", 
              "name": [
                "Kyoto University, Kyoto, Japan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Igarashi", 
            "givenName": "Atsushi", 
            "id": "sg:person.010772740673.77", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010772740673.77"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-3-319-70278-0_33", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1092750884", 
              "https://doi.org/10.1007/978-3-319-70278-0_33"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11575467_24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1017418022", 
              "https://doi.org/10.1007/11575467_24"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-030-54994-7_28", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1130068930", 
              "https://doi.org/10.1007/978-3-030-54994-7_28"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-78800-3_24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034005359", 
              "https://doi.org/10.1007/978-3-540-78800-3_24"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-35873-9_19", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012884073", 
              "https://doi.org/10.1007/978-3-642-35873-9_19"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-22863-6_27", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1021484060", 
              "https://doi.org/10.1007/978-3-642-22863-6_27"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2022-05-27", 
        "datePublishedReg": "2022-05-27", 
        "description": "A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson\u2019s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s00354-022-00167-1", 
        "isAccessibleForFree": true, 
        "isPartOf": [
          {
            "id": "sg:journal.1053619", 
            "issn": [
              "0288-3635", 
              "1882-7055"
            ], 
            "name": "New Generation Computing", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "40"
          }
        ], 
        "keywords": [
          "smart contracts", 
          "type system", 
          "refinement types", 
          "SMT solver Z3", 
          "stack-based language", 
          "refinement type system", 
          "user-defined specifications", 
          "digital signature", 
          "verification conditions", 
          "higher-order functions", 
          "large amount", 
          "specification", 
          "blockchain", 
          "verifier", 
          "datatypes", 
          "invocation", 
          "cryptocurrencies", 
          "system", 
          "transactions", 
          "contracts", 
          "Tezos", 
          "language", 
          "input", 
          "program", 
          "features", 
          "Z3", 
          "demand", 
          "extension", 
          "top", 
          "money", 
          "method", 
          "types", 
          "signatures", 
          "amount", 
          "article", 
          "account", 
          "function", 
          "form", 
          "characteristic features", 
          "Michelson", 
          "conditions", 
          "Helmholtz"
        ], 
        "name": "Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types", 
        "pagination": "507-540", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1148218933"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s00354-022-00167-1"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s00354-022-00167-1", 
          "https://app.dimensions.ai/details/publication/pub.1148218933"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-11-24T21:09", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-springernature-scigraph/baseset/20221124/entities/gbq_results/article/article_949.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s00354-022-00167-1"
      }
    ]
     

    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/s00354-022-00167-1'

    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/s00354-022-00167-1'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s00354-022-00167-1'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s00354-022-00167-1'


     

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

    168 TRIPLES      21 PREDICATES      71 URIs      57 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s00354-022-00167-1 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author N522242e8c3ca4fd69519b75ce7ab1cab
    4 schema:citation sg:pub.10.1007/11575467_24
    5 sg:pub.10.1007/978-3-030-54994-7_28
    6 sg:pub.10.1007/978-3-319-70278-0_33
    7 sg:pub.10.1007/978-3-540-78800-3_24
    8 sg:pub.10.1007/978-3-642-22863-6_27
    9 sg:pub.10.1007/978-3-642-35873-9_19
    10 schema:datePublished 2022-05-27
    11 schema:datePublishedReg 2022-05-27
    12 schema:description A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.
    13 schema:genre article
    14 schema:isAccessibleForFree true
    15 schema:isPartOf N997a33eefc0d474883d2015f7a4d9aeb
    16 Nba922f5e2755417bb4931d0f1d27d374
    17 sg:journal.1053619
    18 schema:keywords Helmholtz
    19 Michelson
    20 SMT solver Z3
    21 Tezos
    22 Z3
    23 account
    24 amount
    25 article
    26 blockchain
    27 characteristic features
    28 conditions
    29 contracts
    30 cryptocurrencies
    31 datatypes
    32 demand
    33 digital signature
    34 extension
    35 features
    36 form
    37 function
    38 higher-order functions
    39 input
    40 invocation
    41 language
    42 large amount
    43 method
    44 money
    45 program
    46 refinement type system
    47 refinement types
    48 signatures
    49 smart contracts
    50 specification
    51 stack-based language
    52 system
    53 top
    54 transactions
    55 type system
    56 types
    57 user-defined specifications
    58 verification conditions
    59 verifier
    60 schema:name Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
    61 schema:pagination 507-540
    62 schema:productId Nc611c076d6da4e87b608533bff302c42
    63 Nd316b60dade547d3a15e472b0cfca6a3
    64 schema:sameAs https://app.dimensions.ai/details/publication/pub.1148218933
    65 https://doi.org/10.1007/s00354-022-00167-1
    66 schema:sdDatePublished 2022-11-24T21:09
    67 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    68 schema:sdPublisher N718cdf3c3f704214aa355caa14a02a1f
    69 schema:url https://doi.org/10.1007/s00354-022-00167-1
    70 sgo:license sg:explorer/license/
    71 sgo:sdDataset articles
    72 rdf:type schema:ScholarlyArticle
    73 N43ca781b0d624b05b95d08e87fc417b5 rdf:first sg:person.013106560427.03
    74 rdf:rest N9773925a9a81414883e3998c12e7d9bb
    75 N4e7102129fb9470e94ebd217c0ea0a7e rdf:first sg:person.015277102027.97
    76 rdf:rest Nae4c9dd79f27449faa25e8d0728ebf91
    77 N522242e8c3ca4fd69519b75ce7ab1cab rdf:first sg:person.012737271257.12
    78 rdf:rest Nd93e7e7f2a3549f993d68c3390f2936a
    79 N718cdf3c3f704214aa355caa14a02a1f schema:name Springer Nature - SN SciGraph project
    80 rdf:type schema:Organization
    81 N82538773492d4cd1b6c04cd362c1feb8 rdf:first sg:person.010772740673.77
    82 rdf:rest rdf:nil
    83 N9773925a9a81414883e3998c12e7d9bb rdf:first sg:person.013704141027.24
    84 rdf:rest N4e7102129fb9470e94ebd217c0ea0a7e
    85 N997a33eefc0d474883d2015f7a4d9aeb schema:volumeNumber 40
    86 rdf:type schema:PublicationVolume
    87 Nae4c9dd79f27449faa25e8d0728ebf91 rdf:first sg:person.016612020443.35
    88 rdf:rest N82538773492d4cd1b6c04cd362c1feb8
    89 Nba922f5e2755417bb4931d0f1d27d374 schema:issueNumber 2
    90 rdf:type schema:PublicationIssue
    91 Nc611c076d6da4e87b608533bff302c42 schema:name dimensions_id
    92 schema:value pub.1148218933
    93 rdf:type schema:PropertyValue
    94 Nd316b60dade547d3a15e472b0cfca6a3 schema:name doi
    95 schema:value 10.1007/s00354-022-00167-1
    96 rdf:type schema:PropertyValue
    97 Nd93e7e7f2a3549f993d68c3390f2936a rdf:first sg:person.011513617427.45
    98 rdf:rest N43ca781b0d624b05b95d08e87fc417b5
    99 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    100 schema:name Information and Computing Sciences
    101 rdf:type schema:DefinedTerm
    102 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    103 schema:name Computation Theory and Mathematics
    104 rdf:type schema:DefinedTerm
    105 sg:journal.1053619 schema:issn 0288-3635
    106 1882-7055
    107 schema:name New Generation Computing
    108 schema:publisher Springer Nature
    109 rdf:type schema:Periodical
    110 sg:person.010772740673.77 schema:affiliation grid-institutes:grid.258799.8
    111 schema:familyName Igarashi
    112 schema:givenName Atsushi
    113 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010772740673.77
    114 rdf:type schema:Person
    115 sg:person.011513617427.45 schema:affiliation grid-institutes:grid.258799.8
    116 schema:familyName Saito
    117 schema:givenName Hiromasa
    118 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011513617427.45
    119 rdf:type schema:Person
    120 sg:person.012737271257.12 schema:affiliation grid-institutes:grid.258799.8
    121 schema:familyName Nishida
    122 schema:givenName Yuki
    123 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012737271257.12
    124 rdf:type schema:Person
    125 sg:person.013106560427.03 schema:affiliation grid-institutes:grid.258799.8
    126 schema:familyName Chen
    127 schema:givenName Ran
    128 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013106560427.03
    129 rdf:type schema:Person
    130 sg:person.013704141027.24 schema:affiliation grid-institutes:grid.258799.8
    131 schema:familyName Kawata
    132 schema:givenName Akira
    133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013704141027.24
    134 rdf:type schema:Person
    135 sg:person.015277102027.97 schema:affiliation grid-institutes:None
    136 schema:familyName Furuse
    137 schema:givenName Jun
    138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015277102027.97
    139 rdf:type schema:Person
    140 sg:person.016612020443.35 schema:affiliation grid-institutes:grid.258799.8
    141 schema:familyName Suenaga
    142 schema:givenName Kohei
    143 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016612020443.35
    144 rdf:type schema:Person
    145 sg:pub.10.1007/11575467_24 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017418022
    146 https://doi.org/10.1007/11575467_24
    147 rdf:type schema:CreativeWork
    148 sg:pub.10.1007/978-3-030-54994-7_28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1130068930
    149 https://doi.org/10.1007/978-3-030-54994-7_28
    150 rdf:type schema:CreativeWork
    151 sg:pub.10.1007/978-3-319-70278-0_33 schema:sameAs https://app.dimensions.ai/details/publication/pub.1092750884
    152 https://doi.org/10.1007/978-3-319-70278-0_33
    153 rdf:type schema:CreativeWork
    154 sg:pub.10.1007/978-3-540-78800-3_24 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034005359
    155 https://doi.org/10.1007/978-3-540-78800-3_24
    156 rdf:type schema:CreativeWork
    157 sg:pub.10.1007/978-3-642-22863-6_27 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021484060
    158 https://doi.org/10.1007/978-3-642-22863-6_27
    159 rdf:type schema:CreativeWork
    160 sg:pub.10.1007/978-3-642-35873-9_19 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012884073
    161 https://doi.org/10.1007/978-3-642-35873-9_19
    162 rdf:type schema:CreativeWork
    163 grid-institutes:None schema:alternateName DaiLambda, Inc., Kyoto, Japan
    164 schema:name DaiLambda, Inc., Kyoto, Japan
    165 rdf:type schema:Organization
    166 grid-institutes:grid.258799.8 schema:alternateName Kyoto University, Kyoto, Japan
    167 schema:name Kyoto University, Kyoto, Japan
    168 rdf:type schema:Organization
     




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


    ...