Add page on formal verification for smart contracts #6394
Conversation
This page offers a high-level introduction to the concept of formal verification of Ethereum smart contracts.
emmanuel-awosika
requested review from
samajammin,
wackerow,
corwintines,
pettinarip and
minimalsm
as code owners
github-actions
bot
added
content 🖋️
Gatsby Cloud Build Reportethereum-org-website-dev 🎉 Your build was successful! See the Deploy preview here. Build Details🕐 Build time: 13m |
|
FYI I edited the PR description to link to the corresponding issue (#6194). |
src/content/developers/docs/smart-contracts/formal-verification.md
Outdated
Show resolved
Hide resolved
…n.md Co-authored-by: Sam Richards <[email protected]>
Oh, I thought they were separate pages? |
Fixed internal link issues.
| --- | ||
|
|
||
|
|
||
| ## A brief introduction {#introduction-to-formal-verification} |
There was a problem hiding this comment.
I'd say we could just remove this header. Many of our docs pages jump straight into the intro, e.g.
|
@emmanuel-awosika haven't been able to review this in detail yet but at first glance it looks like a great start! I'll share this around with some folks to get some eyes & input on it. Thanks again! FYI I just pushed a couple commits to rename the file (index.md in a directory is our typical pattern) & added the page to the docs navigation. |
|
|
||
| Formal verification is grounded in [formal methods](https://en.wikipedia.org/wiki/Formal_methods), which use mathematically rigorous methods for specifying, developing, and verifying software. Formal verification allows developers to mathematically model software programs and create formalized specifications, making testing more precise and robust. | ||
|
|
||
| Specifications are properties or used to describe the intended behavior of a smart contract. Formal verification can prove that a contract behaves exactly as described in the specification. Unlike testing based on informal assumptions, formal verification provides mathematical proof of a smart contract's correctness. |
There was a problem hiding this comment.
Specifications are properties or used to
This sentence doesn't make sense to me. Should it be "Specifications are properties used to", or something else?
There was a problem hiding this comment.
It's a typo. The sentence should read "specifications are properties used to...". I'll edit the content to fix it.
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
…n/index.md Co-authored-by: Sam Richards <[email protected]>
Fixed typos and added new information (about the Parity multisig wallet hack) to demonstrate the value of formal verification. The edit also includes the addition of formal verification projects focused on Ethereum.
There was a problem hiding this comment.
@emmanuel-awosika This is something I am not well versed in, so I would love to get some more eyes on it, but overall I felt like this read well and made sense to read through.
Left just a couple small notes/adjustments, but overall 👍 from me =)
|
|
||
| Specifications are a collection of properties used to describe the intended behavior of a smart contract. Formal verification can prove that a contract behaves exactly as described in the specification. Unlike testing based on informal assumptions, formal verification provides mathematical proof of a smart contract's correctness. | ||
|
|
||
| Formal verification is critical for smart contracts because minor vulnerabilities can lead to massive losses. For example, the [Parity Multisig wallet hack](https://www.freecodecamp.org/news/a-hacker-stole-31m-of-ether-how-it-happened-and-what-it-means-for-ethereum-9e5dc29e33ce/amp/) was the result of an unintended function that allowed the hacker to override owner settings and drain the contract of up to $31 million in ETH. |
There was a problem hiding this comment.
Curious, would this have helped if the contract was formally verified?
There was a problem hiding this comment.
The consensus is that formal verification can help detect unintended code executions in smart contracts, so formal verification would probably have helped in the Parity case. More to the point, the Parity hack was mentioned in a couple of academic research and articles on formal verification, so I thought it'd be a good addition.
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
Co-authored-by: Paul Wackerow <[email protected]>
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
|
|
||
| Reliability is a highly desired quality of smart contracts, and both users and developers want assurances that a smart contract will work as intended. This is important because code in the [Ethereum Virtual Machine (EVM)](/developers/docs/evm/) is immutable, which rules out the possibility of fixing bugs or retrieving funds lost to malicious attacks. | ||
|
|
||
| Formal verification is one of the recommended techniques for [testing smart contracts](/developers/docs/smart-contracts/testing/) and improving [smart contract security](/developers/docs/smart-contracts/security/). Formal verification involves testing a program (a smart contract in this case) to ensure it behaves as expected during execution. |
There was a problem hiding this comment.
Formal verification involves testing a program
This part isn't really precise, since FV is not about testing. I would actually recommend removing this line completely, since line 16 below already introduces FV well.
There was a problem hiding this comment.
Thanks for pointing it out. I mixed up testing contracts (to check results) and evaluating contracts to see if they satisfy specific criteria (which is what I believe FV does). I'm working on rewriting certain page of the page to remove the inaccuracy.
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
|
|
||
| Formal verification can help determine the correctness of a contract's compiled bytecode. This requires creating bytecode-based, low-level specifications that define how a smart contract should behave in the EVM environment. | ||
|
|
||
| Low-level formal verification uses techniques like static analysis and fuzzing to ensure that contract bytecode satisfies all properties. This assures developers that the business logic specified in the source code is what will run in the context of the EVM. |
There was a problem hiding this comment.
This is not 100% precise. There are also several tools that apply symbolic execution and model checking to EVM verification, which are FV techniques.
There was a problem hiding this comment.
Yeah. I did a bit more research and found some more FV techniques (e.g., symbolic execution, model checking, and theorem proving), which are not mentioned in the page. I'll add those details while reworking the page, though.
|
|
||
| ### 1. Comprehensiveness {#comprehensiveness} | ||
|
|
||
| Formal verification uses automated tests, which can be run many times over. A formal verification assessment will likely cover the entire contract, reducing edge cases and hidden vulnerabilities. |
There was a problem hiding this comment.
Not precise, FV doesn't use tests. It mathematically abstracts the software behavior in a way that specialized procedures can guarantee correctness for every possible input case, without having to exhaustively go through each one of them.
There was a problem hiding this comment.
Just figured this out, too, after reading your comment and researching existing literature. I'll add this to the page while editing. Your comment may also be useful in highlighting the difference between FV and regular testing (i.e., that regular testing can only cover a small number of input cases).
Edits to rework the page.
|
Hey @leonardoalt and @corwintines, I made a couple of substantial changes to the page on formal verification for Ethereum contracts. Feedback on the new version would be great. Also, @leonardoalt, I tried to rework the tools section a bit; I'm not totally familiar with them, so if any inputs you have on how to structure that section is welcome. |
Edits to add new detail.
|
@leonardoalt, @corwintines; here are a couple more things I wanted to note:
Another suggestion for the above problem would be to create a section for theorem provers and place them together. Open to your thoughts on this.
|
I think they do belong in a different section, since they're not really specific tools used for smart contracts, but may be used for it too.
IMO it's fine to leave them there too. Although I don't find Manticore that useful for quick testing as Mythril/hevm/fuzzers. But that's just my personal opinion.
It could make sense to say it exists and point to this new page for details, without giving details there.
I think I wouldn't add them. It's just too broad to be able to do justice to all relevant papers, plus even in FV of smart contracts alone there's too many papers. |
|
|
||
| - [How Formal Verification of Smart Contracts Works](https://runtimeverification.com/blog/how-formal-verification-of-smart-contracts-works/) [How Formal Verification Can Ensure Flawless Smart Contracts](https://media.consensys.net/how-formal-verification-can-ensure-flawless-smart-contracts-cbda8ad99bd1) | ||
| - [An Overview of Formal Verification Projects in the Ethereum Ecosystem](https://github.com/leonardoalt/ethereum_formal_verification_overview) | ||
| - [An Introduction to Formal Verification of Ethereum Contracts](https://github.com/pirapira/Ethereum-Formal-Verification-Overview) |
There was a problem hiding this comment.
This repo hasn't been updated in 4 years, so might be a bit misleading.
| - [An Overview of Formal Verification Projects in the Ethereum Ecosystem](https://github.com/leonardoalt/ethereum_formal_verification_overview) | ||
| - [An Introduction to Formal Verification of Ethereum Contracts](https://github.com/pirapira/Ethereum-Formal-Verification-Overview) | ||
| - [SMTChecker and Formal Verification](https://docs.soliditylang.org/en/v0.8.15/smtchecker.html) | ||
|
|
There was a problem hiding this comment.
Maybe worth adding https://runtimeverification.com/blog/end-to-end-formal-verification-of-ethereum-2-0-deposit-smart-contract/ as well?
There was a problem hiding this comment.
Added this too.
| **Oyente** - *_Static analysis tool for analyzing vulnerabilities in EVM bytecode with symbolic execution._* | ||
|
|
||
| - [GitHub](https://github.com/melonproject/oyente) | ||
|
|
There was a problem hiding this comment.
I'd remove Oyente and Securify.
There was a problem hiding this comment.
Removed them now.
| **Harvey** - *_Harvey is an automated fuzzing tool useful for detecting property violations in smart contract code._* | ||
|
|
||
| - [Website](https://consensys.net/diligence/fuzzing/) | ||
|
|
There was a problem hiding this comment.
Echidna and Harvey are fuzzers, so maybe it'd make sense to have a fuzzers section even though this is an FV page? Or maybe move that to the testing page actually?
There was a problem hiding this comment.
That makes sense. I took them out now.
|
|
||
| - [GitHub](https://github.com/SRI-CSL/solidity) | ||
|
|
||
| **hevm** - *_hevm is a symbolic execution engine and equivalence checker for EVM bytecode._* |
There was a problem hiding this comment.
I think hevm fits the symbolic execution section better.
Edits to incorporate feedback.
|
Hi @leonardoalt. Based on your feedback, I made the following changes:
Let me know if there's any other change you want to see. |
|
Reminder that we should link to this page on the testing smart contracts page once this PR is ready. |
@emmanuel-awosika @minimalsm brought in this link |
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
src/content/developers/docs/smart-contracts/formal-verification/index.md
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
This looks great. Thanks, @emmanuel-awosika, great work! I left one nitpick that isn't a blocker. I pinged @leonardoalt to see if they want to do one last pass, but I approve this PR :)
…n/index.md Co-authored-by: Corwin Smith <[email protected]>
Oh, yeah, I'd forgotten @samajammin added the file to the docs nav. Thanks for adding it. |
Looks great! |
This page offers a high-level introduction to the concept of formal verification of Ethereum smart contracts.
Preview deploy:
https://ethereumorgwebsitedev01-emmanuelawosikaethereumor06662.gtsb.io/en/developers/docs/smart-contracts/formal-verification
Description
@samajammin asked for contributions to a new documentation page on formal verification for smart contracts, so I put together a high-level introduction on the topic. The guide explains what formal verification means, how it works, and tools developers can use to conduct formal verification for Ethereum smart contracts.
Related Issue
#6194