News for hackers. Stuff that matters.

A comment on How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors.

Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by pidge on Monday September 13, 2021 @11:13AM (#28512490)
To clarify, they implemented the algorithm in Dafny, and then proved that version correct. They did not verify code that will actually run in production.

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

[ Parent | on HN ]
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by X6S1x6Okd1st on Monday September 13, 2021 @12:04PM (#28513172)
Additionally it's proving a translation of the algorithm implemented in solidity. Solidity is not what is run on Ethereum, EVM bytecode is. Solidity is compiled down to EVM bytecode and that's what is run.

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.

[ Parent | on HN ]
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by yissp on Monday September 13, 2021 @03:21PM (#28515593)
I mean if there was a critical bug in the solidity compiler itself that would put the correctness of pretty much every contract into question, right? It seems like a fork would be hard to argue against in that case.
[ Parent | on HN ]
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by latchkey on Monday September 13, 2021 @12:15PM (#28513294)
There will be many hard forks before the funds from the deposit contract can be retrieved.
[ Parent | on HN ]
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by X6S1x6Okd1st on Monday September 13, 2021 @12:18PM (#28513339)
Fair enough, non-contentious hard forks in Ethereum are usually called upgrades at this point.
[ Parent | on HN ]
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by ilammy on Monday September 13, 2021 @12:20PM (#28513367)
“Beware of bugs in the above code; I have only proved it correct, not tried it.” — D.E.K.
[ Parent | on HN ]
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by westurner on Monday September 13, 2021 @01:12PM (#28513982)
https://github.com/dafny-lang/dafny

Dafny Cheat Sheet: https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZ...

Looks like there's a Haskell-to-Dafny converter.

[ Parent | on HN ]