Simple Formally Verified Dapps, Beyond Smart Contracts

Transcript

okay they start or should I wait for an introduction okay hi I am forsworn every door from mutual knowledge systems and I'm going to tell you about simple verified apps and not just for smart contracts and why depth or the very hard test programs to write and why well something is cutting okay introduction the harder programs to write the apps or billion dollar markets seven billion dollars in 2018 seventeen

now and it's headed toward trillions if we take over finance that's right now instead of having a nice s-curve its slumping why was there circumstantial reasons but also structural reasons we have a vicious cycle of no good tech no good apps no good users no money etc and of course every vicious circle is a virtuous circle if only we had more good tech we could have mobile apps and more users and more money etc so it's a bootstrapping issue and the question is what tech should we work on next into our techies there's scalability I think there are people who do great scalability here portability no one does great possibility interoperability

deserves abilities er but the main thing that makes def so hard to write and so them expensive and impossible to use now is security we don't know how to write that that are secure which means that it's extremely costly risky and volatile to use that closely the smallest simplest app will cost you about eighty thousand dollars to ride but mostly to audit maybe only twenty odd thousand dollars to write and then the whole chunk of money to audit it and it will still be unsafe the best apps written by the best experts with the best track record only 400 lines have lost hundreds of millions of dollars again and again

so if you have a million dollar gap new amount of auditing can prove it correct so you will only run it on permissioned blockchains which means not real blockchain and volatility of course at the end of all your efforts your deck will only run on one blockchain say it's very own may be the best not with hope it will be the best we're trying to make it the best but maybe not which means that there is volatility associated to a single using a single chain and volatility associated to having to choose your chain but what if we could solve these issues what if we could slash government the development caused by 90 percent or more right if we could make the risks so much less that

normal programmers can write a dab that is today infeasible what if deaths could run on any blockchain you write it once it turns anywhere that's what I'm trying to do with mutual knowledge systems so let's go back to why blockchain security is so hard it's so hard for these five reasons there is ZERO tolerance to bug if you have one bug can be four hundred lines of code with million lines of code one bug you lose all your money all your lost customers lose all your money and there is no recourse the whole point of the public blockchain is there's no one to make you wrong and there's no one to make you right but you're dead all code is fragile that's not specific to dabs

but most code is return with languages and methodologies that assume it's okay to make mistakes just fix the bug release the software again that's fine but for that that's not okay if you have a bug in your dab you have lost all your money with that we have active adversaries it's not just like most applications where if the bug only happens by a full moon and it's raining well odds are matter much and at midnight but if a DAP has a bug that only happens at midnight when it's raining by a full moon well guess what there is someone in Ukraine who will contrive to call your dab just on a full moon at midnight relief training and

still all your money you have active adversaries the only other guys who have active adversary's or the military or the secret services but they keep their code secret behind our guard and private networks that's run on the public networks where anyone can interact with it and all the code is public and has to be because you have to convince the other parties who will be your enemies that the code is correct so you have to show than the code so they can look at the code and analyze it and break it and finally all the known techniques used to reason about programs are insufficient for dabs when you go to university and you learn how to prove a program correct

and written about the program you assume that all parts of the program's conspire to the same result that everyone cooperates and this is exactly the thing you cannot assume with a dab the whole reason you have a small contract is because you do not trust the other party to cooperate the glow the glow the smart contract is to create incentives for the party other party to cooperate therefore you must have the cooperation as an output as a your contract as an input to it you must prove that your contract align the incentives you can assume that your contract allowing the incentives that the people will cooperate so for all these reasons the apps or the single

hardest programs for anyone to write if you think writing with that is easy you're fooling yourself and none of the existing techniques will help you write dabs of course you want to use logic Dijkstra is famous for saying that all code must be proven correct before it's run and maybe he was wrong for code in general he was proven wrong for code in general but I think he was right for tabs you don't want to write it up and run it before you know for sure that it's correct maybe you want to toy dab and run it for $5.00 before it's correct you don't want to put a million dollar billion dollar into that that has not been true incorrect that's required

domain-specific logic need more than the usual use logical tools and you can't do the logic afterward you can't first right to adapt in solidity and then hope to prove it correct that's low probability of working especially sure that is big to write that correct you must use a language or a system that is designed for proving the depth correct and otherwise adapt make sure that at each step you do everything designed to make it correct because you can't do that after the fact if you didn't do that as beforehand the best way to push your lap correct is to scratch it and start again using the correct method and of course complexity makes logic intractable if you have a

