How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors
consensys.net
consensys.net
I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual banks don't seem to have these same requirements.
NOTE: Could be wrong on that last point, getting my information about banks third-hand, it's possible that banks are using formal verification. Can someone who works at a bank confirm?
I totally understand why blockchain isn't the standard for everything right now; my statement was in regards to formal methods to ensure correctness. For example, "reversing" a transaction could totally be modeled in TLA+ (and probably other systems, I'm just most familiar with TLA+ than most other systems), which would provide model checking (and possibly even proofs) that you would not otherwise have.
https://www.merriam-webster.com/dictionary/fait%20accompli
There's probably a better term but English isn't my first language.
It seems to me that having every bit of evidence on their end to prove that they are guaranteeing our transactions would be a really good thing....I suppose this solution might just work itself out if banks actually start relying on some kind blockchain to secure their transactions.
Its cheaper for everyone for them to say oops and give you the money back.
Its more expensive for you to sue than for them to be sued.
In fact you would immediately seek another job if you came from formal methods practice and then saw production code at just about any of the different animals called banks.
> [Coq, VST, CompCert]
> Formal methods: https://en.wikipedia.org/wiki/Formal_methods
> Formal specification: https://en.wikipedia.org/wiki/Formal_specification
> Implementation of formal specification: https://en.wikipedia.org/wiki/Anti-pattern#Software_engineer...
> Formal verification: https://en.wikipedia.org/wiki/Formal_verification
> From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 :
>> Which universities teach formal methods?
>> - q=formal+verification https://www.class-central.com/search?q=formal+verification
>> - q=formal+methods https://www.class-central.com/search?q=formal+methods
>> Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?
https://www.absint.com/compcert/structure.htm
A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify.
F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack.
https://github.com/project-everest/hacl-star
https://project-everest.github.io/
F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding
https://github.com/franziskuskiefer/evercrypt-rust
Also this F* stuff is all free software / open source, so it might become a very prevalent crypto and TLS stack
That said, TLA+ is written separately from the code. There could of course be bugs in the translation of TLA+ -> C...TLA+ is about checking the design itself, not the code.
I'm curious which static analysis tool you were using. I used to work in SPARK Ada and false positives were not really a thing due to how it worked. But I've heard of others that were much less restrictive which ended up with lots of false positives, or "maybe" cases that then wasted everyone's time. I can see how systems like that would put people right off using them.
See: Use of Formal Methods at Amazon Web Services
https://lamport.azurewebsites.net/tla/formal-methods-amazon....
> Proof-carrying data (PCD) enables a set of parties to carry out an indefinitely long distributed computation where every step along the way is accompanied by a proof of correctness. It generalizes incrementally verifiable computation
This has the potential to remove the element of trust that you currently must place in the provider of computation resources. With SNARKs you can simply ask them to include a proof that they actually performed the computation that is sublinear in the length of the proof and sublinear in the amount of time taken to verify the proof.
Of course this will always be more computationally expensive for the provider of the computation resources to both do the work and provide the proof.
From the paper:
> Dafny is a practical option for the verification of mission-critical smart contracts, and a possible avenue for adoption could be to extend the Dafny code generator engine to support Solidity … or to automatically translate Solidity into Dafny. We are currently evaluating these options
That seems like another point where a bug could creep in.
I wouldn't be surprised if there was a hard fork to save the deposit contract if there was a critical bug discovered.
Dafny Cheat Sheet: https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZ...
Looks like there's a Haskell-to-Dafny converter.
Some years ago, I had to work on a massively distributed system that scaled up or down with minimal communication between nodes, depending on the amount of work the system had. The developer of that scaling algorithm, a mathematician that gives quite a few software talks, and writes books teaching functional programming, wrote a proof for the system, guaranteeing its upper and lower bounds of performance. I was brought in because the system wasn't acting anywhere near those parameters: The worst part was that often it'd not downscale at all. The mathematician pointed at his proof, and therefore at the fact that if there was a problem, it must be a bug somewhere else.
So after learning how to read his proof, executing it, and doing all the typical ops stuff to identify what the system believed was going on at any particular time, it became clear that the proof had a significant flaw: It believed that the amount of work that the system received was perfect information, with no latency. Since the real world has latency, and none of that was accounted for, the proof was guaranteeing success in a universe that is different from ours. Once I modified the model to represent the real information quality, the outcomes were pretty close to what we were seeing in reality, and equally unacceptable.
So proofs are powerful, and maybe there are zero issues in the proof of this smart contract, but formal models and proofs can still fail you, they'll just fail far less often than your typical system made with unit tests and chewing gum.
I’m sure it strengthens the codebase being verified. But there is a reason systems engineering of involves both verification and validation.
Proving things correct is much harder than finding counter-examples that they aren't correct. But the methods do work. Their based on sound formal logic. Proofs can have mistakes, certainly, but it's a darn strong signal that their system is correct.
If somebody told me that they had a financial system whose security was based on applying the Pythagorean Theorem to physical triangles, it would raise exactly the same red flags—the theorem itself isn't a question, but it doesn't even try to capture how physical materials might be imperfect or change over time, and those are exactly the sort of inconsistencies a motivated attacker could exploit.
Another way of phrasing it is that the law of leaky abstractions means that though the code itself might be 100% correct, lower levels can puncture the assumptions and make that correctness moot - IE, unsinkable titanic vibes
And also, as a long time observer of software correctness proof fails, I'm getting the old popcorn popper ready for the first instance where there's a bug and then we'll have explained to us that, well actually, the prover wasn't covering that case...
What happened?
But more likely we will see developments of security and proofs in languages like cairo, to be used on zkrollups, where we will also see alternative VMs to the EVM. So there will be lots of options with different tradeoffs between composability/security/efficiency/redundancy.
ETH2’s EVM replacement, EWASM, will use WebAssembly, so developers should be able to use saner programming languages than Solidity.
This sounds pretty rad!
Thanks!
I’m wondering how Cardano’s Haskell-based Plutus platform will compare in practice, now that they’re rolling out smart contracts as well. I’m guessing they’re going to have significant adoption issues.
The EVM on the other hand is harder to justify. :)
Why did they stop going in that direction?
The EVM is tailor-made to accurately account for the expense of executing programs in a distributed environment. It has a highly heterogeneous addressing scheme. Every opcode has execution cost metering that has been refined over time. Each word is 256 bits to make 256-bit cryptographic operations easier. There's significant tooling around the EVM for writing and analyzing smart contracts. Other EVM-based blockchains would need to migrate in parallel. The skillset of "blockchain application developer" has coalesced around Solidity and the EVM.
Bottom line is that although WASM offers compatibility with non-blockchain tooling, the blockchain-specific needs of Ethereum are so much better served by the EVM that migrating is difficult.
Alot of the WASM experimentation has also included changes around how storage is charged. Specifically NEAR does a deposit system where you have to HODL to store data on chain. That allows them to innovate in the runtime and cost structure and still incentivize blockchain nodes.
So it's not entirely gas accounting for computation, its more pricing for storage that probably keeps eth on EVM indefinitely.
Other experimental chains are must more likely to become robust and trusted and more performant and then eclipse ethereum.
In what sense?
Allowing the global transaction limit to be raised will decrease the competition for blockchain space and massively decrease transaction fees.
There are also other standards being worked on to allow transactions to be made in a way that they don't have to be broadcast to all nodes, which will also allow their transactions to have much cheaper fees. These systems are being developed simultaneously by unaffiliated developers in userspace ("layer 2") rather than by the core Ethereum developers who are working on proof-of-stake and sharding. These systems generally come with their own sets of trade-offs (including what kinds of smart contracts they support and how smoothly they interoperate with outside systems) so they don't completely replace the need for sharding being done by the core developers. ZK rollups and optimistic rollups are some of the main kinds of layer 2 scaling solutions being worked on now.
You shouldn't just check against a definition Y. Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties. It's generally much easier to specify such properties than to write code implementing them, compare for instance an "is_sorted" function to an efficient "sort" function, so it's not just the same code written in a different language.
The issue is that how do you know you have the correct set of properties that a contract must hold? You might think you have all the properties that you need, but realize later that you missed one that is critical for your desired outcome.
This still dramatically raises the bar. EVM has a variety of very fun footguns and formal verification can help you dodge lots of these.
Solidity is much closer to being C's mentally challenged grandchild than is to javascript.
you might have an uninsured contract with multiple audits and proofs of correctness, vs an insured contract with one quick review. which one would you put money into?
Thus, eth contracts can be enforced by civil courts too, if there is some chicanery going on...
For keeps, no takebacks, no do-overs…
From the wiki page you reference for example:
> The reasoning is that a party should not be held to a contract that they were not even aware existed.
And later on, something directly relevant to this discussion perhaps:
> Mutual assent is vitiated by actions such as fraud, undue influence, duress, mutual mistake, or misrepresentation.
I think that this discussion is more closely related to the legal concept of a Mistake [0], which absolutely can be something that a court might address. Though even that doesn't seem like quite a perfect fit here.
[0] https://en.m.wikipedia.org/wiki/Mistake_(contract_law)#Mutua...
In so far as it relates to Eth, my point was that the meeting of the minds only goes as far as "the code is the contract", and the use case is to eliminate the civil courts combing over intent and who knew what.
Oh wait
A contract call that would misbehave is guaranteed to halt: not by itself, but by the EVM, which, when the contract call eventually runs out of gas, shall take care of halting it.
It's pretty nice I'd say.
In fact you can't really get away from the need for a clear formal description of what the contract does anyway. If you write it in a more flexible language but only accept it with a proof of some formal properties then those formal properties are in effect the contract.
At which point we reach something I still don't quite understand. If people accept code satisfying those formal properties as 'proven correct', then why aren't the contracts written as those formal properties in the first place?
How are you going to enforce the contract? If it's formally verified, the contract is enforced by itself.
Not to mention, I think as a developer accepting a spec that isn't verified is a tough pill to swallow, because any bug no matter the size would mean that you're breaking the contract.
> In fact you can't really get away from the need for a clear formal description of what the contract does anyway.
The code is its own description. The point is verification: does the code implement the contract?
To prove non-trivial things, you need more sophisticated types that make interesting assertions about their values, where it’s not immediately obvious how to construct a value of that type. Special proof languages are used for this.
Formal verification btw is just a formalised methodology for evaluating something against a specification. It doesn’t prove that errors don’t exist, or that the verifier hasn’t managed to independently make their own error. It’s just a rigorous PR.
How would CertiK sell their token otherwise? :p
A state rollback would be extremely disappointing to me, even though that much Eth in the hands of one party would undermine the security of Eth2 (which is why the other state rollback occurred)
This proof is impressive, but doesnt change anything for me whether it is bulletproof or not
I still don't believe this migration is going to happen at all. If you look at the PoS blocks from other EVM chains, you see that reorgs happen way too often to be comfortable with $100B of assets.