2

I am currently researching about the formal verification of smart contracts. I am surprised that I did not manage to find a paper about the (shape) analysis of the storage of a contract.

Is there in the literature or in github a tool to perform shape analysis (on the storage and/or memory) of Ethereum? If not, it is so, because this problem is not a concern or why nobody studied this problem?

Briomkez
  • 1,894
  • 1
  • 11
  • 33
  • There's this article about blockchain size https://dev.to/5chdn/the-ethereum-blockchain-size-will-not-exceed-1tb-anytime-soon-58a but I don't know if there's an automated way of analysis. – Ismael Sep 24 '18 at 18:55

1 Answers1

1

We can see the application of a number of interesting formal verification tools and frameworks on Ethereum lately. In the event of rising attack vectors against the smart contract security model of Ethereum, formal verification has become a strong imperative. Initial efforts were based on Coq proof assistant. Nowadays we can see the adoption of K-framework and other powerful tools.

Ethereum 2.0 Beacon Chain has been formally verified using Dafny in the PegaSysEng/eth2.0-dafny repository. Runtime Verification has done an excellent formal verification of Ethereum Casper CBC Proofs recently. It is available in the following repository. There is also an interesting formal verification of Ethereum in Lem in the pirapira /eth-isabelle repository. Lem is a language that can be translated into Coq, Isabelle/HOL, HOL4, OCaml, HTML and LaTeX. There is another interesting EVM Semantics GitHub repository that applies the K-framework based formal verification of Ethereum Virtual Machine.

Gokul Alex
  • 390
  • 1
  • 14