[deleted]
SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
561–570 of 577 posts
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#562Earlier quoted context omitted.
Formal methods are about matching the spec. Errors in the spec are still an issue. Moreover, there is very, very little formally verified code in the world, much less than you'd believe. My former professor (RIP) oversaw the formal verification of the F-16 computer software and it still had significant bugs in the end where the specification itself was incomplete or in error. And that was a multi-year, team-scale eff…
A nice practical example from TLS 1.3: TLS 1.3 has been formally proven (not an implementation, but the standard itself). To the extent the mathematicians correctly explained what the TLS 1.3 RFC says, and correctly told the machine what TLS 1.3 is supposed to do, the machine proof says this protocol does what we intended. That work assumes a bunch of components are black boxes, they must work. If we ever lose confid…
Keep in mind:
1. a non-verified approach can have many problems in the (informal) specification + implementation errors
2. the verified approach is likely to have less specification errors (because the specification had to be formally written out and matched against an implementation) and implementation errors with respect to the specification will be almost impossible (minus faults in the compiler, OS and hardware).
There's a huge jump in security guarantees between 1 and 2.
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#563The fact that this is trending on HN shows how little hacker news knows about the cryptocurrency space. A relatively unknown, recently launched stablecoin collapsing is not big news in crypto. Now if dai, usdc or usdt had failed, that would be a big deal.
[deleted]
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#564Earlier quoted context omitted.
The Simplicity language is good. I’m sure there are other designs.
Ok I did a really shallow search of the smart contract space and it looks like the trend is towards creating simple languages that are easy to reason about and formalize their semantics. Simplicity seems to be the best example of this. With such a language you can write proofs about the behavior of the runtime using some proof checker and then programs in it should be simple enough to reason about in a rigorous way.…
I think in most cases you wouldn’t want something like idris as a smart contract language on any kind of cryptographic system (blockchain, ZKP system, whatever) because idris programs are expensive to typecheck and evaluate. It would be reasonable to construct a DSL or something in idris that compiles a compact, easily computable language though.
The idea about having proofs as values in smart contracts is interesting though. I could see a few neat applications of that.
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#565Earlier quoted context omitted.
The inverse of "any contract that has been hacked was insecure" is "any contract that hasn't been hacked must be secure". I think this is what OP meant. If something has been around for a long time it does probably mean it's less likely there is a really obvious security flaw, but it doesn't necessarily mean it is 'rock-solid' as plenty of things that have been seen to be 'rock-solid' in the past have turned out to b…
yes this is what I was implying. I am curious how else the previous commenter would interpret my statement.
Let's formalize this to make it easier to discuss.
𝐏(𝐀) = 𝐏(contract has been hacked)
𝐏(¬𝐀) = 𝐏(contract has not been hacked)
𝐏(𝐁) = 𝐏(contract is hack resistant)
𝐏(𝐁|¬𝐀) =
𝐏(contract is hack-resistant given that it has not been hacked)
𝐏(¬𝐀|𝐁) =
𝐏(contract has not been hacked given that it is hack-resistant)
> The probability that a contract is hack-resistant, given that it has not been hacked, is approximately equal to the probability that it has not been hacked, given that it's hack resistant.
More succinctly:
𝐏(𝐁|¬𝐀) ≅ 𝐏(¬𝐀|𝐁)
¬(¬𝐀 → 𝐁)
𝐏(𝐁|¬𝐀) ≅ 𝐏(¬𝐀|𝐁) => the fallacy of the inverse
and
¬(¬𝐀 → 𝐁) => statement in comment
Note that the first statement is a comparison of probabilities, and the second is not. They're not the same. There might be another fallacy at play here, but it's not the fallacy of the inverse.
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#566Earlier quoted context omitted.
Ok I did a really shallow search of the smart contract space and it looks like the trend is towards creating simple languages that are easy to reason about and formalize their semantics. Simplicity seems to be the best example of this. With such a language you can write proofs about the behavior of the runtime using some proof checker and then programs in it should be simple enough to reason about in a rigorous way.…
I think in most cases you wouldn’t want something like idris as a smart contract language on any kind of cryptographic system (blockchain, ZKP system, whatever) because idris programs are expensive to typecheck and evaluate. It would be reasonable to construct a DSL or something in idris that compiles a compact, easily computable language though. The idea about having proofs as values in smart contracts is interestin…
Yeah I agree that Idris itself would be much too large, however you could write a much smaller Lambda Pi that could still enable a lot of nice features.
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#567Earlier quoted context omitted.
When I think about it in those terms... Why not fund bug bounties that way?
Because you presumably want to find bugs in applications that are not smart contracts.
No. I was specifically referring to finding bugs in smart contracts. Stand up a network and have a "bounty" that would attract attempts.
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#568Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#569Earlier quoted context omitted.
> A relatively unknown, recently launched stablecoin collapsing is not big news in crypto. The fact that some people think a $250,000 heist followed by the collapse of a half a million dollar stablecoin is "not news" underscores how ridiculous the cryptocurrency space is right now.
250k is nothing compared to the biggest defi losses: https://rekt.news/leaderboard/
From the link
>These protocols are listed with respect; we appreciate and understand the work that lies behind each name.
Title of leaderboard, REKT.
Re: SafeDollar ‘stablecoin’ drops to $0 following DeFi exploit on Polygon
#570Earlier quoted context omitted.
This just isn't correct. Public ledger cryptocurrencies are able to be digitally transferred without any form of personal identification, unlike almost any other form of payment. Just because the ledger is public does not mean that one's identity is public, merely the addresses involved in the transaction are public. If there is nothing tying one's identity to an address or transaction, then the transaction being pub…
I agree with you. But I think there is nuance. When I hear “crypto is good for crime” I hear “crypto is good for all criminals” (where “criminal” is anyone conducting an illegal $$ transaction). In your process, my statement was 100% talking about the “customer” steps. You’re right. But, at scale, it’s hard to conduct any crime that doesn’t leave a record. At the many millions of dollars of revenue scale, I could see…
Hiya, sorry for a little bit of a late response!
I think there are a couple fundamental misunderstandings here regarding cash. Answering this question may fix that a little bit:
> I’d be hard pressed to acquire Bitcoin in a way that didn’t associate the wallet with my identity (if you have methods, please share!)
If one purchases BTC on Coinbase, trades it for XMR, and then trades the XMR for BTC back to a separate BTC wallet, it is currently unfeasible to determine that the final BTC is linked to the initial BTC. Also, cash is not completely private- bills have serial numbers that are tracked in a similar way as to how one might track Bitcoin (unless you're dealing solely in coins). BTC and XMR are both able to be cashed out fairly easily as well. They could be legally sold, given that they're functionally untraceable. You can also fairly easily coordinate cash overnighted to a PO box set up with a fake identity.
Re: Private ledger cryptocurrencies
With Monero (for example), the sender, receiver, and transaction amount are all private. The quality of Monero's privacy is up for debate, but I see no reason why explicitly tracked cash bills are more secure than a private ledger cryptocurrency.
In conclusion, within the initial context of, "When I’m doing crime, I strongly prefer there to be no record of the transaction", I don't believe that there is an opsec-based reason for you to choose cash over cryptocurrencies. There is always going to be a risk when committing crimes- that is unavoidable. Maybe this is a big point for dealing in gold, haha?