very complex program you will never be able to find the proof automatically and most users won't be able to find it by hand so it will be impossible to prove it correct to prove the program correct must keep it absolutely simple and simple in terms of mathematics not is very simple in terms of human discussion so you want to keep your that in the way that is very simple and then you can use automation and automatically prove your things correct and of course you say oh it's too complex it's too expensive why should I bother with automating logic well if you think that it's costly to use logic you haven't yet built a

billion dollar app that does not use logic and that is all its money because the bad guys will use logic they will either hire or enslave a mathematician from China or Russia and he will break your app he will use the tools so hi friends so that's where butyl donate system is trained to solve these problems we have a domain-specific language that DSL for ducks it uses a domain-specific logic design just for that and when I say that I mean not just a small contract with all solution matching client and server code because if your DAP is perfectly correct but you have a bug in your client or server code

someone is going to lose all their money maybe not everyone is going to lose all their money but someone is going to lose all their money too so is that something you don't want so we are a moon were looking for early customers and investors but I'll come back to that later first let's present our language glow which are that language so what should that first but that is an interaction people will exchange messages who are these people there are multiple people who don't trust each other or have maybe a limited trust but basically new trust between each other and as part of these directions it will exchange assets on public Ledger's and these assets will be subject to rules that we can verify so

you can have a computer check that everyone did or did not do their thing hello oh sorry and so here's a simple program that illustrates essential things about interactions it's only 22 lines of code and it illustrates the main problems it's a rock-paper-scissors so what paper scissors a simple game where two people choose at the same time a hand rock-paper-scissors and rock beats scissors that beats paper that we track that's easy except that on the blockchain there is no such thing as at the same time so let's first look at the set oh no oh no it's God that will make things more complex

okay so doesn't display resolution so you have that okay you have a data type hand that's rock paper scissors and outcome and you compute the winner through this kind of magic formula I don't want to it's only seven lines when you see ones interaction that's not going to can we use a sorry let me try to use my computer because this is not working very well do you have HDMI cable okay I would like to okay let's talk about in

there can you control - or something control - or no okay no well okay so in this program oh okay and you can do oh you can scroll door that's better than nothing I suppose more plus plus plus plus plus again oh good thanks okay so when you do 1d I put some colors you have some some things are done by

Alice a some things are done by Bob and some things are done by Alice the way it works is that we can polish messages at the same time so Alice will first choose her hand and commit to this hand by publishing a digest of this hand and some salt some random salt that she chooses this way Bob knows that at least cannot change her mind and choose the hand that will beat him after the fact at least has to commit to a hand first and then Bob will reveal his hand and then Alice will revolt her hand and salt and we can check that the commitment is correct so when we verify the commitment we verify the formulas above and whenever Alice's defines her hand or her salt

only she can see it until it's published which will be much later when she publishes her commitment and commitment and publishes it then Bob can see it but otherwise variables remain private which means that we have a specification where when we when we have the godly view God can see both what Alice and Bob has we can reason about what's going to happen but when we will compile this program to Alice's client and Bob's clients Alice will only be able to see her variable and what's had been published by Bob but will only be able to see his variable and less has been published by Alice and everyone will be safe and so the rest is less interesting oh yes input hand we

are going to have a UI the dua will be separated from the program and isolated for the blockchain so I the UI will be written in a different language this is a language glow that looks a bit like the JavaScript or Ted script or with an ml but your interface will be written in a separate module that will be easily at from the block saying so you will not be able to talk directly to the blockchain you will talk only to this module or that that is safe okay so this more contract generator is about three times the size of my program no time to look at it the client is also about the same size but that generator client if you need to write it by hand it would be much harder and longer I wrote my first

version by hand just to see how much it would be like five times longer than that of three four times same thing the client for the other player Bob and also generate interface acceleration of course we generate a large expect and happily it's not renewable it's part of my to do this to make suspect readable but what the thing of the kind of things we prove is first that the ledger is always balanced that when everyone cooperates the liveness property is hold whatever the liveness property sources are some that are built into the system and some you want to defend yourself the safety property is I think that no one on the market even thinks about it the fact that you want to prove that even if

the other party does not cooperate the interaction is fine for you you will not if if it's a lease times out Bob can say hey Alice timed out she loses and she forfeited her her wager amount similarly if Bob times out I just can say work times out I can get back my money there is no money that will get locked up they will there will be no other bad things that will happen to Alice or Bob if the other fails to cooperate and of course a lot of the specs will have to be user specified such as two assertions are added in my program that it was safe for Alice and Bob to play I cannot get that as a author of the programming language you

will have to write those things the the programming language can make it much simpler for you to write and even express those things that are not a tool expressible in other programming languages which you still have to write the properties you need to prove for your app that's up specific the one can do that for you it's not magic so what does the we automate we automate adding for center in escrow what if Alice chooses the paper and Bob chooses scissors then that is oh I'm going to lose why should I cooperate and publish the last message she shouldn't and then Bob will time out and loser waste a lot of time but if Alice has to deposit a sufficiently high escrow that can be automated Lee automatically added

