Hacker News Reader

Comment by josh2600 | Hacker News Reader

Cryptography has mathematical proofs of the underlying math that are rigorous. There are constraints such as breaking if a proof of an attack against the discrete log were to emerge or other constraints related to p=np.

The implementations are also very close to formally verified if not fully formally verified.

Nothing is perfect but cryptographic code has to be pretty bulletproof or a lot of systems would get owned. The descriptions of how to verify cryptographic systems are academically and professionally rigorous especially compared to eth.

Caveat: sometimes the underlying systems that cryptographic implementations utilize change degrading their guarantees. There have been times where the compiler will get updated and cause what was a branchless process to branch which could lead to information leaks against a dedicated attacker. Thankfully such examples are rare in the literature.

View on HN

> The implementations are also very close to formally verified if not fully formally verified.

So is Eth2, see "Formal Verification of the Ethereum 2.0 Beacon Chain" by Franck Cassez, Joanne Fuller, Aditya Asgaonkar, paper (https://arxiv.org/abs/2110.12909) and source code (https://github.com/ConsenSys/eth2.0-dafny). More efforts to formally verify Eth2 is ongoing as well, by different entities.

> Nothing is perfect but cryptographic code has to be pretty bulletproof or a lot of systems would get owned

Same with Ethereum. The chance of having a major impact with a vulnerability is even higher I'd argue, as you can easily extract currency you can trade for USD, and the entire network is inter-connected, so finding targets to exploit becomes even easier.

Point still stands that cryptography goes over a lot of peoples head, but you don't hear those people complaining that because they don't understand it, no one does.

I mean, I think this really depends on how you define ethereum. I think we all agree that there hasn’t been an effective attack against the consensus mechanism in a while (we could argue the original dao was sort of a successful attack against all of eth due to the hard fork).

This is kinda where I’ve gotten to on this: consensus is pretty much safe. Smart contracting is very hard to do safely.

This is not unlike the guarantees in general computation. The metal is pretty safe. The further you get away from the metal, the more layers of abstraction you’re relying on functioning predictably.

To be clear, I’m not arguing with you and appreciate your point about formal verification of eth.

I respectfully disagree. While some cryptographic primitives are surely based on some sound math, building cryptographic systems is very hard, and when built, they ane not generally proven to be correct. Some attacks involve influencing source of randomness, whereas proofs simply assume random unguessable numbers, for example. You correctly mention unintended degradation, that is another pretty serious concern, but even when built first, most systems are incorrect, faulty and unsafe.

Proving systems to be correct in computer science is far from settled matter.

I would say that it really depends on how you think about "the system."

If the hardware is in-scope for the system, you're generally out of luck at having provable guarantees unless you're willing to operate a foundry and courier your own products.

I think it comes down to threat modeling. You have some threshold where it's unreasonable for someone to attack a system for less than $X spend. Right now on iOS I think that's on the order of $500k-$1m usd.

Reply on news.ycombinator.com