Conformance Testing of Formal Semantics using Grammar-based Fuzzing

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/

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.},
  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},
}