Formal verification and CBC Casper

Transcript

so without further ado I would like to introduce the first speaker at dooya Nakamura researcher at lyrics at the University of Tokyo who will talk to us about formal verification and CBC Kasper thank you hello morning I will talk about formal education and the form of education of CBC Kasper I'm Leah from Tokyo Japan and working at lay eggs I'm working on CBC Kasper for a few months and the

previously working on came km a bit and the Viper so first well it's for modification so for modification is a kind of a way to prove properties based on Matt and there are two kinds of form of education first one is a form of educational programs which is a relatively popular in Eastern community like the for modification of smart contract and for application or program in the Korean software and today I will talk about the form of Education or protocols of consensus protocols the dual form of reification you first need

to formalize the target this is the example of kvam and this basically formalizing is execution of eevn so why people do form of Education to do form of application you need to define everything in math so this process of formalization makes it clear what is a target what is a goal what is assumptions so this reduces the miscommunication between researchers and developers and instruments and in most cases formal education is performed in tools there are a lot of tools to the form of Education including general

proof interactive theorem provers Leacock Isabel and domain-specific tools like a framework and this help you to find the bugs because machine can check automatically checked with the proof is correct or not so I will talk about my project to a form of Education with shimshi Kasper a quick introduction with shabby chic as per submission Kasper is a family or proof of state consensus protocols defined by five parameters and she be she is stands for collected by construction which means that um every member of gypsy Kasper satisfies the

same proof of a synchronous safety so shimshi transfer is originally written in really formal by brad and other a teacher and other workers and my work is to define and improve the existing formalization in Isabel Isabel is a proof assistant similar to caulk or actor and you can think of it as like a an IDE for mathematical logic I mean you can do you can refactor your proof and you can use members fist booting in Isabel and Isabel is relatively strong in automatic so improving so this is the five parameters of ships to Casper in

Isabel the buoy is set of birth data's and W is the weight mapping of redditors on t is the threshold for certain potential behavior and C is basically a possible set of possible blocks and E is called estimator which is basically for choice and the bottom picture represents restriction of these parameters CPC casper models the protocol by message and state so both dated send messages between each other and the state is a local state and it is a set of messages

and message has three members first one is sender which is birthdate of who sent message and estimate which is the Brock fits the message board for and justification justification is very important in Shiva Kasper so I are explained in this right justification is the set of messages which the sender seen so far so in this figure the arrow Brock bye-bye be is justifying justifying the green rocks and impro in normal protocol execution very data must justify every messages he have sent so far so

justification is essentially the evidence of the for choice so the estimate which is a broke the center would fall must be the result was a folk choice so it's a good point to have justification in messages is that too is that you can detect this these certain kinds of representing behavior yeah so the formal definition of valid message and the state is a bit complicated but there is too important a point the first one is that so far data must see must justify the every messages which the

other message testifies and the the second let settlement is the enforcement or the folk choice so this is a presumption behavior which can be detected by justification which is called equivocation so in this figure the VAR data D there's two blocks by by Delta D does not justify each other so it's it's equivocation so you can detect these kinds of presenting behavior in in CBC Kasper and this helps proof of safety and other things shipshape state transition in shemish Casper is

relatively simple it's just a superset relation of states and this is a formal definition of decision in shape see Casper so in the traditional PFD consensus protocols react endowment and NPV of T but later make decisions on products which two times of two thirds of boats but in subsea Casper the decision-making Lou is really strict because um but letter must make decisions which is blue but it will be true for any future state so to actually detect these decisions you need

some heuristics like all safety Oracle so I'll explain what what proof is about is look like this is a synchronous safety in shimshi Kaspar in Sibel and three line in the bottom is isabelle proofs so Isabelle have a lot of proof method then the first ring is basically doing basically unfolding the definition we decided because Isabelle does not run for definitions by default the second line is means that I want to use the lemma which is already proved in another

place the third line is automatic Syrian probing method which is medicine and it using the built-in lemma to be honest I didn't I don't find the last round line of proof because we have automatic proof such so in Isabelle it does not always prove everything but it's about sometimes help you to find some part of proof this is the picture which Isabel find last line of proof so the previous definition of safety is a little bit too

abstract so we can instantiate the theorem to the proxxon context this is a safety in the context of production which means that there is no conflicting procs which is agreed on perdidos by auditors so finally I explained my work in progress work and the future works the biggest one is that to prove the correctness of safety Oracle so as I explained in submission Casper the decision-making rule is really strict so everybody data must detect the finalized rocks and this is a one kind of safety Oracle called quick Oracle in Creek

Oracle for data try to find a set of or data's which is called Creek this is basically the birth data's through locked on the Brock so hryvnas every people say talk about the liveness of is kasper but my conjecture is that a creek eventually forms when the underlying chain converges so from this observation what we need to do to provide an essential worship see Casper is that to prove the liveness of the underlying chain so Live Nation ship is Casper is essentially equivalent to the lightness of the underlying chain so for that we need to prove the convergence of

elementals because default for choice in ships across space is a remedy ghost so to prove these kinds of things in Isabel might be a bit tricky so I might use another way to prove this for Murray thank you so much [Applause]