
By Diego Marmsoler and Achim D. Brucker.
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
Please cite this work as follows: D. Marmsoler and A. D. Brucker, “Conformance testing of formal semantics using grammar-based fuzzing,” in TAP 2022: Tests and proofs, L. Kovacs and K. Meinke, Eds. Heidelberg: Springer-Verlag, 2022. Author copy: https://logicalhacking.com/publications/marmsoler.ea-conformance-2022/
@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.},keywords = {Conformance Testing, Fuzzing, Verification, Solidity},
location = {Nantes, France},
author = {Diego Marmsoler and Achim D. Brucker},
booktitle = {{TAP} 2022: Tests And Proofs},
language = {USenglish},
publisher = {Springer-Verlag },
address = {Heidelberg },
series = {Lecture Notes in Computer Science },
editor = {Laura Kovacs and Karl Meinke},
title = {Conformance Testing of Formal Semantics using Grammar-based
Fuzzing},areas = {formal methods, software engineering},
year = {2022},
isbn = {978-3-642-38915-3},
note = {Author copy: \url{https://logicalhacking.com/publications/marmsoler.ea-conformance-2022/}},
pdf = {https://logicalhacking.com/publications/marmsoler.ea-conformance-2022/marmsoler.ea-conformance-2022.pdf},
}