and computed then she's incentivized to keep cooperating even if she loses okay she lost but if she does not cooperate you will lose the wager amount and the extra amount so she still cooperates and shows her hand in any interaction where you have a future message you need to deposit an escrow beforehand we can also mercury as a contract contract stated we didn't see that but it's an optimization that will save you a lot of gas and you really don't want to write this optimization by hand when you write it solidity because you will get it wrong or you will modify your program later and that will make it wrong and then the types you say will not help you so amortization of stage will set you a lot of gas and it can be done

automatically for you by our language we can use also generalize state channels if you use or generalized state channel today you must make sure that your JavaScript program and your solid D program or you go for a multiple use or perfectly in sync even as you modify your program that's extremely hard we can generate everything from the same spec in the future we can also use any HT and CK Snorks to add privacy to our contract so that no one else but the contractors know what's in the contract and of course in the future we can also generate code for any blockchain there is nothing a certain specific in my programming language why does it matter well we have better depths for a

fraction of the cost like literally like ten times fewer codes and you had to write it by hand the code states automatically in sync when the spec evolves that's very important because respect will evolve that bit rot it's safer because you can actually express the rings logic the things that matter to your app you're not proving a module of your app you're proving the implementation of your app you can do optimizations you wouldn't afford by hand such as a virtualization of state and it will be possible to any blockchain so we are solving like a lot of hard problems for app developers we're the right company because this requires skills in blockchain but also

in economics in computing in logic and in design and if you miss one of them you will not even know that you are missing it and you will do things wrong I've done this kind of single material long at IT software Google and rich water where I built software to make it simpler and safer for individuals and launched into write code and I left research for industry precisely because I wanted to build systems but I still kept a lot of contacts in research that's why I have a lot of people I know who can help me build a good language how much time do I have to discuss attack models so a lot of major failures in the past can be attributed to what I

would call abstraction failures the dow hack is a real fancy issue why do you even have real currency problems in the EVM maybe you have them in the EVM but you should certainly not expose that to the language you use to program applications in my language there is no reentrant see issue because there's no possible entrance e with any stage that can be used twice so the or entrance e issue no doubt hack possible virtual attack bad access delegation the notion of delegating delegate : relating to a contract should not be visible to the language it's an implementation details you still need to get it right but you can get it right once for all your

applications and you don't have to to get it right or wrong for your language part you'll attack number 2 the library destructions that's again it's an abstraction failure many other hacks or bad or missing permission checks as an abstraction failure in my language every everything is done by some participant and your safety serum say that you are safe whatever the other participant does so if something allows anyone to destroy the code or to steal your money you will be incapable of proving the safety property because it will be

trivial to show no you are not safe because hey this guy can take your money so you will not be able to prove the safety property therefore you will detect early on that I should not run this app there the safety property is not it's not there so abstraction failures and the solution is to have a better programming model and yes you still need to implement it well that the implementation effort can be shared between old apps instead of every dab developer having to get it right and then learn all the tricks of the evn misplaced trust I cannot solve that if you trust them the bad exchange and give them your money and they run away with it or if you trust the bad Oracle and someone's Oracle start lying and your

money is worth nothing I cannot help you with that directly but I can do two things I can make the trust assumption explicit so that when your try to run the app app says beware if you run this app you are trying you are going to trust this operator as custodian of your money or this operator as your Oracle so you choose to trust this Oracle you can still choose to trust it but you know that it's centralized and you know whom to blame if things go wrong and of course as killer that maybe we can build the node in Crystal load non-custodial decks or decentralized Oracle's and I believe it will be much easier to write

these things in a portable way in safer way using my language and without okay low-level attacks oh it's time one novel attack okay you can have Network DDoS so I know where your computer is I will just DDoS it so you cannot post your your play your your turn your your transaction on time and therefore you will time out and I will collect your money so if you are going to play poker on or any high stake contract on on the Sirian you have to make sure that you will be able to post

the trends at your final transaction before the deadline otherwise you lose all your money and if it's $10 or saying I want to anything again stupid if it's a million dollar transaction I will cut your internals line I will destroy your satellite connection I will do lots of bad things for you to get to a million or ten million or a billion dollar and prevent you from posting the transactions that would make you have it I can also do a for most really attacker that's my one of my favorite who here has heard of the most Reedy okay if you haven't you should read it's it's beautiful basically these guys prevented his rivals from posting their final

