pdfreaders.org

Conformance Testing of Formal Semantics using Grammar-based Fuzzing

Diego Marmsoler und Achim D. Brucker

Cover for marmsoler.ea:conformance:2022.A common problem in verification is to ensure that the formal specification models the real-world system, i.e., the implementation, faithfully. Testing is a technique that can help to bridge the gap between a formal specification and its implementation.

Fuzzing in general and grammar-based fuzzing in particular are successfully used for finding bugs in implementations. Traditional fuzzing applications rely on an implicit test specification that informally can be described as "the program under test does not crash".

In this paper, we present an approach using grammar-based fuzzing to ensure the conformance of a formal specification, namely the formal semantics of the Solidity Programming language, to a real-world implementation. For this, we derive an executable test-oracle from the formal semantics of Solidity in Isabelle/HOL. The derived test oracle is used during the fuzzing of the implementation to validate that the formal semantics and the implementation are in conformance.

Schlüsselwörter: Conformance Testing, Fuzzing, Verification, Solidity
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for marmsoler.ea:conformance:2022.Bitte zitieren sie diesen Artikel wie folgt:
Diego Marmsoler und Achim D. Brucker. Conformance Testing of Formal Semantics using Grammar-based Fuzzing. In TAP 2022: Tests And Proofs. Lecture Notes in Computer Science, Springer-Verlag, 2022.
Schlüsselwörter: Conformance Testing, Fuzzing, Verification, Solidity
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ marmsoler.ea:conformance:2022,
abstract = {A common problem in verification is to ensure that the formal specification models the real-world system, i.e., the implementation, faithfully. Testing is a technique that can help to bridge the gap between a formal specification and its implementation.\\\\Fuzzing in general and grammar-based fuzzing in particular are successfully used for finding bugs in implementations. Traditional fuzzing applications rely on an implicit test specification that informally can be described as ``the program under test does not crash''.\\\\In this paper, we present an approach using grammar-based fuzzing to ensure the conformance of a formal specification, namely the formal semantics of the Solidity Programming language, to a real-world implementation. For this, we derive an executable test-oracle from the formal semantics of Solidity in Isabelle/HOL. The derived test oracle is used during the fuzzing of the implementation to validate that the formal semantics and the implementation are in conformance.},
address = {Heidelberg},
author = {Diego Marmsoler and Achim D. Brucker},
booktitle = {{TAP} 2022: Tests And Proofs},
editor = {Laura Kovacs and Karl Meinke},
isbn = {978-3-642-38915-3},
keywords = {Conformance Testing, Fuzzing, Verification, Solidity},
language = {USenglish},
location = {Nantes, France},
pdf = {https://www.brucker.ch/bibliography/download/2022/marmsoler.ea-conformance-2022.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Conformance Testing of Formal Semantics using Grammar-based Fuzzing},
url = {https://www.brucker.ch/bibliography/abstract/marmsoler.ea-conformance-2022},
year = {2022},
}