Specifying Framing Conditions for Smart Contracts

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert und Jonas Schiffl
In:ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation
Verleger:Springer International Publishing
Jahr:2020
Seiten:43-59

Abstract

Smart contracts are programs which run in conjunction with distributed ledgers. They often manage valuable assets, but, like all programs, they contain errors which can be exploited by an attacker. This makes them are a prime target for formal methods. Many formal analysis methods require the contracts' program code to be annotated with formal specifications. In this paper, we propose an approach and a formalism to enrich specifications with frame conditions, i.e., a specification of what a smart contract function cannot resp. will not do. We discuss the storage models of two smart contract platforms, Ethereum and Hyperledger Fabric, and propose languages for specifying frame conditions for both of them, based on the theory of dynamic frames.

BibTeX

@inproceedings{beckert_specifying_2020,
	location = {Cham},
	title = {Specifying Framing Conditions for Smart Contracts},
	isbn = {978-3-030-61467-6},
	abstract = {Smart contracts are programs which run in conjunction with distributed ledgers.
                    They often manage valuable assets, but, like all programs, they contain errors
                    which can be exploited by an attacker. This makes them are a prime target for
                    formal methods. Many formal analysis methods require the contracts' program code
                    to be annotated with formal specifications. In this paper, we propose an approach
                    and a formalism to enrich specifications with frame conditions, i.e., a
                    specification of what a smart contract function cannot resp. will not do. We
                    discuss the storage models of two smart contract platforms, Ethereum and
                    Hyperledger Fabric, and propose languages for specifying frame conditions for
                    both of them, based on the theory of dynamic frames.},
	pages = {43--59},
	booktitle = {ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation},
	publisher = {Springer International Publishing},
	author = {Bernhard Beckert and Jonas Schiffl},
	editor = {Tiziana Margaria and Bernhard Steffen},
	year = {2020},
        month = oct
}