Perun: Virtual Payment and State Channel Networks (Devcon4)

okay so thanks a lot and I'm also very excited to be here at Def Con I never was was here although I had several times watch the videos off of James Otis area so so this talk will be about Tarun our work it's like a joint research project between the Technical University of Darmstadt in Germany and the University of Warsaw in Poland in several of my co-authors so this is some kind of academic work so we published some papers at some top conferences in security and several of them also here sitting there over there and here in the front row so we are very happy to answer questions later also okay so as we have seen already today several talks there are many exciting projects currently going on people like do a lot of research and also development in building different types of state channel and payment channel networks so I would like to explain to you basically at a high level what we do in karoon so in Peru essentially the goal is similar to the previous two talks of Moore and Liam we are trying to build generalized state channel networks and I will talk in a moment a bit in more detail what we understand about general state channel networks the main technique that we developed in our work and I'm kind of happy that nobody so far talked so much about this is about virtual Channel so some people also call it meta channels and I will explain in more detail what actually are virtual channels and what are the advantages of these virtual channels and the special feature and maybe this is also one distinctive feature of our project because we have like a very strong background in cryptographic research we focus a lot also on not only designing these protocols at an abstract level but also proving the security of these protocols okay so we usually when we come up with a design of what the protocol is specification of the protocol what it what it what it is then we also usually carry out a formal security proof that it satisfies certain security guarantees so what is the state channel network I will essentially show you our view at the rune of what this is the basic ingredient and you have already seen this in several other talks we call them legislators and let us state channels they are built directly over the ledger okay so that's why they call legislate channels so we have these two parties Alice and Bob and they want for example to execute some contract off chain for example it could be some chess game or some other online game or a payment or whatever and the letter state channel then works in three phases so in the first phase the party's Alice and Bob they have to go to the blockchain and create this legislature and help this is happening with some kind of cryptography like signatures are exchanged and so on and then at the end parties Alice and Bob don't have a pointer here Alice and Bob they can like go to the send something to the blockchain and deploy some channel contract which is later on going to be used potentially if there are some disagreements between the parties so once the letter state channel has been deployed so it's established the parties can then like execute contracts of chain so this is the whole purpose of course so they can like for example run multiple execution of a chess game without ever touching the blockchain and s like Liam mentioned earlier so we also support like this generalized state channels where you can not only run a chess contract but you could run several chess contracts or like even completely other games also in this in this in this legislature and the main point here is that as you can see that this execution of contracts so this update of the state this is carried out of jail so it's carried out without Alice and Bob needing to interact with the blockchain so then at some point when Alice and Bob they don't want to use anymore this legislature state channel then they can settle this channel and go to the blockchain close it and this again requires unchain communication okay so this is essentially the three phases of a basic state now we would like to extend this to forming a network so this is the most simple network that you can think of you have like LS ingress and Bob Ellis is connected to Ingrid by a letter state channel and Ingrid is connected to both via a letter State Channel and now what Ellis wants to do is she wants to execute off chain a contract with Bob okay so how can she do this there are several options to achieve this the first option would be of course we just have seen like legislate channels so we could just use this okay so we could just create a new letter state channel between Alice and Bob but this of course has some disadvantages because as you saw like creating a channel let us say channel this requires interaction with the blockchain so I need to communicate to the ledger deploy it as contracts this is slow so it takes some time it is also expensive because like deploying a contract takes cost a lot of fees so you would like to avoid this so another option is because we have these two channels between LS English and English and Bob we could use this existing infrastructure to let Alice and Bob directly execute contracts between them by using these two underlying legislators okay so and this is of course the advantage that this can be fast if we manage to design such a protocol can be fast it can also be cheap because it does not require any communication with the underlying ledger and this is essentially what we do in Peru so we developed a technique that we call virtual channels and the main idea is you can think of these underlying let's just state channels as like a two-party blockchain okay so let's just state channels between Alice and Ingrid and the letter state channel between Ingrid and Bob they offer you something similar to what the blockchain offers you so how can we now create a virtual state Channel so essentially also this works in three phases in the first phase in the creation of the legislature now we run a protocol between Ellis Ingrid and Bob now there are three parties involved okay Ingrid kind of takes the role of the blockchain to some extent and this is object so the communication between the the parties is going on like off chain without touching the blockchain so it can also be very fast of course and then you can compare this to let's just state channels they're the creation was on chain so it took potentially a lot of time now executing executing is very similar to let us say what happens in letter state channel so Alice and Bob they can now execute multiple contracts of chain so also here we can allow contracts several contracts potentially to be executed off chain and finally when Alice and Bob they don't want to use anymore dead Channel then they can close it by again not going to the to the blockchain not going to the ledger but going to the underlying legislature okay again this has the advantage that all of this year as you can see all of this create execute and close all of this happens off chain without interaction with the ledger which is in contrast to the legend state channels now this is very nice but we of course would like to consider to also capture exception more complicated networks so like here we have much more complicated network like little more complicated Network and we want for example that Ellis wants to talk to Dave okay so how can they do this you can just apply this technique that I just thought I told you about recursively so we could let Ellis first create a virtual state channel with Bob then over the virtual state channel between Alice and Bob Ellis can now create another virtual state channel was clear and then this can be continuing like this until finally Ellis has it has reached Dave and then they can execute in this final channels they can execute their contracts of chain so what are the advantages of channel visualizations there are several of them that I would like to highlight first of all this is low costs so since the intermediary is not involved anymore in the execution of the the contract similar to the later state channel where the blockchain is not involved in the execution of the contract this can be very fast and it can also be cheap so there in particular the intermediary does not necessarily need to ask for fees we also have better privacy so because the intermediary does not know what happens in the letter individual state Channel Alice and Bob can keep the state updates private and tears of course the other advantage there is no availability required so even if Ingrid goes offline for a while then Alice and Bob can still continue playing chess which is of course a nice feature so now you have seen a basic idea of how we construct generalized state channels now or like what are actually general stations you would like of course to know how you can construct them unfortunately I cannot explain in detail how this works now because it will take quite a lot of time and we can I would refer liked to refer you to our papers which are on the webpage it was mentioned on the first slide the one thing that I want to explain to you is what happens in the case of corruption so corruption makes as we all know our life more difficult and this is also why designing such protocols gets quite complex so we have the first case the first example that I would like to look at with you is now the following so we have Ellis Ingrid Bob and clear and Ellis wants to play chess was clear so Ellis can open a virtual state channel between Ellis and clear by using this recursive approach that I just explained and then she can open a chess contract and maybe in this chess contract she did some several moves okay she played very smartly and at the end she is in state n minus one and there is only one state left substitue finally wins the game ok so this has to submit to execute to the next state and then she will win but now of course clear and potentially all the other parties they don't have any interest in this ok so they tend to interrupt and try to prevent this they disappear like just in this example that mu short on this slide they disappear and then we still have to finish finalize this execution because we want to have a secure protocol so how can this work at the very high level of course it gets very technique because of their many Sitecore aside cases that we have to do is essentially Ellis first tries to execute the contract in the underlying virtual channel between Bob if this also fails because in my example Bob is also corrupt and essentially everybody can be the protocols have to work even if all parties are corrupt except for this single party and if this also fails then she goes to the next underlying legislation on here she tries to execute to the next state in this and then finally if also England as corrupt she goes to the to the underlying ledger okay and of course we trust a serum we trust vitalik so we will get eventually we get eventually the execution time okay so this is the first example that I would like to look in so now let's look into the next example how can we deal with the corruption case when Alice and Bob are corrupted and they try to cheat Ingrid and try to steal her money so they want to steal some is from from her and this is like a kind of can be a difficult case so for example consider the following situation we have a again a virtual led a virtual state channel between Alice and Bob and we are having a rerun a contract and this contract has the following property that if state n minus 1 is set by n minus 1 it pays 5 is to Bob and in state n it pays 5 is to Alice ok so now what Alice and Bob can do to try to cheat Ingrid for her money they could try to submit in the underlying legislation Al's because I said this underlying legislation else take the role of the blockchain the accept MIT in these underlying lesson state channels these conflicting states and this would result in the following situation if you don't design a carefully develop protocol then it would result in the situation that LS the corrupted LS wins five coins to corrupt the Bob who wins five coins but Ingrid who just who's just played the role of the intermediary she was not even involved in this contract she loses 10 coins okay so this is something that we want to prevent and we can do this by using the by developing a carefully designed called in particular using timings or carefully chosen timings to deal with these special cases unfortunately this is like very simple cases only and it gets much more complicated in our situation so we have this complicated Network and now we want to handle also full concurrent protocol execution so many things can happen in parallel packets can open contracts in parallel for example here this middle party here she is involved in two virtual state channels and she runs possibly several contracts and them in parallel and they can also be many corrupted parties and of course we want to deal with this situation okay so we want to design protocol that even is secure when there are so many corrupted parties when so many things happen in parallel when these all these messages are exchanged and the protocol should guarantee security the security requirements that we specified so how can we design such a complex protocol and for this we rely on what is essentially the approach of modern cryptography which uses what I mentioned the beginning security proves to kind of design the protocol using a sound methodology so this approach of modern cryptography which we use essentially for designing cryptographic protocols like whatever encryption schemes are more complicated schemes it works like this that you first specify what is your security definition so you what do you want that the protocol actually should achieve then we design the protocol so we come up with a candidate scheme that hopefully achieves the security definition and once we have done this then we prove its security okay so at the point so okay we prove its security so at the point then of course this process is not like so nice as I showed to you here okay it's like iterative way so we sometimes you come up with the candidate scheme we find some problem in this candidate scheme so when we try to prove it so the proof course fails okay so that's the nice thing about it it's gives you a sound methodology so to say so the proof fails we have to adjust the protocol and then we try to again prove it we fail we try to again prove so we could try to adjust it we try to again food and so on and so forth at some point hopefully then we have a security proof that our protocol the our protocol specification guarantees the security requirements that we have specified earlier in this definition but so this is the main benefits of this approach is that it provides a sound methodology for designing complex protocols and it also prevents insecure Atok design so there is like maybe some of you have heard about it there's like this protocol of this probably most of you have heard about TLS okay and it was designed in a talk way without having it without using this kind of approach of modern cryptography of proofs provable security and it turned out that there are many kind of bugs in this protocol okay so there are many people found problems and now they are trying to fix it it's a kind of a cat-and-mouse game and we want to prevent this from the start and actually now in the new version of TLS people decided to use security proofs to develop the protocols so we believe that we should also do this from this from the start with something as complicated as state channel networks so what is our basic framework to use this this is the quality universal comm possibility framework and some time ago we gave a talks if you gave some talks at the workshop in Berlin and everybody liked this universal compatibility framework so I would like to mention it here as well so this is basically how we kind of define security what actually security means okay so so we have these two worlds ideal world and the real world the ideal world is some kind of abstract specification of what kind of security properties the protocol should satisfy okay so it's very simple it just can be written maybe on half a page yeah so it's very simple specification of what this protocol it is and then the protocol can be like pages long maybe in our case was 2000 I don't know whatever so and now we would like to show that actually this protocol has the same security features then this very compact description this very compact RP description of the specification and this is done by what is called a you see proof a universal comm possibility security proof and this essentially reduces complex protocol to something as simple as this idea of functionality so before I run out of time I want to quickly talk about some extensions and implement it and also briefly about implementation so we recently worked on some follow-up of our original Peru Network paper and we extended it to also cover or to also support multi-party state channels so what is a multi-party state Channel we have now a situation Alice Bob Carol David and Ellis Bob and David they would like to execute some multi-party contract like maybe a game that involves poker game that involves three players and they can do this as follows they built first a virtual channel between Bob and David which was stationed between Bob and David that's what we already have seen in this talk and then over this virtual state channel and the underlying legislation or between Alice and Bob they can create a multi-party state channel and in this case this one then they can deploy a gaming contract a multi-party gaming contract so about implementation we are cooperating with the company Bosh to provide an open-source implementation for a cerium of course we also happy to cooperate with other people we are like a research project mainly at the moment I talked to our colleagues from Porsche and they are currently developing the note software for later state channels they will release this in at the end of this year as an open source project then in hue so on the second half on the first half of 2019 we will they will release an implementation of the visual state channels and the Hopf software and then later at the end of the year they plan to integrate it in some industry use cases okay so this is for the implementation at the moment we of course happy to like this would be open source released soon and it would be great if people here collaborate on this with us so let me conclude my talk so what we are trying to build is provably secure layer two solutions we will also look into other possibly soon other solutions like plasma and so on and we believe that to make them ready for mass for mass of users should there should be solid foundations for these protocols okay so and that just explained you at a very high level what this is like giving these definitions making a protocol specification really formal and releasing it to the public and then proving the security so this is essentially what we did we designed a protocol it's out there you can go to our web page you can read it and it's it's really like I think fully described so you can like take it and implement it where maybe not tonight but maybe in five nights okay so then you can then we have security proofs we prove that these protocols are secure and the next step that we would like to do is because these proofs are quite complicated very involved like many corner cases we have to take care of we would actually like to formally verify them by machines so there are some kind of tools like easy crypt and so on we would like to use to use them to verify that actually our proofs are correct we of course hope that they are correct already but better to let them check by a machine this is what we are currently doing we want to in the future work more on implementations and in particular this is maybe a long-term goal also provides some formally verified implementation and of course is it's very necessary to start with a sound protocol before you like implement something as complicated as this because if you make mistakes at the protocol level already then you don't need even to formally formally verify your implementation so talk further information I hear I would like to thank all our sponsors here it's for our research and I'm happy to take questions you so when you're writing these protocol specs to basically like specify or come up with set of failure modes and then prove that those failure modes can happen and if so then then of course there might be failure modes that you did not think of right yeah and another question is which frameworks are using like what protocol specification languages and proving languages are using so the first question was if there can be connect is I mean like of course what we do is like we have a specification of the after after of the of the protocol okay we give this then we have also model and then we show that whatever and at worst we can do in this model he will not succeed whatever this means for example he will not be able to steal money from the intermediary okay like whatever his behavior is as long as he behaves as specified in the model so all this kind of stuff that you heard today like replay attacks and this kind of stuff this is all covered by our model automatically by this you see framework but other stuff maybe it's not covered like for example side channel attacks okay if there is some kind of adversary who tries to break it by doing some side channel attack or I don't know some other stuff this is the not covered by our our model and you would have to extend it also currently our model we don't really like have integrated fees yet so this is something also that we would like so gasps you don't have this probe you don't have this formally modelled yet and this would also be some next step the second question was well yeah second part was just a twitch so yeah at the moment we have like some abstract specification of the pseudo code of the protocols okay so it says okay party a creates a signature sends it to Bob then Bob does something waits five seconds it creates a signature of this sense it to others and so on so there is something like this it's like a like a pseudo code essentially but we are trying now to move it closer to something like formal language that can then be checked by these automated tools okay so you haven't like written anything like from a large specification and like like temporal if we have not written it in Coke yet or some like I do wanna yeah we will do this we are working on this we also here so you can catch us later all right thanks passion [Applause]