Predicate abstractions for smart contract validation
File(s)
Author(s)
Godoy, Javier
Galeotti, Juan Pablo
Garbervetsky, Diego
Uchitel, Sebastian
Type
Conference Paper
Abstract
Smart contracts are immutable programs deployed on the blockchain
that can manage significant assets. Because of this, verification and
validation of smart contracts is of vital importance. Indeed, it is
industrial practice to hire independent specialized companies to
audit smart contracts before deployment. Auditors typically rely
on a combination of tools and experience but still fail to identify
problems in smart contracts before deployment, causing significant
losses. In this paper, we propose using predicate abstraction to con-
struct models which can be used by auditors to explore and validate
smart contact behaviour at the function call level by proposing
predicates that expose different aspects of the contract. We pro-
pose predicates based on requires clauses and enum-type state
variables as a starting point for contract validation and report on
an evaluation on two different benchmarks.
that can manage significant assets. Because of this, verification and
validation of smart contracts is of vital importance. Indeed, it is
industrial practice to hire independent specialized companies to
audit smart contracts before deployment. Auditors typically rely
on a combination of tools and experience but still fail to identify
problems in smart contracts before deployment, causing significant
losses. In this paper, we propose using predicate abstraction to con-
struct models which can be used by auditors to explore and validate
smart contact behaviour at the function call level by proposing
predicates that expose different aspects of the contract. We pro-
pose predicates based on requires clauses and enum-type state
variables as a starting point for contract validation and report on
an evaluation on two different benchmarks.
Date Issued
2022-10-24
Date Acceptance
2022-07-13
Citation
ACM / IEEE 25th International Conference on Model Driven Engineering Languages and Systems (MODELS), 2022, pp.289-299
Publisher
IEEE
Start Page
289
End Page
299
Journal / Book Title
ACM / IEEE 25th International Conference on Model Driven Engineering Languages and Systems (MODELS)
Copyright Statement
© 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in https://doi.org/10.1145/3550355.3552462
Identifier
https://dl.acm.org/doi/10.1145/3550355.3552462
Source
ACM / IEEE 25th International Conference on Model Driven Engineering Languages and Systems (MODELS 2022)
Publication Status
Published
Start Date
2022-10-23
Finish Date
2022-10-28
Coverage Spatial
Montreal, Canada
Date Publish Online
2022-10-24