pdfreaders.org

Conformance Testing of Formal Semantics using Grammar-based Fuzzing

by Diego Marmsoler and 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.

Keywords: Conformance Testing, Fuzzing, Verification, Solidity
Categories: ,
Documents: (full text as PDF file)

QR Code for marmsoler.ea:conformance:2022.Please cite this article as follows:
Diego Marmsoler and 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.
Keywords: Conformance Testing, Fuzzing, Verification, Solidity
(full text as PDF file) (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},
}