Analyzing The Security Of Casper by Ryuya Nakamura (Devcon5)
Devcon·Fri, Oct 9, 2020, 12:00 AM
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more. https://archive.devcon.org/archive/watch/5/analyzing-the-security-of-casper From the beginning of this year, we have been working on the security analysis of Casper FFG/CBC, resulting in findings of attacks and formal proofs of properties. In this talk, I'll share a few tips towards the secure development of cryptoeconomic protocols, as well as our research on Casper. Speaker(s): Ryuya Nakamura Skill level: Intermediate Track: Security Keywords: Casper, ETH2.0, formal verification, FFG/CBC, Technical Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum Learn more about devcon: https://www.devcon.org/ Learn more about ethereum: https://ethereum.org/ Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019. Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
Transcript
Andrea from Leia x-ray X is a Brockton startup based on Tokyo and working on Casper research and its positive power its own Foundation grant so today I will talk about my research on the security of Casper so you know Casper what consensus protocol has two property safety and aliveness so the talk is divided into two parts and safety part and the Lebanese border so first I want to introduce Casper is not that different from traditional protocols and Casper FFG and the shippi she is not that different also so first pbft tender mint and Casper Fuji and Shiva are all categorized into a synchronous resaved consensus protocol so I mean safety does not require any timing assumptions so basically in these protocols minority comes when sufficient number of our data's is locked on a block so let's start with his tender meat so in tandem int a Brock is called notarized when to F plus one birthday that is brought on the block so here F is with an chain for treasure and the Brock is finalized when it's directed child Brock is notarized and then when birth data its bottle for notarized block that VAR data is locked on a Brock so he cannot vote for a conflicting Brock so in this case the past Brock is finalized and here the boards must be collected in own chain this is very important point so here the reason why we can say the post Brock is finalized is we know that these validated vote for the second Brock knows we know that this value tie is locked because we know that the posts are on chain right this is why on sham voting is very important for this bro what it's protocols the reason why minority comes around only when it's direct Brock it's it's notarized there might be some another drop in the middle and you know we discussed locking is necessary for safety but you know if locking is too much too much strong does not create some liveness property so here we have some unlocking condition so in tandem ain't a validator locked on the brock is unlocked when he see a higher notarized Brock so in his picture I was taught to but I'm unlocked because I see that new notarized abroad clear so let's start with the next is Casper a refugee the cash point of G is fundamentally similar to tandem it but it's more like chain based leader s tandem it so in Casper refugee we don't use not finalized block we finalize checkpoints so in this picture we have Brock chained but we finalized on say every 50 blocks or every fifty strötzbach right so yeah and again foods a steer on chain the difference between tandem it is the fork choice itself is doing the similar role of leader so in tandem ain't everybody that bought for Brock which decided to buy the leader of that round but in class by 50 G it's a folk choice that decides of you and unlocking and locking it's super similar to tender meat so in every case they are unlocked when they see higher notarized what just justify the checkpoint so finally she Misha Casper is also locking abased consider protocol but the log king and the unlocking is purely by the fortress itself so in shabby chic as per every message boats rock must follow the folk choice and in tandem int or FFG we included supports on chain but in Shiva she weeken the same thing but more for x-ray we can allow the message to point to the every all front boats were broke so in this picture the block P is pointing to open block but the reason is um okay so yeah additional explanation so in this case this proc is invalid because they know that the different chain is more heavier so this is inverted and unlocking condition it's super obstructed into equivocation condition that every vote must include is the previous message in its message so in this picture this block is invalid because he has previous message here but is not including on chain in message so the similarity of she be she and FFG is that the boss is chain based so every vote Brock is voting was supporting for the same ancestor right so in FFG what 2.0 they include all from boats in own shame because they are supporting for the same checkpoints this is also same force revision Kasper but it's more flexible way so exact finality condition is something like I do not do not talk in this talk but we finally finished our formal education in elaboration it more than half a year but you know it's great job I think so yeah pretty much summary is ten demand cashback refugee and ceviche is based basically based on some locking idea and you know the difference comes from where the locking is based on the notarized checkpoint of rock or folk choice itself so to me I want to move to ravenous but ravenous has a lot of design strategies so I do not cannot talk in this 20 minutes so today I want to focus on 2.0 ravenous so basically in 2.0 Lebanon strategy is super simple it's just a remedy ghost press just by refugee so remedy ghost is a variant of ghost in which where the latest message is only counted so in this picture the traditional longest chain rule this chain that is ahead in normal ghost this chain is head-butting aromatic ghost we only count the latest message so the the third chain is ahead so to talk about the liveness based on our MD goals we need to define when the chain converges and in a remedy ghost a block is not opened when the chain is supported by modern majority of honest supports so in this example say says 100 total bar details and the brew chain is supported by more than 51 votes in this case whatever the what I do the top chain does not orbit reorganised so this is a convergence condition of aromatic ghost but it cannot be observed by you know protocol boring part data's this is why we want Casper to detect finality but for revenue analysis this is the convergence condition yeah so before I introduce attack on elementary ghosts I want to introduce some very nice property on folk trees so in basically in any constant protocol we want some property called fairness so I mean any player cannot increase the power against the stake or hash power but the something break this property called saving strategy so the bursary can skip their votes and the later use their votes to free prop this not work in the longest chain because so say we divided into climbing the slots six-second the ten seconds and every three block were vote is but otherwise for the battery and in this case adversary with horde was save every block but in longest chain we can add some validity conditions that every block wall vote cannot extend the future rock so here after some network failure they cannot use the save the board to prevent the revenues here but in ghost every vote does not expired so here there is a huge to fog from rock from early days and but you can use the save save the bro save the boat in ghost using ghost the fog choice is based on every per student election on each height so every word has not expired so this turns into creating a new attack on a remedy ghost which I call decoy flip flop attack so basically what I want to do is to flip every roads into another chain and go back to another chain and continue the friends the big difference in normal ghosts and error Emily ghost is the flip of volts decreases the score in longest chain what normal ghost some squirrel chain monotonically increasing and every Raven is proof is based on that property but in a remedy ghost you cannot have that property this is the situation I have so imagine that to chain that chain brew chain and we continuously flip-flop just before the chain converges and the desert is the necessary saving which that the battery needs to prepare exponential disgraces against the adversary power and for some parameter 33% attacker can prevent ripeness for 100 epic it's like a few hours or 10 hours by 5 epochs of savings now for more big adversary it takes much longer to the chain for the chain wineries yeah small might occasion of this attack is FMOD ghost it's a variant of a remedy ghost to mitigating saving strategy so in aromatic ghost we count every vote every old abroad if it is greatest but in affinity ghost we only count a vote from the current epoch was a previous block someone say that it's kind of introduce a new synchronous function on consensus but it's not that true because in 2.0 case the effigy is decoupled from the chain so the synchronous sumption does not change but here still the coil flip-flop is possible because we can have one epoch of savings so this starts a pretty much a new question that why a remedy goes in the first place compared to non aromatic parental ghosts especially there's no sheepish Casper in 2.
0 for now so it's a bit easy to manipulate the factories the another interesting topic which I don't cannot talk today is flip-flopping a remedy ghost in sheepish Casper it was in sheepish Casper every message is imposed to follow the folk choice so the analysis gets a bit complicated but basically it's mighty gated free flow of strategy so a bit not incentives so you might say savings can be detected and rushed but basically to punish driving this failure is as I explained in the bicep italic in this morning is defined a difficult to distinguish between no malicious failure because it just might honest no just get down so in 2.0 has some incentive mechanism to punish driving this failure called in activity link but it's just kind mild punishment so the current parameterization with develop robotic 33% attacker attacker can prevent finality for a few days with 1% cost of the stake and you know ravenous attack sometimes has a lot of the world because there's a layer two solutions in which they had some challenge period and if they can not if they can sense a shape on the fraud proof in plasma and writing otherwise so you can get a bunch of money from the layer two construction so I think it's a new question to how to nourish this incentive compatibility enlivens failure so I think I have a time so I quickly introduced some attack on class by refugee which is funded by last year so in FFG so originally effigy removing the leader in kinds of bad way because so these squares are not rocks it's checkpoints and remember that unlocking lure in Casper effigy is observation of high year notarized checkpoint and so in this case imagine that 104 letters and this checkpoint it's close to two swords that is not notarized yet but the bursary can justify this checkpoint arbitrary any time so in this situation the folk choice favors this side of a chain so creating a new checkpoint which is close to the notarization but exactly the same that at the time at the grocery flip the head of the folk choice that in that way and in high synchrony Network other words so you can continue this attack whoever so why this does not happen in tandem and it's simply because leader decides the view of the current around so what we should do is to have some sort of thickness property in effigy so there's a lot of construction to prevent this attack it's one idea is to not allow the change was a view in the middle of the epoch for example we do not allow any new justified checkpoint if it's in the middle of the epoch yes I think it's finish thank you
Automatic transcript — names and jargon may be misspelled.