transactions our next transaction and making them timeout by buying the entire Eastern Bloc chain for five minutes and so for some like tens of thousands of dollars she collected a million dollar prize it's the right way so if you are if you don't have an economist at work in your team you will not be able to survive this kind of attack who he is who here has a DAP and does not have an economist to do that to do that right okay well you better either hire one or Hydra services of someone who hires one because otherwise your dad will fail as soon as stakes get high enough for someone to play for much Rudy plenty of

other Berg's if you don't have redundancy but all that's what I mean that you will need a lot of specialized engineering and what you really want to do is focus on your business logic the things that you're good at the thing like I want to do defi to help people finance whatever I would you focus on the finance I want don't know what you're doing supply chain trading whatever you're doing you want to focus on that the thing where you're creating value for people you don't want to focus on this rigid systems systems programming economic modeling economic mechanism the mechanism design cryptography information security programming language use and programming language implementation you don't want to focus

on that and if you want to you better hire top experts in each of them and a manager to manage all of them and your business logic expert that's a lot of people to get it up right and so if you would do adapt today you need all of that and that will cost you ten times more than hiring just a business logic guy and having us hire the other experts by using our language you can cut tremendously on codes by basically pulling the coasts with everyone else who uses our language so my conclusion is that at moon mutual knowledge moon we are solving the hardest problems in that

making it safe to write them with a domain-specific language and it's not just more contracts but also the client server that good that comes with it we are looking for our little customers if you have a killer dub that's just too hard please come to me with my language you can make it doable and of course investors let's keep the business plan the meta story is that simplicity is very important if you want people to write apps you must make it very simple to write that you don't want to expose your DAP developers to all these complexities that I alluded to before hand that's not you can't do it you must have simple interfaces and yes the implementation can be complex to a

point but the interface will be very simple and this is possible because we need to have skills at the intersection of blockchain economics computing logic and design all these are needed to make a good language and ultimate goal of course is to give back to users control over the Jizo sovereignty we want to decentralize internets which were called Internet and I think we can do it we can do it together please come and join me at moon for more information we have a website and white paper etc etc and now I will open the floor to questions [Applause] so please let me play the devil's

prosecutor yes because so usually when I hear talks like that I asked the following questions so the majority of these attacks resulted not from the formals but the implementation not matching the formal specification the problem was almost always that the informal specification and the formal specification were mismatched yes and if exactly and when I looked at your source code it looks like something out of the underhanded sea context so where you know a misplaced a misplace the semicolon can completely change the meaning yes so how would you suggest to match the informal specification and the

kind of code that you write in your language to things yes it is a very important problem like I wrote an article about the limits what formal methods can and cannot do and they can never do everything because there's only this part of matching the reality to the code but once again the input simplicity is extremely important with more complex systems you still have this problem you just have this problem like ten times more and exponentially more complex so you still it denoted but auditing twenty two lines of code will be ten times easier than auditing 200 lines of code which will be thousand times easier than auditing two thousand lines of code

because like the the complexity grows only are known linearly with the complexity and the size of the code so this does not save everything you still needed someone to audit this code it's only 22 lines but yes it could be underhanded and you probably want to add lots of tests lots of additional properties etc before you trust it yes but to be so much easier to OD just 22 lines of code then - who did the society variant and then the chasers violent and in the Cardinal variant and then the Bitcoin cash variant or whatever you have you can check it once for this abstract 22 line saying and own it everywhere and trust it you also need to trust implementation but then so then

again you can pool resources to check it and audit it but saying that's a very important question thank you any other question Stan you want to say something just you know the question which I have actually just have you considered like your approaches in a sense revolutionary in the sense that you're creating a new language but usually it's very hard to create a new language you know yes well there could be you could sit like a smaller goal you could say you know let's take solidity because reality 99.999% of people programming solidity can you take solidity and somehow add

some decorators maybe you know some attributes can you actually instead of trying to solve the entire problem just use somehow find a way to inject these ideas into solidity to make just a little bit more secure you know go the other way I don't think solid the solidity can be saved but what I cut what I do think is that you can write contracts that have like large part that are computations done in say Python or roasts or whatever what have you and say this computation is running a sandbox so I only care about the result of this computation and I will be able to verify that the computation is correct what is that we

agree on the result of the computation and have a contract where the co of the interactions interactive sport may still be written in my language or something very close to it at the core that let the logic you can't escape but the rest will be returned in your usual language like you will write it in APL bison or whatever your financial team uses you know not your your geek Network team and so the financial part will be written the language of the finance guys which it will be run in a sandbox so that I only need to check the results so no not solidity you want to language that the

financial guys use and yes we will be able to that's a further project I know how to do that but it's more work this is already too much work so but yes no more questions thank you very much for listening and thank you for coming [Applause] you