WEBVTT Kind: captions Language: en 00:00:14.259 --> 00:00:15.909 align:start position:0% thank<00:00:15.259> you 00:00:15.909 --> 00:00:15.919 align:start position:0% thank you 00:00:15.919 --> 00:00:17.770 align:start position:0% thank you corrupted<00:00:16.460> good<00:00:17.060> afternoon<00:00:17.270> everyone<00:00:17.660> and 00:00:17.770 --> 00:00:17.780 align:start position:0% corrupted good afternoon everyone and 00:00:17.780 --> 00:00:20.560 align:start position:0% corrupted good afternoon everyone and welcome<00:00:18.020> to<00:00:18.620> this<00:00:18.740> talk<00:00:19.010> about<00:00:19.820> sacrify 00:00:20.560 --> 00:00:20.570 align:start position:0% welcome to this talk about sacrify 00:00:20.570 --> 00:00:23.110 align:start position:0% welcome to this talk about sacrify Sakura<00:00:21.530> is<00:00:21.770> a<00:00:21.800> smart<00:00:22.190> contract<00:00:22.310> verification 00:00:23.110 --> 00:00:23.120 align:start position:0% Sakura is a smart contract verification 00:00:23.120 --> 00:00:25.540 align:start position:0% Sakura is a smart contract verification tool<00:00:23.500> which<00:00:24.500> was<00:00:24.710> developed<00:00:25.070> by<00:00:25.130> the<00:00:25.220> people 00:00:25.540 --> 00:00:25.550 align:start position:0% tool which was developed by the people 00:00:25.550 --> 00:00:26.890 align:start position:0% tool which was developed by the people that<00:00:25.670> you<00:00:25.760> can<00:00:25.880> see<00:00:26.090> on<00:00:26.210> this<00:00:26.360> slide 00:00:26.890 --> 00:00:26.900 align:start position:0% that you can see on this slide 00:00:26.900 --> 00:00:29.140 align:start position:0% that you can see on this slide it<00:00:27.320> was<00:00:27.440> developed<00:00:27.860> at<00:00:27.950> ETH<00:00:28.430> Zurich<00:00:28.730> which<00:00:28.940> is 00:00:29.140 --> 00:00:29.150 align:start position:0% it was developed at ETH Zurich which is 00:00:29.150 --> 00:00:30.730 align:start position:0% it was developed at ETH Zurich which is leading<00:00:29.750> Technical<00:00:30.230> University<00:00:30.260> in 00:00:30.730 --> 00:00:30.740 align:start position:0% leading Technical University in 00:00:30.740 --> 00:00:33.250 align:start position:0% leading Technical University in Switzerland<00:00:31.340> and<00:00:31.880> you<00:00:32.719> can<00:00:32.840> learn<00:00:33.020> more<00:00:33.200> about 00:00:33.250 --> 00:00:33.260 align:start position:0% Switzerland and you can learn more about 00:00:33.260 --> 00:00:36.250 align:start position:0% Switzerland and you can learn more about sacrified<00:00:34.250> by<00:00:34.490> visiting<00:00:35.329> the<00:00:35.480> various<00:00:36.020> links 00:00:36.250 --> 00:00:36.260 align:start position:0% sacrified by visiting the various links 00:00:36.260 --> 00:00:37.810 align:start position:0% sacrified by visiting the various links that<00:00:36.440> will<00:00:36.560> appear<00:00:36.829> in<00:00:36.920> these<00:00:37.010> slides<00:00:37.220> and<00:00:37.579> I 00:00:37.810 --> 00:00:37.820 align:start position:0% that will appear in these slides and I 00:00:37.820 --> 00:00:39.400 align:start position:0% that will appear in these slides and I will<00:00:38.000> make<00:00:38.810> the<00:00:38.990> slides<00:00:39.230> available 00:00:39.400 --> 00:00:39.410 align:start position:0% will make the slides available 00:00:39.410 --> 00:00:43.120 align:start position:0% will make the slides available afterwards<00:00:40.280> after<00:00:40.790> this<00:00:40.940> talk<00:00:41.620> so<00:00:42.620> first<00:00:42.920> let 00:00:43.120 --> 00:00:43.130 align:start position:0% afterwards after this talk so first let 00:00:43.130 --> 00:00:47.200 align:start position:0% afterwards after this talk so first let me<00:00:43.160> let<00:00:43.970> me<00:00:45.190> tell<00:00:46.190> you<00:00:46.310> the<00:00:46.460> reasoning<00:00:46.850> behind 00:00:47.200 --> 00:00:47.210 align:start position:0% me let me tell you the reasoning behind 00:00:47.210 --> 00:00:49.750 align:start position:0% me let me tell you the reasoning behind Sakura<00:00:47.989> Phi<00:00:48.200> and<00:00:48.440> motivate<00:00:49.160> the<00:00:49.310> creation<00:00:49.670> of 00:00:49.750 --> 00:00:49.760 align:start position:0% Sakura Phi and motivate the creation of 00:00:49.760 --> 00:00:53.250 align:start position:0% Sakura Phi and motivate the creation of Sakura<00:00:50.120> Phi<00:00:50.440> so<00:00:51.610> most<00:00:52.610> of<00:00:52.700> you<00:00:52.850> are<00:00:53.090> aware 00:00:53.250 --> 00:00:53.260 align:start position:0% Sakura Phi so most of you are aware 00:00:53.260 --> 00:00:56.049 align:start position:0% Sakura Phi so most of you are aware assume<00:00:54.260> in<00:00:54.500> this<00:00:54.680> room<00:00:54.890> of<00:00:55.130> the<00:00:55.430> various 00:00:56.049 --> 00:00:56.059 align:start position:0% assume in this room of the various 00:00:56.059 --> 00:00:57.940 align:start position:0% assume in this room of the various security<00:00:57.020> flaws<00:00:57.320> that<00:00:57.350> have<00:00:57.590> plagued<00:00:57.920> the 00:00:57.940 --> 00:00:57.950 align:start position:0% security flaws that have plagued the 00:00:57.950 --> 00:00:59.590 align:start position:0% security flaws that have plagued the theorems<00:00:58.430> in<00:00:58.579> the<00:00:58.700> beginning<00:00:59.090> so<00:00:59.270> the<00:00:59.420> most 00:00:59.590 --> 00:00:59.600 align:start position:0% theorems in the beginning so the most 00:00:59.600 --> 00:01:02.110 align:start position:0% theorems in the beginning so the most famous<00:00:59.809> one<00:01:00.079> remains<00:01:00.440> the<00:01:00.890> dowel<00:01:01.250> bug<00:01:01.489> which 00:01:02.110 --> 00:01:02.120 align:start position:0% famous one remains the dowel bug which 00:01:02.120 --> 00:01:04.450 align:start position:0% famous one remains the dowel bug which eventually<00:01:02.480> led<00:01:02.809> the<00:01:03.020> developers<00:01:03.500> to<00:01:03.920> do<00:01:04.430> a 00:01:04.450 --> 00:01:04.460 align:start position:0% eventually led the developers to do a 00:01:04.460 --> 00:01:06.760 align:start position:0% eventually led the developers to do a hard<00:01:04.790> fork<00:01:05.089> of<00:01:05.299> the<00:01:05.329> chain<00:01:05.659> so<00:01:06.260> as<00:01:06.380> to<00:01:06.500> river 00:01:06.760 --> 00:01:06.770 align:start position:0% hard fork of the chain so as to river 00:01:06.770 --> 00:01:08.740 align:start position:0% hard fork of the chain so as to river the<00:01:06.950> state<00:01:07.310> the<00:01:07.520> state<00:01:07.760> change<00:01:08.000> is<00:01:08.150> created<00:01:08.600> by 00:01:08.740 --> 00:01:08.750 align:start position:0% the state the state change is created by 00:01:08.750 --> 00:01:12.000 align:start position:0% the state the state change is created by the<00:01:08.810> attackers<00:01:10.330> another<00:01:11.330> more<00:01:11.840> recent 00:01:12.000 --> 00:01:12.010 align:start position:0% the attackers another more recent 00:01:12.010 --> 00:01:14.830 align:start position:0% the attackers another more recent security<00:01:13.010> flaw<00:01:13.490> was<00:01:13.700> a<00:01:13.760> multi<00:01:14.150> security<00:01:14.659> bug 00:01:14.830 --> 00:01:14.840 align:start position:0% security flaw was a multi security bug 00:01:14.840 --> 00:01:16.780 align:start position:0% security flaw was a multi security bug which<00:01:15.409> resulted<00:01:15.890> in<00:01:15.979> 30<00:01:16.310> Millions 00:01:16.780 --> 00:01:16.790 align:start position:0% which resulted in 30 Millions 00:01:16.790 --> 00:01:21.430 align:start position:0% which resulted in 30 Millions in<00:01:17.360> a<00:01:17.510> theorem<00:01:18.250> robbed<00:01:19.250> by<00:01:19.520> by<00:01:20.060> attackers<00:01:20.510> so 00:01:21.430 --> 00:01:21.440 align:start position:0% in a theorem robbed by by attackers so 00:01:21.440 --> 00:01:23.890 align:start position:0% in a theorem robbed by by attackers so let<00:01:22.070> me<00:01:22.220> go<00:01:22.310> into<00:01:22.580> details<00:01:22.880> of<00:01:23.090> this<00:01:23.150> second 00:01:23.890 --> 00:01:23.900 align:start position:0% let me go into details of this second 00:01:23.900 --> 00:01:27.219 align:start position:0% let me go into details of this second floss<00:01:24.140> more<00:01:24.560> more<00:01:25.040> precisely<00:01:26.030> so<00:01:26.810> it<00:01:27.020> was<00:01:27.200> a 00:01:27.219 --> 00:01:27.229 align:start position:0% floss more more precisely so it was a 00:01:27.229 --> 00:01:30.070 align:start position:0% floss more more precisely so it was a case<00:01:27.440> of<00:01:27.500> in<00:01:27.950> privileged<00:01:28.340> right<00:01:28.549> storage<00:01:29.090> here 00:01:30.070 --> 00:01:30.080 align:start position:0% case of in privileged right storage here 00:01:30.080 --> 00:01:32.440 align:start position:0% case of in privileged right storage here I<00:01:30.140> have<00:01:30.409> a<00:01:30.439> really<00:01:30.799> simple<00:01:31.130> example<00:01:31.790> of<00:01:31.909> this 00:01:32.440 --> 00:01:32.450 align:start position:0% I have a really simple example of this 00:01:32.450 --> 00:01:34.690 align:start position:0% I have a really simple example of this kind<00:01:32.630> of<00:01:32.720> flaw<00:01:32.990> so<00:01:33.380> just<00:01:33.770> keep<00:01:33.950> in<00:01:34.070> mind<00:01:34.310> for 00:01:34.690 --> 00:01:34.700 align:start position:0% kind of flaw so just keep in mind for 00:01:34.700 --> 00:01:36.550 align:start position:0% kind of flaw so just keep in mind for all<00:01:34.850> the<00:01:35.000> examples<00:01:35.270> that<00:01:35.450> are<00:01:35.630> going<00:01:35.840> to<00:01:36.140> come 00:01:36.550 --> 00:01:36.560 align:start position:0% all the examples that are going to come 00:01:36.560 --> 00:01:38.770 align:start position:0% all the examples that are going to come that<00:01:37.100> these<00:01:37.820> are<00:01:38.030> meant<00:01:38.270> only<00:01:38.450> to<00:01:38.600> illustrate 00:01:38.770 --> 00:01:38.780 align:start position:0% that these are meant only to illustrate 00:01:38.780 --> 00:01:41.469 align:start position:0% that these are meant only to illustrate the<00:01:39.590> flaws<00:01:39.860> and<00:01:40.070> not<00:01:40.280> are<00:01:40.670> not<00:01:40.729> meant<00:01:41.119> to<00:01:41.210> to 00:01:41.469 --> 00:01:41.479 align:start position:0% the flaws and not are not meant to to 00:01:41.479 --> 00:01:43.030 align:start position:0% the flaws and not are not meant to to have<00:01:41.600> a<00:01:41.630> real<00:01:41.900> logic<00:01:42.290> in<00:01:42.409> themselves<00:01:42.770> so<00:01:42.890> as 00:01:43.030 --> 00:01:43.040 align:start position:0% have a real logic in themselves so as 00:01:43.040 --> 00:01:44.679 align:start position:0% have a real logic in themselves so as you<00:01:43.159> see<00:01:43.340> here<00:01:43.580> it's<00:01:43.970> really<00:01:44.210> a<00:01:44.240> toy<00:01:44.479> example 00:01:44.679 --> 00:01:44.689 align:start position:0% you see here it's really a toy example 00:01:44.689 --> 00:01:47.170 align:start position:0% you see here it's really a toy example so<00:01:45.259> this<00:01:46.009> is<00:01:46.159> a<00:01:46.189> wallet<00:01:46.580> contract<00:01:47.030> which 00:01:47.170 --> 00:01:47.180 align:start position:0% so this is a wallet contract which 00:01:47.180 --> 00:01:49.719 align:start position:0% so this is a wallet contract which contains<00:01:47.600> the<00:01:47.780> storage<00:01:48.140> viable<00:01:48.619> honor<00:01:48.890> which 00:01:49.719 --> 00:01:49.729 align:start position:0% contains the storage viable honor which 00:01:49.729 --> 00:01:52.390 align:start position:0% contains the storage viable honor which specify<00:01:50.720> the<00:01:50.780> owner<00:01:51.080> of<00:01:51.350> this<00:01:51.530> wallet<00:01:51.770> and 00:01:52.390 --> 00:01:52.400 align:start position:0% specify the owner of this wallet and 00:01:52.400 --> 00:01:54.179 align:start position:0% specify the owner of this wallet and there<00:01:52.790> are<00:01:52.880> two<00:01:53.090> functions<00:01:53.540> this 00:01:54.179 --> 00:01:54.189 align:start position:0% there are two functions this 00:01:54.189 --> 00:01:56.620 align:start position:0% there are two functions this initialization<00:01:55.189> function<00:01:55.400> init<00:01:56.270> wallet 00:01:56.620 --> 00:01:56.630 align:start position:0% initialization function init wallet 00:01:56.630 --> 00:01:59.020 align:start position:0% initialization function init wallet which<00:01:57.140> can<00:01:57.380> change<00:01:57.409> the<00:01:57.950> honor<00:01:58.100> and<00:01:58.369> this 00:01:59.020 --> 00:01:59.030 align:start position:0% which can change the honor and this 00:01:59.030 --> 00:02:00.999 align:start position:0% which can change the honor and this withdraw<00:01:59.659> function<00:02:00.170> through<00:02:00.619> which<00:02:00.799> the 00:02:00.999 --> 00:02:01.009 align:start position:0% withdraw function through which the 00:02:01.009 --> 00:02:04.120 align:start position:0% withdraw function through which the owner<00:02:01.250> can<00:02:01.900> actually<00:02:02.900> withdraw<00:02:03.380> money<00:02:03.710> so<00:02:04.070> you 00:02:04.120 --> 00:02:04.130 align:start position:0% owner can actually withdraw money so you 00:02:04.130 --> 00:02:07.899 align:start position:0% owner can actually withdraw money so you can<00:02:04.460> see<00:02:04.700> here<00:02:05.470> this<00:02:06.470> works<00:02:06.710> so<00:02:07.579> you<00:02:07.640> can<00:02:07.759> see 00:02:07.899 --> 00:02:07.909 align:start position:0% can see here this works so you can see 00:02:07.909 --> 00:02:10.059 align:start position:0% can see here this works so you can see here<00:02:08.090> that<00:02:08.119> there<00:02:08.689> is<00:02:08.780> actually<00:02:09.170> a<00:02:09.200> check<00:02:09.530> to 00:02:10.059 --> 00:02:10.069 align:start position:0% here that there is actually a check to 00:02:10.069 --> 00:02:12.520 align:start position:0% here that there is actually a check to prevent<00:02:10.429> anybody<00:02:10.640> else<00:02:10.940> from<00:02:11.200> from<00:02:12.200> from 00:02:12.520 --> 00:02:12.530 align:start position:0% prevent anybody else from from from 00:02:12.530 --> 00:02:15.040 align:start position:0% prevent anybody else from from from withdrawing<00:02:13.160> money<00:02:13.400> but<00:02:14.270> the<00:02:14.360> problem<00:02:14.690> in 00:02:15.040 --> 00:02:15.050 align:start position:0% withdrawing money but the problem in 00:02:15.050 --> 00:02:18.010 align:start position:0% withdrawing money but the problem in case<00:02:15.260> is<00:02:15.530> that<00:02:15.710> anybody<00:02:16.100> can<00:02:16.460> actually<00:02:17.020> change 00:02:18.010 --> 00:02:18.020 align:start position:0% case is that anybody can actually change 00:02:18.020 --> 00:02:21.130 align:start position:0% case is that anybody can actually change the<00:02:18.140> the<00:02:19.040> owner<00:02:19.190> viable<00:02:19.790> which<00:02:20.360> is<00:02:20.540> a<00:02:20.570> problem 00:02:21.130 --> 00:02:21.140 align:start position:0% the the owner viable which is a problem 00:02:21.140 --> 00:02:24.870 align:start position:0% the the owner viable which is a problem since<00:02:21.500> because<00:02:22.430> it<00:02:22.580> makes<00:02:22.820> the<00:02:23.000> check<00:02:23.600> useless 00:02:24.870 --> 00:02:24.880 align:start position:0% since because it makes the check useless 00:02:24.880 --> 00:02:28.800 align:start position:0% since because it makes the check useless so<00:02:25.880> this<00:02:26.240> is<00:02:26.560> this<00:02:27.560> is<00:02:27.620> in<00:02:27.950> a<00:02:28.070> sense<00:02:28.280> the<00:02:28.730> the 00:02:28.800 --> 00:02:28.810 align:start position:0% so this is this is in a sense the the 00:02:28.810 --> 00:02:31.600 align:start position:0% so this is this is in a sense the the mystic<00:02:29.810> peyote<00:02:30.020> bug<00:02:30.320> that<00:02:30.830> is<00:02:31.040> you<00:02:31.370> allow 00:02:31.600 --> 00:02:31.610 align:start position:0% mystic peyote bug that is you allow 00:02:31.610 --> 00:02:34.150 align:start position:0% mystic peyote bug that is you allow anybody<00:02:31.910> to<00:02:32.150> write<00:02:32.450> to<00:02:33.020> your<00:02:33.380> storage<00:02:33.680> even 00:02:34.150 --> 00:02:34.160 align:start position:0% anybody to write to your storage even 00:02:34.160 --> 00:02:36.090 align:start position:0% anybody to write to your storage even though<00:02:34.430> you<00:02:34.490> rely<00:02:34.850> on<00:02:34.880> it<00:02:35.150> for<00:02:35.180> crucial 00:02:36.090 --> 00:02:36.100 align:start position:0% though you rely on it for crucial 00:02:36.100 --> 00:02:39.070 align:start position:0% though you rely on it for crucial operations<00:02:37.100> so<00:02:37.790> of<00:02:37.970> course<00:02:38.180> the<00:02:38.450> exploit<00:02:38.930> in 00:02:39.070 --> 00:02:39.080 align:start position:0% operations so of course the exploit in 00:02:39.080 --> 00:02:41.290 align:start position:0% operations so of course the exploit in the<00:02:39.170> multi<00:02:39.410> sick<00:02:39.590> party<00:02:39.950> bug<00:02:40.160> was<00:02:40.670> much<00:02:41.000> more 00:02:41.290 --> 00:02:41.300 align:start position:0% the multi sick party bug was much more 00:02:41.300 --> 00:02:43.330 align:start position:0% the multi sick party bug was much more complicated<00:02:41.690> because<00:02:42.410> the<00:02:42.650> contract<00:02:43.070> itself 00:02:43.330 --> 00:02:43.340 align:start position:0% complicated because the contract itself 00:02:43.340 --> 00:02:46.080 align:start position:0% complicated because the contract itself was<00:02:43.580> more<00:02:43.790> sophisticated<00:02:44.420> but<00:02:44.990> the<00:02:45.560> basic 00:02:46.080 --> 00:02:46.090 align:start position:0% was more sophisticated but the basic 00:02:46.090 --> 00:02:50.800 align:start position:0% was more sophisticated but the basic vulnerability<00:02:47.090> is<00:02:47.270> the<00:02:47.360> same<00:02:49.270> so<00:02:50.270> there<00:02:50.720> are 00:02:50.800 --> 00:02:50.810 align:start position:0% vulnerability is the same so there are 00:02:50.810 --> 00:02:52.270 align:start position:0% vulnerability is the same so there are many<00:02:51.140> more<00:02:51.350> security<00:02:51.890> bugs<00:02:52.100> that<00:02:52.190> are 00:02:52.270 --> 00:02:52.280 align:start position:0% many more security bugs that are 00:02:52.280 --> 00:02:54.580 align:start position:0% many more security bugs that are possible<00:02:52.670> with<00:02:52.850> the<00:02:52.970> etherium<00:02:53.390> platform<00:02:53.930> one 00:02:54.580 --> 00:02:54.590 align:start position:0% possible with the etherium platform one 00:02:54.590 --> 00:02:57.100 align:start position:0% possible with the etherium platform one of<00:02:54.680> them<00:02:54.860> is<00:02:55.010> the<00:02:55.520> category<00:02:56.330> of<00:02:56.420> unexpected 00:02:57.100 --> 00:02:57.110 align:start position:0% of them is the category of unexpected 00:02:57.110 --> 00:02:59.170 align:start position:0% of them is the category of unexpected ether<00:02:57.440> flows<00:02:57.680> for<00:02:58.220> instance<00:02:58.490> when<00:02:58.610> you<00:02:58.700> expect 00:02:59.170 --> 00:02:59.180 align:start position:0% ether flows for instance when you expect 00:02:59.180 --> 00:03:00.730 align:start position:0% ether flows for instance when you expect ether<00:02:59.480> to<00:02:59.630> go<00:02:59.780> to<00:02:59.840> your<00:03:00.020> contract<00:03:00.410> but<00:03:00.530> don't 00:03:00.730 --> 00:03:00.740 align:start position:0% ether to go to your contract but don't 00:03:00.740 --> 00:03:02.860 align:start position:0% ether to go to your contract but don't provide<00:03:01.040> any<00:03:01.310> means<00:03:01.610> to<00:03:01.850> withdraw<00:03:02.240> it<00:03:02.300> so<00:03:02.810> you 00:03:02.860 --> 00:03:02.870 align:start position:0% provide any means to withdraw it so you 00:03:02.870 --> 00:03:05.200 align:start position:0% provide any means to withdraw it so you end<00:03:03.290> up<00:03:03.380> with<00:03:03.440> locked<00:03:03.830> it<00:03:04.100> ether<00:03:04.550> in<00:03:04.760> your<00:03:04.970> in 00:03:05.200 --> 00:03:05.210 align:start position:0% end up with locked it ether in your in 00:03:05.210 --> 00:03:09.160 align:start position:0% end up with locked it ether in your in your<00:03:05.330> contract<00:03:06.970> in<00:03:07.970> secure<00:03:08.390> coding<00:03:08.750> such<00:03:09.020> as 00:03:09.160 --> 00:03:09.170 align:start position:0% your contract in secure coding such as 00:03:09.170 --> 00:03:11.530 align:start position:0% your contract in secure coding such as the<00:03:09.290> mystic<00:03:09.710> party<00:03:10.070> bug<00:03:10.250> so<00:03:10.520> providing<00:03:11.150> ways 00:03:11.530 --> 00:03:11.540 align:start position:0% the mystic party bug so providing ways 00:03:11.540 --> 00:03:13.630 align:start position:0% the mystic party bug so providing ways to<00:03:11.930> write<00:03:12.110> your<00:03:12.380> storage<00:03:12.680> without<00:03:13.190> checking 00:03:13.630 --> 00:03:13.640 align:start position:0% to write your storage without checking 00:03:13.640 --> 00:03:15.700 align:start position:0% to write your storage without checking whether<00:03:14.180> the<00:03:14.510> user<00:03:14.780> should<00:03:15.140> be<00:03:15.170> able<00:03:15.290> to<00:03:15.500> do 00:03:15.700 --> 00:03:15.710 align:start position:0% whether the user should be able to do 00:03:15.710 --> 00:03:18.970 align:start position:0% whether the user should be able to do that<00:03:15.860> or<00:03:15.980> not<00:03:16.780> the<00:03:17.780> use<00:03:17.930> of<00:03:18.110> and<00:03:18.290> safe<00:03:18.440> input 00:03:18.970 --> 00:03:18.980 align:start position:0% that or not the use of and safe input 00:03:18.980 --> 00:03:21.010 align:start position:0% that or not the use of and safe input whenever<00:03:19.280> you<00:03:19.550> use<00:03:19.580> for<00:03:20.030> instance<00:03:20.209> timestamp 00:03:21.010 --> 00:03:21.020 align:start position:0% whenever you use for instance timestamp 00:03:21.020 --> 00:03:23.470 align:start position:0% whenever you use for instance timestamp or<00:03:21.140> block<00:03:21.380> numbers<00:03:21.770> and<00:03:22.010> pretend<00:03:23.000> that<00:03:23.030> these 00:03:23.470 --> 00:03:23.480 align:start position:0% or block numbers and pretend that these 00:03:23.480 --> 00:03:26.890 align:start position:0% or block numbers and pretend that these are<00:03:23.720> random<00:03:24.250> variables<00:03:25.250> and<00:03:25.459> even<00:03:26.300> feed<00:03:26.660> them 00:03:26.890 --> 00:03:26.900 align:start position:0% are random variables and even feed them 00:03:26.900 --> 00:03:29.050 align:start position:0% are random variables and even feed them into<00:03:27.080> cryptographic<00:03:27.560> functions<00:03:28.060> for 00:03:29.050 --> 00:03:29.060 align:start position:0% into cryptographic functions for 00:03:29.060 --> 00:03:30.280 align:start position:0% into cryptographic functions for instance<00:03:29.120> to<00:03:29.420> create<00:03:29.540> a<00:03:29.690> pseudo-random 00:03:30.280 --> 00:03:30.290 align:start position:0% instance to create a pseudo-random 00:03:30.290 --> 00:03:32.590 align:start position:0% instance to create a pseudo-random generator<00:03:31.040> then<00:03:31.430> this<00:03:31.760> is<00:03:31.910> bound<00:03:32.120> to<00:03:32.240> failure 00:03:32.590 --> 00:03:32.600 align:start position:0% generator then this is bound to failure 00:03:32.600 --> 00:03:36.730 align:start position:0% generator then this is bound to failure because<00:03:32.990> these<00:03:33.470> variables<00:03:33.980> can<00:03:34.160> be<00:03:34.240> biased<00:03:35.740> by 00:03:36.730 --> 00:03:36.740 align:start position:0% because these variables can be biased by 00:03:36.740 --> 00:03:39.250 align:start position:0% because these variables can be biased by miners<00:03:37.370> so<00:03:37.910> for<00:03:38.120> instance<00:03:38.390> a<00:03:38.630> miner<00:03:38.900> can 00:03:39.250 --> 00:03:39.260 align:start position:0% miners so for instance a miner can 00:03:39.260 --> 00:03:41.140 align:start position:0% miners so for instance a miner can decide<00:03:39.620> to<00:03:40.160> not<00:03:40.459> to<00:03:40.640> process<00:03:41.000> your 00:03:41.140 --> 00:03:41.150 align:start position:0% decide to not to process your 00:03:41.150 --> 00:03:43.180 align:start position:0% decide to not to process your transaction<00:03:41.630> right<00:03:41.810> away<00:03:42.110> and<00:03:42.320> this<00:03:42.709> is<00:03:42.770> going 00:03:43.180 --> 00:03:43.190 align:start position:0% transaction right away and this is going 00:03:43.190 --> 00:03:44.560 align:start position:0% transaction right away and this is going to<00:03:43.250> be<00:03:43.370> delayed<00:03:43.610> by<00:03:43.790> at<00:03:43.850> least<00:03:44.030> one<00:03:44.330> block 00:03:44.560 --> 00:03:44.570 align:start position:0% to be delayed by at least one block 00:03:44.570 --> 00:03:48.270 align:start position:0% to be delayed by at least one block which<00:03:44.870> gonna<00:03:45.110> result<00:03:45.680> in<00:03:45.830> a<00:03:45.980> higher<00:03:46.190> timestamp 00:03:48.270 --> 00:03:48.280 align:start position:0% which gonna result in a higher timestamp 00:03:48.280 --> 00:03:50.290 align:start position:0% which gonna result in a higher timestamp reinsured<00:03:49.280> method<00:03:49.640> call<00:03:49.850> so<00:03:49.970> this<00:03:50.120> is 00:03:50.290 --> 00:03:50.300 align:start position:0% reinsured method call so this is 00:03:50.300 --> 00:03:54.640 align:start position:0% reinsured method call so this is basically<00:03:50.630> the<00:03:50.840> DAO<00:03:51.230> bug<00:03:51.650> and<00:03:53.650> manipulating 00:03:54.640 --> 00:03:54.650 align:start position:0% basically the DAO bug and manipulating 00:03:54.650 --> 00:03:56.949 align:start position:0% basically the DAO bug and manipulating ether<00:03:54.980> flows<00:03:55.250> by<00:03:55.580> a<00:03:55.610> transaction<00:03:56.240> reordering 00:03:56.949 --> 00:03:56.959 align:start position:0% ether flows by a transaction reordering 00:03:56.959 --> 00:03:58.690 align:start position:0% ether flows by a transaction reordering so<00:03:57.080> this<00:03:57.230> is<00:03:57.380> a<00:03:57.560> bit<00:03:57.740> specific<00:03:58.220> to<00:03:58.340> the<00:03:58.490> a 00:03:58.690 --> 00:03:58.700 align:start position:0% so this is a bit specific to the a 00:03:58.700 --> 00:04:01.120 align:start position:0% so this is a bit specific to the a theorem<00:03:59.030> platform<00:03:59.510> where<00:04:00.350> all<00:04:00.590> the 00:04:01.120 --> 00:04:01.130 align:start position:0% theorem platform where all the 00:04:01.130 --> 00:04:05.260 align:start position:0% theorem platform where all the transaction<00:04:01.610> can<00:04:01.790> African<00:04:03.970> where<00:04:04.970> all<00:04:05.150> the 00:04:05.260 --> 00:04:05.270 align:start position:0% transaction can African where all the 00:04:05.270 --> 00:04:07.060 align:start position:0% transaction can African where all the transaction<00:04:05.750> can<00:04:05.959> can<00:04:06.500> be<00:04:06.620> processed 00:04:07.060 --> 00:04:07.070 align:start position:0% transaction can can be processed 00:04:07.070 --> 00:04:10.330 align:start position:0% transaction can can be processed concurrently<00:04:08.000> so<00:04:08.709> for<00:04:09.709> the<00:04:09.800> details<00:04:10.100> of<00:04:10.250> this 00:04:10.330 --> 00:04:10.340 align:start position:0% concurrently so for the details of this 00:04:10.340 --> 00:04:12.699 align:start position:0% concurrently so for the details of this one<00:04:10.550> I<00:04:10.580> have<00:04:10.790> another<00:04:11.209> toy<00:04:11.690> example<00:04:12.230> this 00:04:12.699 --> 00:04:12.709 align:start position:0% one I have another toy example this 00:04:12.709 --> 00:04:14.320 align:start position:0% one I have another toy example this token<00:04:13.160> contract<00:04:13.550> where<00:04:13.730> you<00:04:13.820> have<00:04:14.000> two 00:04:14.320 --> 00:04:14.330 align:start position:0% token contract where you have two 00:04:14.330 --> 00:04:17.590 align:start position:0% token contract where you have two storage<00:04:14.660> variables<00:04:15.489> one<00:04:16.489> is<00:04:16.520> the<00:04:17.060> price<00:04:17.299> of 00:04:17.590 --> 00:04:17.600 align:start position:0% storage variables one is the price of 00:04:17.600 --> 00:04:19.840 align:start position:0% storage variables one is the price of this<00:04:17.810> token<00:04:18.200> and<00:04:18.410> the<00:04:18.620> other<00:04:18.709> is<00:04:18.980> the<00:04:19.160> the 00:04:19.840 --> 00:04:19.850 align:start position:0% this token and the other is the the 00:04:19.850 --> 00:04:23.200 align:start position:0% this token and the other is the the owner<00:04:20.060> of<00:04:20.419> this<00:04:21.200> contract<00:04:21.680> and<00:04:21.910> so<00:04:22.910> you<00:04:22.970> can 00:04:23.200 --> 00:04:23.210 align:start position:0% owner of this contract and so you can 00:04:23.210 --> 00:04:25.320 align:start position:0% owner of this contract and so you can set<00:04:23.450> the<00:04:23.570> price<00:04:23.810> where<00:04:24.350> only<00:04:24.650> the<00:04:24.860> owner<00:04:25.010> can 00:04:25.320 --> 00:04:25.330 align:start position:0% set the price where only the owner can 00:04:25.330 --> 00:04:28.959 align:start position:0% set the price where only the owner can can<00:04:26.330> can<00:04:26.990> change<00:04:27.350> this<00:04:27.979> price<00:04:28.280> and 00:04:28.959 --> 00:04:28.969 align:start position:0% can can change this price and 00:04:28.969 --> 00:04:30.609 align:start position:0% can can change this price and the<00:04:29.059> second<00:04:29.329> one<00:04:29.479> is<00:04:29.659> a<00:04:29.689> cell<00:04:30.049> token<00:04:30.409> where 00:04:30.609 --> 00:04:30.619 align:start position:0% the second one is a cell token where 00:04:30.619 --> 00:04:34.479 align:start position:0% the second one is a cell token where some<00:04:31.159> ether<00:04:31.309> is<00:04:31.939> transferred<00:04:33.039> as<00:04:34.039> you<00:04:34.189> can<00:04:34.339> as 00:04:34.479 --> 00:04:34.489 align:start position:0% some ether is transferred as you can as 00:04:34.489 --> 00:04:37.029 align:start position:0% some ether is transferred as you can as you<00:04:34.519> can<00:04:34.729> see<00:04:34.909> here<00:04:35.119> a<00:04:35.329> user<00:04:35.689> can<00:04:35.929> can<00:04:36.649> call 00:04:37.029 --> 00:04:37.039 align:start position:0% you can see here a user can can call 00:04:37.039 --> 00:04:39.039 align:start position:0% you can see here a user can can call this<00:04:37.159> function<00:04:37.269> according<00:04:38.269> to<00:04:38.509> a<00:04:38.629> given<00:04:38.839> price 00:04:39.039 --> 00:04:39.049 align:start position:0% this function according to a given price 00:04:39.049 --> 00:04:41.289 align:start position:0% this function according to a given price so<00:04:39.229> what<00:04:39.379> happens<00:04:39.799> in<00:04:39.949> practice<00:04:40.129> that<00:04:40.519> a<00:04:40.759> user 00:04:41.289 --> 00:04:41.299 align:start position:0% so what happens in practice that a user 00:04:41.299 --> 00:04:43.119 align:start position:0% so what happens in practice that a user can<00:04:41.479> read<00:04:41.659> the<00:04:41.839> price<00:04:42.349> variable<00:04:42.829> on<00:04:43.069> the 00:04:43.119 --> 00:04:43.129 align:start position:0% can read the price variable on the 00:04:43.129 --> 00:04:45.339 align:start position:0% can read the price variable on the blockchain<00:04:43.429> everything<00:04:44.329> is<00:04:44.479> public<00:04:44.959> and<00:04:45.289> you 00:04:45.339 --> 00:04:45.349 align:start position:0% blockchain everything is public and you 00:04:45.349 --> 00:04:47.439 align:start position:0% blockchain everything is public and you don't<00:04:45.559> even<00:04:45.649> you<00:04:46.069> don't<00:04:46.189> even<00:04:46.339> need<00:04:46.819> to<00:04:46.879> create 00:04:47.439 --> 00:04:47.449 align:start position:0% don't even you don't even need to create 00:04:47.449 --> 00:04:49.899 align:start position:0% don't even you don't even need to create a<00:04:47.479> transaction<00:04:47.899> to<00:04:48.619> read<00:04:48.799> the<00:04:49.429> value<00:04:49.669> of<00:04:49.759> this 00:04:49.899 --> 00:04:49.909 align:start position:0% a transaction to read the value of this 00:04:49.909 --> 00:04:52.629 align:start position:0% a transaction to read the value of this variable<00:04:50.439> but<00:04:51.439> what<00:04:51.799> happens<00:04:52.099> here<00:04:52.429> is<00:04:52.579> that 00:04:52.629 --> 00:04:52.639 align:start position:0% variable but what happens here is that 00:04:52.639 --> 00:04:55.350 align:start position:0% variable but what happens here is that once<00:04:53.360> a<00:04:53.479> user<00:04:53.689> decide<00:04:54.169> to<00:04:54.349> call<00:04:54.949> this<00:04:55.129> function 00:04:55.350 --> 00:04:55.360 align:start position:0% once a user decide to call this function 00:04:55.360 --> 00:04:58.029 align:start position:0% once a user decide to call this function the<00:04:56.360> owner<00:04:56.509> can<00:04:56.839> still<00:04:57.110> call<00:04:57.799> another 00:04:58.029 --> 00:04:58.039 align:start position:0% the owner can still call another 00:04:58.039 --> 00:04:59.889 align:start position:0% the owner can still call another function<00:04:58.129> so<00:04:58.579> what<00:04:59.179> would<00:04:59.329> happen<00:04:59.569> is<00:04:59.869> that 00:04:59.889 --> 00:04:59.899 align:start position:0% function so what would happen is that 00:04:59.899 --> 00:05:01.959 align:start position:0% function so what would happen is that the<00:05:00.649> owner<00:05:00.829> would<00:05:01.219> realize<00:05:01.579> that<00:05:01.729> there<00:05:01.849> is<00:05:01.879> a 00:05:01.959 --> 00:05:01.969 align:start position:0% the owner would realize that there is a 00:05:01.969 --> 00:05:04.839 align:start position:0% the owner would realize that there is a transaction<00:05:02.360> pending<00:05:02.929> with<00:05:03.169> this<00:05:03.849> this 00:05:04.839 --> 00:05:04.849 align:start position:0% transaction pending with this this 00:05:04.849 --> 00:05:06.819 align:start position:0% transaction pending with this this function<00:05:05.059> and<00:05:05.629> then<00:05:05.929> this<00:05:06.139> side<00:05:06.319> okay<00:05:06.559> maybe<00:05:06.739> I 00:05:06.819 --> 00:05:06.829 align:start position:0% function and then this side okay maybe I 00:05:06.829 --> 00:05:09.399 align:start position:0% function and then this side okay maybe I want<00:05:07.009> to<00:05:07.039> increase<00:05:07.309> the<00:05:07.399> price<00:05:07.639> or<00:05:08.199> lower<00:05:09.199> the 00:05:09.399 --> 00:05:09.409 align:start position:0% want to increase the price or lower the 00:05:09.409 --> 00:05:11.049 align:start position:0% want to increase the price or lower the price<00:05:09.619> depending<00:05:10.129> on<00:05:10.279> what<00:05:10.519> he<00:05:10.610> wants<00:05:10.819> to<00:05:10.939> do 00:05:11.049 --> 00:05:11.059 align:start position:0% price depending on what he wants to do 00:05:11.059 --> 00:05:13.119 align:start position:0% price depending on what he wants to do so<00:05:11.659> the<00:05:12.139> thing<00:05:12.349> is<00:05:12.379> when<00:05:12.860> you<00:05:12.979> have<00:05:13.099> a 00:05:13.119 --> 00:05:13.129 align:start position:0% so the thing is when you have a 00:05:13.129 --> 00:05:14.259 align:start position:0% so the thing is when you have a transaction<00:05:13.489> pending<00:05:13.939> you<00:05:14.029> have<00:05:14.119> no 00:05:14.259 --> 00:05:14.269 align:start position:0% transaction pending you have no 00:05:14.269 --> 00:05:16.449 align:start position:0% transaction pending you have no guarantee<00:05:14.779> that<00:05:15.019> it's<00:05:15.559> going<00:05:15.739> to<00:05:15.799> be<00:05:15.919> executed 00:05:16.449 --> 00:05:16.459 align:start position:0% guarantee that it's going to be executed 00:05:16.459 --> 00:05:19.089 align:start position:0% guarantee that it's going to be executed within<00:05:16.699> the<00:05:17.029> context<00:05:17.599> that<00:05:18.409> you<00:05:18.649> that<00:05:18.979> you 00:05:19.089 --> 00:05:19.099 align:start position:0% within the context that you that you 00:05:19.099 --> 00:05:22.600 align:start position:0% within the context that you that you just<00:05:19.309> read<00:05:19.549> and<00:05:21.009> so<00:05:22.009> in<00:05:22.129> a<00:05:22.219> sense<00:05:22.369> the<00:05:22.579> two 00:05:22.600 --> 00:05:22.610 align:start position:0% just read and so in a sense the two 00:05:22.610 --> 00:05:24.069 align:start position:0% just read and so in a sense the two operations<00:05:23.179> do<00:05:23.360> not<00:05:23.389> commit<00:05:23.839> and<00:05:23.959> you 00:05:24.069 --> 00:05:24.079 align:start position:0% operations do not commit and you 00:05:24.079 --> 00:05:26.189 align:start position:0% operations do not commit and you shouldn't<00:05:24.349> expect<00:05:24.649> them<00:05:24.949> to<00:05:25.099> commit<00:05:25.279> either 00:05:26.189 --> 00:05:26.199 align:start position:0% shouldn't expect them to commit either 00:05:26.199 --> 00:05:30.579 align:start position:0% shouldn't expect them to commit either so<00:05:27.199> how<00:05:27.589> to<00:05:27.789> detect<00:05:28.789> this<00:05:28.969> kind<00:05:29.269> of<00:05:29.389> bugs<00:05:29.689> I'm 00:05:30.579 --> 00:05:30.589 align:start position:0% so how to detect this kind of bugs I'm 00:05:30.589 --> 00:05:31.989 align:start position:0% so how to detect this kind of bugs I'm going<00:05:30.799> to<00:05:30.860> talk<00:05:31.009> about<00:05:31.129> automated<00:05:31.819> security 00:05:31.989 --> 00:05:31.999 align:start position:0% going to talk about automated security 00:05:31.999 --> 00:05:34.299 align:start position:0% going to talk about automated security analysis<00:05:32.659> as<00:05:32.839> a<00:05:32.869> way<00:05:33.169> to<00:05:33.229> make<00:05:33.919> sure<00:05:34.099> that 00:05:34.299 --> 00:05:34.309 align:start position:0% analysis as a way to make sure that 00:05:34.309 --> 00:05:37.389 align:start position:0% analysis as a way to make sure that these<00:05:34.789> bugs<00:05:35.269> are<00:05:35.989> not<00:05:36.559> implemented<00:05:37.159> in<00:05:37.279> your 00:05:37.389 --> 00:05:37.399 align:start position:0% these bugs are not implemented in your 00:05:37.399 --> 00:05:40.749 align:start position:0% these bugs are not implemented in your contracts<00:05:37.839> so<00:05:38.839> if<00:05:39.079> I<00:05:39.229> were<00:05:39.319> to<00:05:39.469> draw<00:05:39.709> a<00:05:40.339> big 00:05:40.749 --> 00:05:40.759 align:start position:0% contracts so if I were to draw a big 00:05:40.759 --> 00:05:42.519 align:start position:0% contracts so if I were to draw a big drawing<00:05:40.999> of<00:05:41.209> all<00:05:41.389> the<00:05:41.539> possible<00:05:41.929> behaviors 00:05:42.519 --> 00:05:42.529 align:start position:0% drawing of all the possible behaviors 00:05:42.529 --> 00:05:45.609 align:start position:0% drawing of all the possible behaviors and<00:05:42.769> I<00:05:43.459> would<00:05:44.209> I<00:05:44.389> would<00:05:44.599> have<00:05:44.779> some<00:05:45.139> something 00:05:45.609 --> 00:05:45.619 align:start position:0% and I would I would have some something 00:05:45.619 --> 00:05:47.079 align:start position:0% and I would I would have some something with<00:05:45.739> all<00:05:45.919> the<00:05:46.069> possible<00:05:46.429> behaviors<00:05:46.579> and 00:05:47.079 --> 00:05:47.089 align:start position:0% with all the possible behaviors and 00:05:47.089 --> 00:05:49.479 align:start position:0% with all the possible behaviors and within<00:05:47.300> them<00:05:47.629> a<00:05:47.869> lot<00:05:48.499> of<00:05:48.679> security<00:05:48.979> bugs<00:05:49.369> that 00:05:49.479 --> 00:05:49.489 align:start position:0% within them a lot of security bugs that 00:05:49.489 --> 00:05:51.339 align:start position:0% within them a lot of security bugs that you<00:05:49.639> want<00:05:49.819> to<00:05:49.909> avoid<00:05:50.149> when<00:05:50.719> implementing 00:05:51.339 --> 00:05:51.349 align:start position:0% you want to avoid when implementing 00:05:51.349 --> 00:05:55.059 align:start position:0% you want to avoid when implementing smart<00:05:51.499> contracts<00:05:53.139> the<00:05:54.139> problem<00:05:54.499> is<00:05:54.649> that<00:05:54.860> you 00:05:55.059 --> 00:05:55.069 align:start position:0% smart contracts the problem is that you 00:05:55.069 --> 00:05:56.979 align:start position:0% smart contracts the problem is that you cannot<00:05:55.279> enumerate<00:05:55.789> all<00:05:56.029> possible<00:05:56.059> behaviors 00:05:56.979 --> 00:05:56.989 align:start position:0% cannot enumerate all possible behaviors 00:05:56.989 --> 00:05:59.079 align:start position:0% cannot enumerate all possible behaviors for<00:05:57.349> instance<00:05:57.649> if<00:05:57.829> you<00:05:57.979> have<00:05:58.099> an<00:05:58.309> earning<00:05:58.909> an 00:05:59.079 --> 00:05:59.089 align:start position:0% for instance if you have an earning an 00:05:59.089 --> 00:06:01.239 align:start position:0% for instance if you have an earning an integer<00:05:59.419> argument<00:06:00.349> in<00:06:00.469> your<00:06:00.619> function<00:06:00.889> it's 00:06:01.239 --> 00:06:01.249 align:start position:0% integer argument in your function it's 00:06:01.249 --> 00:06:03.669 align:start position:0% integer argument in your function it's going<00:06:01.339> to<00:06:01.489> be<00:06:01.579> you<00:06:02.239> cannot<00:06:02.559> call<00:06:03.559> this 00:06:03.669 --> 00:06:03.679 align:start position:0% going to be you cannot call this 00:06:03.679 --> 00:06:05.679 align:start position:0% going to be you cannot call this function<00:06:04.129> with<00:06:04.309> all<00:06:04.459> possible<00:06:04.729> integers<00:06:05.479> and 00:06:05.679 --> 00:06:05.689 align:start position:0% function with all possible integers and 00:06:05.689 --> 00:06:08.889 align:start position:0% function with all possible integers and just<00:06:06.199> say<00:06:06.439> ok<00:06:06.739> this<00:06:06.860> this<00:06:07.189> trace<00:06:07.639> is<00:06:07.909> faulty<00:06:08.329> so 00:06:08.889 --> 00:06:08.899 align:start position:0% just say ok this this trace is faulty so 00:06:08.899 --> 00:06:10.600 align:start position:0% just say ok this this trace is faulty so at<00:06:09.259> one<00:06:09.439> point<00:06:09.469> you<00:06:09.679> have<00:06:09.799> to<00:06:10.009> make<00:06:10.309> a<00:06:10.339> trade 00:06:10.600 --> 00:06:10.610 align:start position:0% at one point you have to make a trade 00:06:10.610 --> 00:06:15.069 align:start position:0% at one point you have to make a trade off<00:06:10.759> and<00:06:10.969> decide<00:06:11.269> how<00:06:12.019> to<00:06:12.549> to<00:06:13.549> find<00:06:14.029> the<00:06:14.179> bad 00:06:15.069 --> 00:06:15.079 align:start position:0% off and decide how to to find the bad 00:06:15.079 --> 00:06:19.209 align:start position:0% off and decide how to to find the bad behaviors<00:06:16.299> so<00:06:17.299> the<00:06:17.539> different<00:06:18.219> security 00:06:19.209 --> 00:06:19.219 align:start position:0% behaviors so the different security 00:06:19.219 --> 00:06:21.429 align:start position:0% behaviors so the different security analysis<00:06:20.089> approaches<00:06:20.599> that<00:06:20.959> you<00:06:21.110> can<00:06:21.229> have 00:06:21.429 --> 00:06:21.439 align:start position:0% analysis approaches that you can have 00:06:21.439 --> 00:06:25.149 align:start position:0% analysis approaches that you can have are<00:06:22.369> here<00:06:23.469> represented<00:06:24.469> so<00:06:24.619> the<00:06:24.739> first<00:06:24.949> one 00:06:25.149 --> 00:06:25.159 align:start position:0% are here represented so the first one 00:06:25.159 --> 00:06:29.109 align:start position:0% are here represented so the first one would<00:06:25.339> be<00:06:25.689> testing<00:06:26.769> where<00:06:27.769> you<00:06:28.249> actually<00:06:28.399> try 00:06:29.109 --> 00:06:29.119 align:start position:0% would be testing where you actually try 00:06:29.119 --> 00:06:32.229 align:start position:0% would be testing where you actually try to<00:06:29.229> cover<00:06:30.229> one<00:06:30.529> path<00:06:30.829> and<00:06:31.069> from<00:06:31.519> this<00:06:31.759> one<00:06:32.029> path 00:06:32.229 --> 00:06:32.239 align:start position:0% to cover one path and from this one path 00:06:32.239 --> 00:06:36.729 align:start position:0% to cover one path and from this one path you<00:06:32.329> can<00:06:32.479> extract<00:06:32.869> one<00:06:33.679> trace<00:06:33.949> and<00:06:34.489> try<00:06:35.209> to<00:06:35.269> -<00:06:35.839> - 00:06:36.729 --> 00:06:36.739 align:start position:0% you can extract one trace and try to - - 00:06:36.739 --> 00:06:39.519 align:start position:0% you can extract one trace and try to - - to<00:06:37.519> check<00:06:37.759> whether<00:06:37.999> or<00:06:38.419> not<00:06:38.629> it's<00:06:38.869> faulty<00:06:39.289> and 00:06:39.519 --> 00:06:39.529 align:start position:0% to check whether or not it's faulty and 00:06:39.529 --> 00:06:41.589 align:start position:0% to check whether or not it's faulty and whether<00:06:39.949> or<00:06:40.099> not<00:06:40.159> it<00:06:40.759> corresponds<00:06:41.300> to<00:06:41.389> what 00:06:41.589 --> 00:06:41.599 align:start position:0% whether or not it corresponds to what 00:06:41.599 --> 00:06:42.820 align:start position:0% whether or not it corresponds to what you<00:06:41.719> expected 00:06:42.820 --> 00:06:42.830 align:start position:0% you expected 00:06:42.830 --> 00:06:46.659 align:start position:0% you expected dynamic<00:06:43.430> symbolic<00:06:43.789> analysis<00:06:44.419> which<00:06:45.349> is<00:06:45.889> an 00:06:46.659 --> 00:06:46.669 align:start position:0% dynamic symbolic analysis which is an 00:06:46.669 --> 00:06:50.230 align:start position:0% dynamic symbolic analysis which is an improvement<00:06:47.060> on<00:06:48.340> basic<00:06:49.340> tasting<00:06:49.729> because 00:06:50.230 --> 00:06:50.240 align:start position:0% improvement on basic tasting because 00:06:50.240 --> 00:06:52.540 align:start position:0% improvement on basic tasting because you're<00:06:50.419> not<00:06:50.569> able<00:06:50.780> to<00:06:51.110> cover<00:06:51.319> way<00:06:52.039> many<00:06:52.460> more 00:06:52.540 --> 00:06:52.550 align:start position:0% you're not able to cover way many more 00:06:52.550 --> 00:06:56.379 align:start position:0% you're not able to cover way many more paths<00:06:52.940> so<00:06:53.659> this<00:06:54.110> is<00:06:54.289> a<00:06:54.530> bit<00:06:55.030> testing<00:06:56.030> plus 00:06:56.379 --> 00:06:56.389 align:start position:0% paths so this is a bit testing plus 00:06:56.389 --> 00:06:58.659 align:start position:0% paths so this is a bit testing plus purse<00:06:56.599> if<00:06:56.780> you<00:06:56.900> want<00:06:57.080> and<00:06:57.319> so<00:06:58.310> you<00:06:58.370> have<00:06:58.580> the 00:06:58.659 --> 00:06:58.669 align:start position:0% purse if you want and so you have the 00:06:58.669 --> 00:07:01.330 align:start position:0% purse if you want and so you have the same<00:06:58.849> kind<00:06:59.030> of<00:06:59.090> guarantees<00:06:59.539> that<00:06:59.960> is<00:07:00.500> testing 00:07:01.330 --> 00:07:01.340 align:start position:0% same kind of guarantees that is testing 00:07:01.340 --> 00:07:03.730 align:start position:0% same kind of guarantees that is testing and<00:07:01.550> dynamic<00:07:01.970> analysis<00:07:02.479> report<00:07:03.199> through<00:07:03.500> bugs 00:07:03.730 --> 00:07:03.740 align:start position:0% and dynamic analysis report through bugs 00:07:03.740 --> 00:07:04.960 align:start position:0% and dynamic analysis report through bugs that<00:07:03.889> actually<00:07:04.220> exist<00:07:04.460> in<00:07:04.550> your<00:07:04.759> in<00:07:04.940> your 00:07:04.960 --> 00:07:04.970 align:start position:0% that actually exist in your in your 00:07:04.970 --> 00:07:06.760 align:start position:0% that actually exist in your in your codes<00:07:05.300> and<00:07:05.539> say<00:07:05.750> they<00:07:06.229> provide<00:07:06.500> you<00:07:06.620> with 00:07:06.760 --> 00:07:06.770 align:start position:0% codes and say they provide you with 00:07:06.770 --> 00:07:10.240 align:start position:0% codes and say they provide you with traces<00:07:07.340> of<00:07:07.520> what<00:07:08.060> happened<00:07:08.599> and<00:07:08.949> put<00:07:09.949> the<00:07:10.069> can 00:07:10.240 --> 00:07:10.250 align:start position:0% traces of what happened and put the can 00:07:10.250 --> 00:07:11.740 align:start position:0% traces of what happened and put the can still<00:07:10.490> miss<00:07:10.669> bugs<00:07:10.940> because<00:07:11.210> your<00:07:11.330> evolution 00:07:11.740 --> 00:07:11.750 align:start position:0% still miss bugs because your evolution 00:07:11.750 --> 00:07:13.990 align:start position:0% still miss bugs because your evolution of<00:07:11.990> code<00:07:12.289> coverage<00:07:12.650> which<00:07:13.220> is<00:07:13.400> not<00:07:13.580> equal<00:07:13.699> to 00:07:13.990 --> 00:07:14.000 align:start position:0% of code coverage which is not equal to 00:07:14.000 --> 00:07:17.050 align:start position:0% of code coverage which is not equal to 100%<00:07:14.419> so<00:07:14.990> this<00:07:15.889> is<00:07:16.069> a<00:07:16.250> problem<00:07:16.729> because<00:07:16.819> you 00:07:17.050 --> 00:07:17.060 align:start position:0% 100% so this is a problem because you 00:07:17.060 --> 00:07:19.719 align:start position:0% 100% so this is a problem because you can<00:07:17.569> never<00:07:17.750> be<00:07:17.900> sure<00:07:18.159> unless<00:07:19.159> you<00:07:19.430> have<00:07:19.520> caught 00:07:19.719 --> 00:07:19.729 align:start position:0% can never be sure unless you have caught 00:07:19.729 --> 00:07:22.420 align:start position:0% can never be sure unless you have caught you<00:07:20.210> have<00:07:20.330> covered<00:07:20.629> all<00:07:20.780> your<00:07:21.050> on<00:07:22.039> your<00:07:22.190> codes 00:07:22.420 --> 00:07:22.430 align:start position:0% you have covered all your on your codes 00:07:22.430 --> 00:07:24.670 align:start position:0% you have covered all your on your codes and<00:07:22.669> that<00:07:22.759> is<00:07:22.909> 100%<00:07:23.389> coverage<00:07:23.870> you<00:07:24.289> can<00:07:24.440> never 00:07:24.670 --> 00:07:24.680 align:start position:0% and that is 100% coverage you can never 00:07:24.680 --> 00:07:27.010 align:start position:0% and that is 100% coverage you can never be<00:07:24.860> sure<00:07:25.009> that<00:07:25.250> your<00:07:26.150> code<00:07:26.449> doesn't<00:07:26.629> contain 00:07:27.010 --> 00:07:27.020 align:start position:0% be sure that your code doesn't contain 00:07:27.020 --> 00:07:29.469 align:start position:0% be sure that your code doesn't contain any<00:07:27.289> of<00:07:27.409> these<00:07:27.590> bugs<00:07:27.860> and<00:07:28.340> the<00:07:29.030> last<00:07:29.180> one<00:07:29.360> in 00:07:29.469 --> 00:07:29.479 align:start position:0% any of these bugs and the last one in 00:07:29.479 --> 00:07:31.779 align:start position:0% any of these bugs and the last one in the<00:07:29.569> focus<00:07:29.870> of<00:07:29.990> my<00:07:30.139> talk<00:07:30.169> today<00:07:30.500> is<00:07:30.889> automated 00:07:31.779 --> 00:07:31.789 align:start position:0% the focus of my talk today is automated 00:07:31.789 --> 00:07:34.330 align:start position:0% the focus of my talk today is automated verification<00:07:32.509> which<00:07:33.349> makes<00:07:33.830> a<00:07:33.979> different 00:07:34.330 --> 00:07:34.340 align:start position:0% verification which makes a different 00:07:34.340 --> 00:07:36.550 align:start position:0% verification which makes a different trait<00:07:34.520> of<00:07:34.550> that<00:07:35.060> is<00:07:35.210> it<00:07:35.629> can<00:07:35.840> report<00:07:36.199> false 00:07:36.550 --> 00:07:36.560 align:start position:0% trait of that is it can report false 00:07:36.560 --> 00:07:41.320 align:start position:0% trait of that is it can report false alarms<00:07:37.039> but<00:07:37.610> it<00:07:37.729> has<00:07:37.849> no<00:07:38.060> missed<00:07:38.300> bugs<00:07:40.180> so<00:07:41.180> it 00:07:41.320 --> 00:07:41.330 align:start position:0% alarms but it has no missed bugs so it 00:07:41.330 --> 00:07:43.899 align:start position:0% alarms but it has no missed bugs so it is<00:07:41.419> a<00:07:41.449> current<00:07:42.020> state<00:07:42.139> of<00:07:42.199> the<00:07:42.440> art<00:07:42.789> for<00:07:43.789> the 00:07:43.899 --> 00:07:43.909 align:start position:0% is a current state of the art for the 00:07:43.909 --> 00:07:45.820 align:start position:0% is a current state of the art for the Ihram<00:07:44.449> platform<00:07:45.020> what<00:07:45.199> do<00:07:45.259> we<00:07:45.349> have<00:07:45.560> what 00:07:45.820 --> 00:07:45.830 align:start position:0% Ihram platform what do we have what 00:07:45.830 --> 00:07:47.950 align:start position:0% Ihram platform what do we have what tools<00:07:46.009> do<00:07:46.099> we<00:07:46.159> have<00:07:46.400> and<00:07:46.669> why<00:07:47.330> do<00:07:47.389> i<00:07:47.479> suggest 00:07:47.950 --> 00:07:47.960 align:start position:0% tools do we have and why do i suggest 00:07:47.960 --> 00:07:50.920 align:start position:0% tools do we have and why do i suggest today<00:07:48.699> so<00:07:49.699> on<00:07:49.940> the<00:07:50.060> testing<00:07:50.419> side<00:07:50.449> we<00:07:50.810> have 00:07:50.920 --> 00:07:50.930 align:start position:0% today so on the testing side we have 00:07:50.930 --> 00:07:52.330 align:start position:0% today so on the testing side we have truffle<00:07:51.259> in<00:07:51.560> populous<00:07:51.889> which<00:07:52.099> are 00:07:52.330 --> 00:07:52.340 align:start position:0% truffle in populous which are 00:07:52.340 --> 00:07:54.100 align:start position:0% truffle in populous which are respectively<00:07:52.840> JavaScript<00:07:53.840> and<00:07:53.990> Python 00:07:54.100 --> 00:07:54.110 align:start position:0% respectively JavaScript and Python 00:07:54.110 --> 00:07:56.830 align:start position:0% respectively JavaScript and Python frameworks<00:07:54.710> and<00:07:54.889> help<00:07:55.520> the<00:07:55.639> developer<00:07:56.060> to<00:07:56.270> to 00:07:56.830 --> 00:07:56.840 align:start position:0% frameworks and help the developer to to 00:07:56.840 --> 00:07:59.050 align:start position:0% frameworks and help the developer to to implement<00:07:57.349> that<00:07:57.560> constructs<00:07:57.949> and<00:07:58.219> associated 00:07:59.050 --> 00:07:59.060 align:start position:0% implement that constructs and associated 00:07:59.060 --> 00:08:02.200 align:start position:0% implement that constructs and associated test<00:07:59.449> and<00:07:59.719> deploy<00:08:00.710> them<00:08:01.099> efficiently<00:08:01.969> on<00:08:02.120> the 00:08:02.200 --> 00:08:02.210 align:start position:0% test and deploy them efficiently on the 00:08:02.210 --> 00:08:04.629 align:start position:0% test and deploy them efficiently on the local<00:08:02.479> dead<00:08:02.690> chain<00:08:02.930> and<00:08:03.139> this<00:08:03.860> way<00:08:04.099> that 00:08:04.629 --> 00:08:04.639 align:start position:0% local dead chain and this way that 00:08:04.639 --> 00:08:07.420 align:start position:0% local dead chain and this way that developer<00:08:05.150> can<00:08:05.330> run<00:08:05.630> these<00:08:06.110> traces<00:08:06.529> and<00:08:06.919> check 00:08:07.420 --> 00:08:07.430 align:start position:0% developer can run these traces and check 00:08:07.430 --> 00:08:09.360 align:start position:0% developer can run these traces and check their<00:08:07.639> assertions<00:08:08.150> in<00:08:08.659> an<00:08:08.810> efficient<00:08:09.229> manner 00:08:09.360 --> 00:08:09.370 align:start position:0% their assertions in an efficient manner 00:08:09.370 --> 00:08:14.619 align:start position:0% their assertions in an efficient manner on<00:08:11.080> dynamic<00:08:12.080> analysis<00:08:12.560> sad<00:08:13.190> you<00:08:14.090> have<00:08:14.210> a<00:08:14.360> Yenta 00:08:14.619 --> 00:08:14.629 align:start position:0% on dynamic analysis sad you have a Yenta 00:08:14.629 --> 00:08:17.709 align:start position:0% on dynamic analysis sad you have a Yenta which<00:08:14.930> was<00:08:15.080> just<00:08:15.289> presented<00:08:15.590> in<00:08:16.069> which<00:08:16.719> allows 00:08:17.709 --> 00:08:17.719 align:start position:0% which was just presented in which allows 00:08:17.719 --> 00:08:20.399 align:start position:0% which was just presented in which allows the<00:08:17.930> developer<00:08:18.319> to<00:08:18.349> cover<00:08:18.650> when<00:08:19.279> many<00:08:20.060> more 00:08:20.399 --> 00:08:20.409 align:start position:0% the developer to cover when many more 00:08:20.409 --> 00:08:23.230 align:start position:0% the developer to cover when many more many<00:08:21.409> more<00:08:21.500> paths<00:08:21.830> in<00:08:22.099> his<00:08:22.490> code<00:08:22.819> execution 00:08:23.230 --> 00:08:23.240 align:start position:0% many more paths in his code execution 00:08:23.240 --> 00:08:25.719 align:start position:0% many more paths in his code execution and<00:08:24.169> on<00:08:24.349> the<00:08:24.469> automate<00:08:24.830> automated 00:08:25.719 --> 00:08:25.729 align:start position:0% and on the automate automated 00:08:25.729 --> 00:08:27.879 align:start position:0% and on the automate automated verification<00:08:26.330> side<00:08:26.569> we<00:08:27.229> now<00:08:27.349> have<00:08:27.500> sakura 00:08:27.879 --> 00:08:27.889 align:start position:0% verification side we now have sakura 00:08:27.889 --> 00:08:30.339 align:start position:0% verification side we now have sakura Fida<00:08:28.159> i'm<00:08:28.310> presenting<00:08:28.729> today<00:08:29.000> and<00:08:29.180> which<00:08:29.569> as<00:08:30.199> i 00:08:30.339 --> 00:08:30.349 align:start position:0% Fida i'm presenting today and which as i 00:08:30.349 --> 00:08:31.930 align:start position:0% Fida i'm presenting today and which as i said<00:08:30.379> makes<00:08:30.800> a<00:08:30.919> different<00:08:31.279> trade-off<00:08:31.610> that<00:08:31.639> is 00:08:31.930 --> 00:08:31.940 align:start position:0% said makes a different trade-off that is 00:08:31.940 --> 00:08:33.850 align:start position:0% said makes a different trade-off that is it<00:08:32.360> provides<00:08:32.750> you<00:08:32.899> with<00:08:33.020> strong<00:08:33.320> guarantees 00:08:33.850 --> 00:08:33.860 align:start position:0% it provides you with strong guarantees 00:08:33.860 --> 00:08:36.490 align:start position:0% it provides you with strong guarantees at<00:08:34.010> the<00:08:34.159> bug<00:08:34.820> that<00:08:35.690> you<00:08:35.839> are<00:08:35.899> trying<00:08:36.169> to<00:08:36.289> find 00:08:36.490 --> 00:08:36.500 align:start position:0% at the bug that you are trying to find 00:08:36.500 --> 00:08:38.409 align:start position:0% at the bug that you are trying to find doesn't<00:08:36.890> exist<00:08:37.159> in<00:08:37.279> your<00:08:37.310> code<00:08:37.610> on<00:08:38.089> the<00:08:38.270> other 00:08:38.409 --> 00:08:38.419 align:start position:0% doesn't exist in your code on the other 00:08:38.419 --> 00:08:40.600 align:start position:0% doesn't exist in your code on the other hand<00:08:38.599> it<00:08:38.690> can<00:08:38.810> also<00:08:38.990> report<00:08:39.409> that<00:08:39.620> the<00:08:40.130> by<00:08:40.310> the 00:08:40.600 --> 00:08:40.610 align:start position:0% hand it can also report that the by the 00:08:40.610 --> 00:08:42.159 align:start position:0% hand it can also report that the by the bug<00:08:40.760> might<00:08:41.149> exist<00:08:41.599> in<00:08:41.750> your<00:08:41.839> code<00:08:41.990> and<00:08:42.110> then 00:08:42.159 --> 00:08:42.169 align:start position:0% bug might exist in your code and then 00:08:42.169 --> 00:08:44.500 align:start position:0% bug might exist in your code and then you<00:08:42.349> have<00:08:42.469> to<00:08:42.589> look<00:08:42.709> at<00:08:43.130> it<00:08:43.310> on<00:08:43.909> your<00:08:43.969> own<00:08:44.300> and 00:08:44.500 --> 00:08:44.510 align:start position:0% you have to look at it on your own and 00:08:44.510 --> 00:08:47.860 align:start position:0% you have to look at it on your own and tell<00:08:44.990> whether<00:08:45.230> or<00:08:45.380> not<00:08:45.560> it's<00:08:45.860> it's<00:08:46.490> here<00:08:46.870> so 00:08:47.860 --> 00:08:47.870 align:start position:0% tell whether or not it's it's here so 00:08:47.870 --> 00:08:49.569 align:start position:0% tell whether or not it's it's here so this<00:08:47.990> is<00:08:48.260> really<00:08:48.649> a<00:08:48.680> different<00:08:49.070> trade-off 00:08:49.569 --> 00:08:49.579 align:start position:0% this is really a different trade-off 00:08:49.579 --> 00:08:53.920 align:start position:0% this is really a different trade-off from<00:08:50.209> the<00:08:50.420> two<00:08:50.779> previous<00:08:51.079> categories<00:08:52.570> so<00:08:53.570> if<00:08:53.810> I 00:08:53.920 --> 00:08:53.930 align:start position:0% from the two previous categories so if I 00:08:53.930 --> 00:08:56.590 align:start position:0% from the two previous categories so if I were<00:08:54.050> to<00:08:54.290> summarize<00:08:54.740> sakura<00:08:55.459> in<00:08:55.699> a<00:08:55.790> few<00:08:56.000> words 00:08:56.590 --> 00:08:56.600 align:start position:0% were to summarize sakura in a few words 00:08:56.600 --> 00:08:58.870 align:start position:0% were to summarize sakura in a few words I<00:08:56.630> would<00:08:57.110> say<00:08:57.260> that<00:08:57.440> Sakura<00:08:58.160> is<00:08:58.490> fully 00:08:58.870 --> 00:08:58.880 align:start position:0% I would say that Sakura is fully 00:08:58.880 --> 00:09:01.000 align:start position:0% I would say that Sakura is fully automated<00:08:59.330> one<00:09:00.050> click<00:09:00.350> for<00:09:00.860> more 00:09:01.000 --> 00:09:01.010 align:start position:0% automated one click for more 00:09:01.010 --> 00:09:02.860 align:start position:0% automated one click for more verification<00:09:01.280> system<00:09:01.970> for<00:09:02.180> a<00:09:02.210> 3m<00:09:02.540> smart 00:09:02.860 --> 00:09:02.870 align:start position:0% verification system for a 3m smart 00:09:02.870 --> 00:09:06.960 align:start position:0% verification system for a 3m smart contract<00:09:04.240> so<00:09:05.240> I<00:09:05.270> prepared<00:09:05.600> a<00:09:05.720> short<00:09:05.930> demo<00:09:06.290> and 00:09:06.960 --> 00:09:06.970 align:start position:0% contract so I prepared a short demo and 00:09:06.970 --> 00:09:17.320 align:start position:0% contract so I prepared a short demo and so<00:09:07.970> I<00:09:08.000> hope<00:09:08.360> it's<00:09:08.660> gonna<00:09:08.930> work<00:09:16.000> so<00:09:17.000> this<00:09:17.120> is 00:09:17.320 --> 00:09:17.330 align:start position:0% so I hope it's gonna work so this is 00:09:17.330 --> 00:09:27.040 align:start position:0% so I hope it's gonna work so this is recorded<00:09:18.820> so<00:09:25.270> here<00:09:26.270> you<00:09:26.390> have<00:09:26.510> the<00:09:26.690> interface 00:09:27.040 --> 00:09:27.050 align:start position:0% recorded so here you have the interface 00:09:27.050 --> 00:09:29.650 align:start position:0% recorded so here you have the interface of<00:09:27.260> Sakura<00:09:28.190> Phi<00:09:28.400> you<00:09:29.030> can<00:09:29.090> see<00:09:29.330> that<00:09:29.510> by 00:09:29.650 --> 00:09:29.660 align:start position:0% of Sakura Phi you can see that by 00:09:29.660 --> 00:09:31.090 align:start position:0% of Sakura Phi you can see that by default<00:09:29.720> there<00:09:30.110> is<00:09:30.200> some<00:09:30.380> example<00:09:30.710> of 00:09:31.090 --> 00:09:31.100 align:start position:0% default there is some example of 00:09:31.100 --> 00:09:33.010 align:start position:0% default there is some example of solidity<00:09:31.490> code<00:09:31.760> so<00:09:32.060> this<00:09:32.120> is<00:09:32.330> the<00:09:32.660> website 00:09:33.010 --> 00:09:33.020 align:start position:0% solidity code so this is the website 00:09:33.020 --> 00:09:39.100 align:start position:0% solidity code so this is the website itself<00:09:36.820> so<00:09:37.820> here<00:09:38.030> you<00:09:38.120> have<00:09:38.240> a<00:09:38.300> some<00:09:38.540> solidity 00:09:39.100 --> 00:09:39.110 align:start position:0% itself so here you have a some solidity 00:09:39.110 --> 00:09:41.410 align:start position:0% itself so here you have a some solidity code<00:09:39.470> that<00:09:39.800> you<00:09:39.890> can<00:09:40.010> input<00:09:40.280> tech<00:09:40.580> so<00:09:41.180> that<00:09:41.300> you 00:09:41.410 --> 00:09:41.420 align:start position:0% code that you can input tech so that you 00:09:41.420 --> 00:09:43.090 align:start position:0% code that you can input tech so that you can<00:09:41.540> verify<00:09:41.720> it<00:09:41.990> afterwards<00:09:42.500> you<00:09:42.830> can<00:09:42.950> also 00:09:43.090 --> 00:09:43.100 align:start position:0% can verify it afterwards you can also 00:09:43.100 --> 00:09:45.430 align:start position:0% can verify it afterwards you can also feed<00:09:43.490> some<00:09:43.850> byte<00:09:44.120> code<00:09:44.390> or<00:09:44.870> you<00:09:45.140> can<00:09:45.290> also 00:09:45.430 --> 00:09:45.440 align:start position:0% feed some byte code or you can also 00:09:45.440 --> 00:09:48.160 align:start position:0% feed some byte code or you can also input<00:09:46.070> the<00:09:46.580> address<00:09:46.730> of<00:09:47.090> a<00:09:47.120> contract<00:09:47.990> already 00:09:48.160 --> 00:09:48.170 align:start position:0% input the address of a contract already 00:09:48.170 --> 00:09:51.070 align:start position:0% input the address of a contract already deployed<00:09:48.710> on<00:09:48.860> a<00:09:48.890> main<00:09:49.490> chain<00:09:49.730> so<00:09:50.240> the<00:09:50.780> thing<00:09:50.960> to 00:09:51.070 --> 00:09:51.080 align:start position:0% deployed on a main chain so the thing to 00:09:51.080 --> 00:09:52.870 align:start position:0% deployed on a main chain so the thing to keep<00:09:51.380> in<00:09:51.500> mind<00:09:51.560> here<00:09:52.010> is<00:09:52.040> that<00:09:52.190> Sakura 00:09:52.870 --> 00:09:52.880 align:start position:0% keep in mind here is that Sakura 00:09:52.880 --> 00:09:54.940 align:start position:0% keep in mind here is that Sakura actually<00:09:53.450> works<00:09:53.690> on<00:09:53.810> byte<00:09:54.050> code<00:09:54.260> so<00:09:54.410> even<00:09:54.830> if 00:09:54.940 --> 00:09:54.950 align:start position:0% actually works on byte code so even if 00:09:54.950 --> 00:09:56.800 align:start position:0% actually works on byte code so even if you<00:09:55.070> give<00:09:55.370> solid<00:09:55.730> it<00:09:55.850> could<00:09:56.060> what<00:09:56.510> is<00:09:56.660> this 00:09:56.800 --> 00:09:56.810 align:start position:0% you give solid it could what is this 00:09:56.810 --> 00:09:58.990 align:start position:0% you give solid it could what is this gonna<00:09:56.960> do<00:09:57.260> under<00:09:58.130> the<00:09:58.220> hood<00:09:58.400> is<00:09:58.580> this<00:09:58.820> gonna 00:09:58.990 --> 00:09:59.000 align:start position:0% gonna do under the hood is this gonna 00:09:59.000 --> 00:10:01.630 align:start position:0% gonna do under the hood is this gonna compile<00:09:59.390> this<00:09:59.570> code<00:09:59.630> and<00:10:00.050> work<00:10:00.800> on<00:10:01.040> the<00:10:01.220> EVM 00:10:01.630 --> 00:10:01.640 align:start position:0% compile this code and work on the EVM 00:10:01.640 --> 00:10:07.690 align:start position:0% compile this code and work on the EVM code<00:10:05.650> so<00:10:06.650> now<00:10:06.800> if<00:10:06.920> we<00:10:06.950> look<00:10:07.100> at<00:10:07.250> this<00:10:07.430> simple 00:10:07.690 --> 00:10:07.700 align:start position:0% code so now if we look at this simple 00:10:07.700 --> 00:10:10.060 align:start position:0% code so now if we look at this simple example<00:10:07.850> of<00:10:08.300> a<00:10:08.330> simple<00:10:08.810> bank<00:10:09.170> you<00:10:09.740> can<00:10:09.890> see 00:10:10.060 --> 00:10:10.070 align:start position:0% example of a simple bank you can see 00:10:10.070 --> 00:10:12.540 align:start position:0% example of a simple bank you can see here<00:10:10.250> that<00:10:10.430> you<00:10:10.580> have<00:10:10.640> a<00:10:10.730> storage<00:10:11.450> variable 00:10:12.540 --> 00:10:12.550 align:start position:0% here that you have a storage variable 00:10:12.550 --> 00:10:15.250 align:start position:0% here that you have a storage variable balances<00:10:13.550> which<00:10:13.760> contains<00:10:14.120> the<00:10:14.750> balances<00:10:15.230> of 00:10:15.250 --> 00:10:15.260 align:start position:0% balances which contains the balances of 00:10:15.260 --> 00:10:18.370 align:start position:0% balances which contains the balances of the<00:10:15.380> users<00:10:15.950> you<00:10:16.520> have<00:10:16.550> a<00:10:16.730> deposit<00:10:17.380> function 00:10:18.370 --> 00:10:18.380 align:start position:0% the users you have a deposit function 00:10:18.380 --> 00:10:20.950 align:start position:0% the users you have a deposit function which<00:10:18.560> allows<00:10:18.740> a<00:10:18.890> user<00:10:19.130> to<00:10:19.480> the<00:10:20.480> pose<00:10:20.690> to 00:10:20.950 --> 00:10:20.960 align:start position:0% which allows a user to the pose to 00:10:20.960 --> 00:10:24.700 align:start position:0% which allows a user to the pose to deposit<00:10:21.910> some<00:10:22.910> money<00:10:22.940> and<00:10:23.450> you<00:10:23.750> also<00:10:23.930> withdraw 00:10:24.700 --> 00:10:24.710 align:start position:0% deposit some money and you also withdraw 00:10:24.710 --> 00:10:29.560 align:start position:0% deposit some money and you also withdraw function<00:10:27.760> so<00:10:28.760> there<00:10:28.910> are<00:10:29.000> many<00:10:29.180> things<00:10:29.390> that 00:10:29.560 --> 00:10:29.570 align:start position:0% function so there are many things that 00:10:29.570 --> 00:10:31.450 align:start position:0% function so there are many things that are<00:10:29.690> wrong<00:10:29.810> with<00:10:29.990> this<00:10:30.110> code<00:10:30.380> and<00:10:30.860> I<00:10:31.100> just<00:10:31.310> want 00:10:31.450 --> 00:10:31.460 align:start position:0% are wrong with this code and I just want 00:10:31.460 --> 00:10:33.250 align:start position:0% are wrong with this code and I just want to<00:10:31.580> show<00:10:32.120> one<00:10:32.300> of<00:10:32.330> the<00:10:32.510> code<00:10:32.660> so<00:10:32.810> here<00:10:33.020> you<00:10:33.110> can 00:10:33.250 --> 00:10:33.260 align:start position:0% to show one of the code so here you can 00:10:33.260 --> 00:10:35.680 align:start position:0% to show one of the code so here you can click<00:10:33.500> formally<00:10:33.890> verify<00:10:34.310> and<00:10:34.550> your<00:10:35.120> you<00:10:35.660> know 00:10:35.680 --> 00:10:35.690 align:start position:0% click formally verify and your you know 00:10:35.690 --> 00:10:38.020 align:start position:0% click formally verify and your you know have<00:10:35.990> a<00:10:36.020> security<00:10:36.770> report<00:10:37.190> with<00:10:37.460> various 00:10:38.020 --> 00:10:38.030 align:start position:0% have a security report with various 00:10:38.030 --> 00:10:40.540 align:start position:0% have a security report with various patterns<00:10:38.330> that<00:10:38.690> are<00:10:38.870> checked<00:10:39.470> or<00:10:39.710> not<00:10:39.980> so<00:10:40.430> the 00:10:40.540 --> 00:10:40.550 align:start position:0% patterns that are checked or not so the 00:10:40.550 --> 00:10:42.250 align:start position:0% patterns that are checked or not so the ones<00:10:40.730> that<00:10:40.850> I'm<00:10:40.940> interested<00:10:41.450> in<00:10:41.540> right<00:10:41.900> now<00:10:41.930> is 00:10:42.250 --> 00:10:42.260 align:start position:0% ones that I'm interested in right now is 00:10:42.260 --> 00:10:44.050 align:start position:0% ones that I'm interested in right now is gas<00:10:42.530> dependent<00:10:42.980> reinsurance<00:10:43.430> II<00:10:43.580> so 00:10:44.050 --> 00:10:44.060 align:start position:0% gas dependent reinsurance II so 00:10:44.060 --> 00:10:47.080 align:start position:0% gas dependent reinsurance II so basically<00:10:44.480> basically<00:10:44.870> the<00:10:45.230> DAO<00:10:45.590> bug<00:10:45.950> so<00:10:46.400> if<00:10:46.880> we 00:10:47.080 --> 00:10:47.090 align:start position:0% basically basically the DAO bug so if we 00:10:47.090 --> 00:10:49.390 align:start position:0% basically basically the DAO bug so if we click<00:10:47.300> on<00:10:47.450> the<00:10:48.140> the<00:10:48.410> matched<00:10:48.620> line<00:10:48.860> to<00:10:49.190> find 00:10:49.390 --> 00:10:49.400 align:start position:0% click on the the matched line to find 00:10:49.400 --> 00:10:53.800 align:start position:0% click on the the matched line to find out<00:10:49.550> where<00:10:49.880> the<00:10:50.120> the<00:10:50.870> faulty<00:10:51.200> code<00:10:51.920> is<00:10:52.810> we're 00:10:53.800 --> 00:10:53.810 align:start position:0% out where the the faulty code is we're 00:10:53.810 --> 00:10:56.460 align:start position:0% out where the the faulty code is we're gonna<00:10:53.900> see<00:10:54.140> that<00:10:54.230> here<00:10:54.620> there<00:10:55.130> is<00:10:55.280> actually 00:10:56.460 --> 00:10:56.470 align:start position:0% gonna see that here there is actually 00:10:56.470 --> 00:10:59.560 align:start position:0% gonna see that here there is actually some<00:10:57.470> ether<00:10:57.680> which<00:10:57.980> is<00:10:58.160> sent<00:10:58.430> and<00:10:58.640> some 00:10:59.560 --> 00:10:59.570 align:start position:0% some ether which is sent and some 00:10:59.570 --> 00:11:02.410 align:start position:0% some ether which is sent and some storage<00:11:00.410> value<00:11:00.800> which<00:11:00.980> is<00:11:01.250> which<00:11:01.940> is<00:11:02.150> set<00:11:02.390> to 00:11:02.410 --> 00:11:02.420 align:start position:0% storage value which is which is set to 00:11:02.420 --> 00:11:05.530 align:start position:0% storage value which is which is set to another<00:11:02.810> value<00:11:03.620> at<00:11:03.980> after<00:11:04.790> the<00:11:05.060> course<00:11:05.300> so 00:11:05.530 --> 00:11:05.540 align:start position:0% another value at after the course so 00:11:05.540 --> 00:11:08.110 align:start position:0% another value at after the course so this<00:11:06.200> means<00:11:06.500> that<00:11:06.590> the<00:11:06.800> attacker<00:11:06.980> through<00:11:07.940> is 00:11:08.110 --> 00:11:08.120 align:start position:0% this means that the attacker through is 00:11:08.120 --> 00:11:10.710 align:start position:0% this means that the attacker through is fallback<00:11:08.420> function<00:11:09.020> can<00:11:09.350> call<00:11:09.950> this<00:11:10.100> function 00:11:10.710 --> 00:11:10.720 align:start position:0% fallback function can call this function 00:11:10.720 --> 00:11:12.900 align:start position:0% fallback function can call this function and<00:11:10.980> this<00:11:11.980> dysfunction<00:11:12.519> is<00:11:12.610> gonna<00:11:12.790> be 00:11:12.900 --> 00:11:12.910 align:start position:0% and this dysfunction is gonna be 00:11:12.910 --> 00:11:14.730 align:start position:0% and this dysfunction is gonna be executed<00:11:13.329> within<00:11:13.600> the<00:11:13.810> same<00:11:14.019> state<00:11:14.199> which<00:11:14.529> is 00:11:14.730 --> 00:11:14.740 align:start position:0% executed within the same state which is 00:11:14.740 --> 00:11:21.059 align:start position:0% executed within the same state which is the<00:11:15.519> DAO<00:11:15.790> bug<00:11:16.769> so<00:11:17.769> one<00:11:18.310> one<00:11:18.990> solution<00:11:19.990> for<00:11:20.560> this 00:11:21.059 --> 00:11:21.069 align:start position:0% the DAO bug so one one solution for this 00:11:21.069 --> 00:11:23.879 align:start position:0% the DAO bug so one one solution for this Posey's<00:11:21.850> bug<00:11:22.029> in<00:11:22.180> this<00:11:22.329> particular<00:11:23.319> example 00:11:23.879 --> 00:11:23.889 align:start position:0% Posey's bug in this particular example 00:11:23.889 --> 00:11:25.769 align:start position:0% Posey's bug in this particular example is<00:11:24.009> just<00:11:24.160> to<00:11:24.399> remove<00:11:24.850> this<00:11:25.029> line<00:11:25.300> and<00:11:25.480> put<00:11:25.690> it 00:11:25.769 --> 00:11:25.779 align:start position:0% is just to remove this line and put it 00:11:25.779 --> 00:11:28.170 align:start position:0% is just to remove this line and put it before<00:11:26.250> which<00:11:27.250> is<00:11:27.279> a<00:11:27.430> quick<00:11:27.819> and<00:11:28.000> dirty 00:11:28.170 --> 00:11:28.180 align:start position:0% before which is a quick and dirty 00:11:28.180 --> 00:11:32.249 align:start position:0% before which is a quick and dirty solution<00:11:28.990> let's<00:11:29.500> say<00:11:30.899> so<00:11:31.899> if<00:11:31.990> we<00:11:32.139> click 00:11:32.249 --> 00:11:32.259 align:start position:0% solution let's say so if we click 00:11:32.259 --> 00:11:36.179 align:start position:0% solution let's say so if we click formerly<00:11:32.889> verify<00:11:33.310> again<00:11:34.470> we're<00:11:35.470> going<00:11:35.560> to<00:11:35.620> get 00:11:36.179 --> 00:11:36.189 align:start position:0% formerly verify again we're going to get 00:11:36.189 --> 00:11:38.790 align:start position:0% formerly verify again we're going to get another<00:11:36.790> security<00:11:37.449> report<00:11:37.870> and<00:11:38.350> in<00:11:38.470> that<00:11:38.589> case 00:11:38.790 --> 00:11:38.800 align:start position:0% another security report and in that case 00:11:38.800 --> 00:11:40.350 align:start position:0% another security report and in that case you<00:11:38.949> can<00:11:39.100> see<00:11:39.279> that<00:11:39.430> the<00:11:39.579> pattern<00:11:39.790> is<00:11:40.120> not<00:11:40.149> a 00:11:40.350 --> 00:11:40.360 align:start position:0% you can see that the pattern is not a 00:11:40.360 --> 00:11:42.179 align:start position:0% you can see that the pattern is not a gun<00:11:40.540> check<00:11:40.750> so<00:11:40.990> you<00:11:41.470> have<00:11:41.560> made<00:11:41.800> sure<00:11:42.009> that 00:11:42.179 --> 00:11:42.189 align:start position:0% gun check so you have made sure that 00:11:42.189 --> 00:11:47.090 align:start position:0% gun check so you have made sure that your<00:11:42.430> contract<00:11:42.970> is<00:11:43.720> no<00:11:43.990> longer<00:11:44.170> a<00:11:45.720> victim<00:11:46.720> of 00:11:47.090 --> 00:11:47.100 align:start position:0% your contract is no longer a victim of 00:11:47.100 --> 00:11:50.639 align:start position:0% your contract is no longer a victim of gas<00:11:48.100> dependent<00:11:48.610> s<00:11:49.089> dependent<00:11:49.509> reenter<00:11:49.839> NC<00:11:50.079> and 00:11:50.639 --> 00:11:50.649 align:start position:0% gas dependent s dependent reenter NC and 00:11:50.649 --> 00:11:52.439 align:start position:0% gas dependent s dependent reenter NC and this<00:11:51.310> is<00:11:51.459> a<00:11:51.490> strong<00:11:51.759> guarantee<00:11:51.910> that<00:11:52.300> is 00:11:52.439 --> 00:11:52.449 align:start position:0% this is a strong guarantee that is 00:11:52.449 --> 00:11:54.720 align:start position:0% this is a strong guarantee that is you're<00:11:52.839> 100%<00:11:53.350> sure<00:11:53.889> of<00:11:53.920> that<00:11:54.250> there<00:11:54.459> is<00:11:54.579> no 00:11:54.720 --> 00:11:54.730 align:start position:0% you're 100% sure of that there is no 00:11:54.730 --> 00:11:57.900 align:start position:0% you're 100% sure of that there is no national<00:11:54.970> code<00:11:55.389> coverage<00:11:55.750> here<00:11:56.079> or<00:11:56.920> they<00:11:57.699> said 00:11:57.900 --> 00:11:57.910 align:start position:0% national code coverage here or they said 00:11:57.910 --> 00:12:06.030 align:start position:0% national code coverage here or they said that<00:11:58.029> the<00:11:58.120> code<00:11:58.269> coverage<00:11:58.600> is<00:11:58.779> 100%<00:12:05.040> so 00:12:06.030 --> 00:12:06.040 align:start position:0% that the code coverage is 100% so 00:12:06.040 --> 00:12:12.269 align:start position:0% that the code coverage is 100% so another<00:12:06.550> example<00:12:07.120> now<00:12:08.040> is<00:12:09.040> this<00:12:11.220> flow<00:12:12.220> the 00:12:12.269 --> 00:12:12.279 align:start position:0% another example now is this flow the 00:12:12.279 --> 00:12:14.369 align:start position:0% another example now is this flow the wallet<00:12:12.639> contract<00:12:13.600> so<00:12:13.810> here<00:12:14.079> you<00:12:14.230> have<00:12:14.350> a 00:12:14.369 --> 00:12:14.379 align:start position:0% wallet contract so here you have a 00:12:14.379 --> 00:12:16.410 align:start position:0% wallet contract so here you have a storage<00:12:15.189> Bible<00:12:15.490> which<00:12:15.670> is<00:12:15.699> owner<00:12:16.000> which<00:12:16.269> is 00:12:16.410 --> 00:12:16.420 align:start position:0% storage Bible which is owner which is 00:12:16.420 --> 00:12:18.240 align:start position:0% storage Bible which is owner which is the<00:12:16.540> owner<00:12:16.660> of<00:12:16.810> the<00:12:17.139> contract<00:12:17.620> so<00:12:17.920> this<00:12:18.069> is 00:12:18.240 --> 00:12:18.250 align:start position:0% the owner of the contract so this is 00:12:18.250 --> 00:12:20.160 align:start position:0% the owner of the contract so this is example<00:12:18.550> I<00:12:19.000> showed<00:12:19.209> earlier<00:12:19.240> you<00:12:19.689> you<00:12:20.019> can 00:12:20.160 --> 00:12:20.170 align:start position:0% example I showed earlier you you can 00:12:20.170 --> 00:12:22.050 align:start position:0% example I showed earlier you you can initialize<00:12:20.709> the<00:12:21.250> owner<00:12:21.399> of<00:12:21.579> the<00:12:21.670> contract 00:12:22.050 --> 00:12:22.060 align:start position:0% initialize the owner of the contract 00:12:22.060 --> 00:12:23.879 align:start position:0% initialize the owner of the contract through<00:12:22.329> the<00:12:22.509> first<00:12:22.810> function<00:12:23.259> in<00:12:23.439> it<00:12:23.589> wallet 00:12:23.879 --> 00:12:23.889 align:start position:0% through the first function in it wallet 00:12:23.889 --> 00:12:26.730 align:start position:0% through the first function in it wallet and<00:12:24.009> the<00:12:24.490> second<00:12:24.790> function<00:12:25.000> allows<00:12:25.959> some 00:12:26.730 --> 00:12:26.740 align:start position:0% and the second function allows some 00:12:26.740 --> 00:12:28.920 align:start position:0% and the second function allows some transfer<00:12:27.160> of<00:12:27.399> ether<00:12:27.670> if<00:12:27.970> the<00:12:28.180> message<00:12:28.630> sender 00:12:28.920 --> 00:12:28.930 align:start position:0% transfer of ether if the message sender 00:12:28.930 --> 00:12:33.689 align:start position:0% transfer of ether if the message sender is<00:12:29.230> the<00:12:29.410> owner<00:12:29.529> so<00:12:32.130> we're<00:12:33.130> not<00:12:33.250> going<00:12:33.430> to<00:12:33.519> try 00:12:33.689 --> 00:12:33.699 align:start position:0% is the owner so we're not going to try 00:12:33.699 --> 00:12:35.939 align:start position:0% is the owner so we're not going to try to<00:12:33.759> to<00:12:34.149> get<00:12:34.300> the<00:12:34.420> security<00:12:34.990> report<00:12:35.199> out<00:12:35.769> of 00:12:35.939 --> 00:12:35.949 align:start position:0% to to get the security report out of 00:12:35.949 --> 00:12:43.710 align:start position:0% to to get the security report out of this<00:12:36.130> contract<00:12:42.149> so<00:12:43.149> if<00:12:43.240> you<00:12:43.329> remember<00:12:43.540> it's 00:12:43.710 --> 00:12:43.720 align:start position:0% this contract so if you remember it's 00:12:43.720 --> 00:12:47.730 align:start position:0% this contract so if you remember it's the<00:12:43.810> multi<00:12:44.079> sick<00:12:44.230> party<00:12:44.589> bug<00:12:46.350> so<00:12:47.350> you<00:12:47.410> see 00:12:47.730 --> 00:12:47.740 align:start position:0% the multi sick party bug so you see 00:12:47.740 --> 00:12:49.650 align:start position:0% the multi sick party bug so you see different<00:12:47.889> patterns<00:12:48.250> and<00:12:48.639> here<00:12:48.910> the<00:12:49.060> one<00:12:49.240> that 00:12:49.650 --> 00:12:49.660 align:start position:0% different patterns and here the one that 00:12:49.660 --> 00:12:51.300 align:start position:0% different patterns and here the one that I<00:12:49.689> want<00:12:49.899> to<00:12:49.959> focus<00:12:50.110> on<00:12:50.410> is<00:12:50.560> I'm<00:12:50.860> privileged 00:12:51.300 --> 00:12:51.310 align:start position:0% I want to focus on is I'm privileged 00:12:51.310 --> 00:12:53.309 align:start position:0% I want to focus on is I'm privileged right<00:12:51.490> to<00:12:51.699> storage<00:12:52.060> so<00:12:52.630> I<00:12:52.660> explained<00:12:53.170> it 00:12:53.309 --> 00:12:53.319 align:start position:0% right to storage so I explained it 00:12:53.319 --> 00:12:55.049 align:start position:0% right to storage so I explained it earlier<00:12:53.439> this<00:12:53.860> that<00:12:54.069> you<00:12:54.220> allow<00:12:54.490> anybody<00:12:54.850> to 00:12:55.049 --> 00:12:55.059 align:start position:0% earlier this that you allow anybody to 00:12:55.059 --> 00:12:57.720 align:start position:0% earlier this that you allow anybody to write<00:12:55.360> to<00:12:55.480> your<00:12:55.600> storage<00:12:55.990> without<00:12:56.649> any<00:12:56.920> check 00:12:57.720 --> 00:12:57.730 align:start position:0% write to your storage without any check 00:12:57.730 --> 00:13:01.319 align:start position:0% write to your storage without any check so<00:12:58.449> if<00:12:58.569> we<00:12:58.689> click<00:12:58.899> on<00:12:59.079> a<00:12:59.139> match<00:12:59.500> line<00:13:00.329> we're 00:13:01.319 --> 00:13:01.329 align:start position:0% so if we click on a match line we're 00:13:01.329 --> 00:13:03.240 align:start position:0% so if we click on a match line we're gonna<00:13:01.449> see<00:13:01.689> that<00:13:01.809> the<00:13:02.019> faulty<00:13:02.470> line<00:13:02.620> is<00:13:02.889> where 00:13:03.240 --> 00:13:03.250 align:start position:0% gonna see that the faulty line is where 00:13:03.250 --> 00:13:05.220 align:start position:0% gonna see that the faulty line is where you<00:13:03.430> assign<00:13:03.730> the<00:13:04.000> owner<00:13:04.149> to<00:13:04.569> another<00:13:04.870> viable 00:13:05.220 --> 00:13:05.230 align:start position:0% you assign the owner to another viable 00:13:05.230 --> 00:13:08.579 align:start position:0% you assign the owner to another viable without<00:13:05.709> any<00:13:05.949> any<00:13:06.370> check<00:13:07.230> so<00:13:08.230> here's<00:13:08.470> a 00:13:08.579 --> 00:13:08.589 align:start position:0% without any any check so here's a 00:13:08.589 --> 00:13:12.240 align:start position:0% without any any check so here's a solution<00:13:09.069> that<00:13:09.220> we<00:13:09.399> can<00:13:10.199> that<00:13:11.199> we<00:13:11.230> can<00:13:11.290> use<00:13:11.949> and 00:13:12.240 --> 00:13:12.250 align:start position:0% solution that we can that we can use and 00:13:12.250 --> 00:13:13.999 align:start position:0% solution that we can that we can use and that<00:13:12.339> work<00:13:12.519> that<00:13:12.819> was<00:13:13.029> actually<00:13:13.240> used<00:13:13.629> in<00:13:13.750> a 00:13:13.999 --> 00:13:14.009 align:start position:0% that work that was actually used in a 00:13:14.009 --> 00:13:17.100 align:start position:0% that work that was actually used in a multi-state<00:13:15.009> party<00:13:15.370> bug<00:13:15.550> was<00:13:16.149> to<00:13:16.360> have<00:13:16.990> a 00:13:17.100 --> 00:13:17.110 align:start position:0% multi-state party bug was to have a 00:13:17.110 --> 00:13:20.699 align:start position:0% multi-state party bug was to have a modifier<00:13:17.559> only<00:13:18.129> honor<00:13:18.309> which<00:13:18.939> is<00:13:19.559> gonna<00:13:20.559> make 00:13:20.699 --> 00:13:20.709 align:start position:0% modifier only honor which is gonna make 00:13:20.709 --> 00:13:22.650 align:start position:0% modifier only honor which is gonna make sure<00:13:20.889> that<00:13:21.130> the<00:13:21.399> function<00:13:21.939> will<00:13:22.180> be<00:13:22.240> actually 00:13:22.650 --> 00:13:22.660 align:start position:0% sure that the function will be actually 00:13:22.660 --> 00:13:24.480 align:start position:0% sure that the function will be actually executed<00:13:23.319> only<00:13:23.500> if<00:13:23.740> the 00:13:24.480 --> 00:13:24.490 align:start position:0% executed only if the 00:13:24.490 --> 00:13:26.580 align:start position:0% executed only if the if<00:13:24.910> the<00:13:25.180> message<00:13:25.450> sender<00:13:25.660> is<00:13:25.930> the<00:13:26.080> owner<00:13:26.200> so 00:13:26.580 --> 00:13:26.590 align:start position:0% if the message sender is the owner so 00:13:26.590 --> 00:13:29.010 align:start position:0% if the message sender is the owner so basically<00:13:26.890> having<00:13:27.700> the<00:13:27.820> same<00:13:28.180> check<00:13:28.510> as<00:13:28.750> you 00:13:29.010 --> 00:13:29.020 align:start position:0% basically having the same check as you 00:13:29.020 --> 00:13:31.050 align:start position:0% basically having the same check as you had<00:13:29.200> in<00:13:29.230> this<00:13:29.590> function<00:13:30.010> but<00:13:30.520> for<00:13:30.730> the 00:13:31.050 --> 00:13:31.060 align:start position:0% had in this function but for the 00:13:31.060 --> 00:13:35.250 align:start position:0% had in this function but for the initialization<00:13:31.600> function<00:13:33.840> so<00:13:34.840> here<00:13:35.110> you 00:13:35.250 --> 00:13:35.260 align:start position:0% initialization function so here you 00:13:35.260 --> 00:13:38.640 align:start position:0% initialization function so here you click<00:13:35.380> formally<00:13:35.800> verify<00:13:36.190> again<00:13:36.430> and<00:13:37.380> if<00:13:38.380> you 00:13:38.640 --> 00:13:38.650 align:start position:0% click formally verify again and if you 00:13:38.650 --> 00:13:40.500 align:start position:0% click formally verify again and if you look<00:13:38.800> at<00:13:38.920> the<00:13:39.040> patterns<00:13:39.370> nights<00:13:39.820> it's<00:13:40.240> safe 00:13:40.500 --> 00:13:40.510 align:start position:0% look at the patterns nights it's safe 00:13:40.510 --> 00:13:42.690 align:start position:0% look at the patterns nights it's safe and<00:13:40.810> so<00:13:41.350> now<00:13:41.650> your<00:13:41.800> contract<00:13:42.130> is<00:13:42.280> guaranteed 00:13:42.690 --> 00:13:42.700 align:start position:0% and so now your contract is guaranteed 00:13:42.700 --> 00:13:45.510 align:start position:0% and so now your contract is guaranteed to<00:13:42.730> be<00:13:42.850> to<00:13:43.450> be<00:13:43.600> deprived<00:13:44.440> of<00:13:44.590> any<00:13:45.220> and 00:13:45.510 --> 00:13:45.520 align:start position:0% to be to be deprived of any and 00:13:45.520 --> 00:13:55.200 align:start position:0% to be to be deprived of any and privilege<00:13:45.880> destroyed<00:13:46.150> to<00:13:46.330> storage<00:13:54.030> one<00:13:55.030> last 00:13:55.200 --> 00:13:55.210 align:start position:0% privilege destroyed to storage one last 00:13:55.210 --> 00:14:00.150 align:start position:0% privilege destroyed to storage one last example<00:13:55.750> quickly<00:13:56.740> is<00:13:57.960> that<00:13:58.960> of<00:13:59.140> the<00:13:59.380> token 00:14:00.150 --> 00:14:00.160 align:start position:0% example quickly is that of the token 00:14:00.160 --> 00:14:03.120 align:start position:0% example quickly is that of the token with<00:14:00.340> the<00:14:00.490> changing<00:14:00.880> price<00:14:01.150> so<00:14:02.080> this<00:14:02.260> is<00:14:02.440> a<00:14:02.470> the 00:14:03.120 --> 00:14:03.130 align:start position:0% with the changing price so this is a the 00:14:03.130 --> 00:14:04.890 align:start position:0% with the changing price so this is a the other<00:14:03.310> transaction<00:14:03.850> reordering<00:14:04.450> example 00:14:04.890 --> 00:14:04.900 align:start position:0% other transaction reordering example 00:14:04.900 --> 00:14:06.900 align:start position:0% other transaction reordering example that<00:14:05.050> I<00:14:05.080> showed<00:14:05.500> earlier<00:14:06.040> where<00:14:06.730> you<00:14:06.760> have 00:14:06.900 --> 00:14:06.910 align:start position:0% that I showed earlier where you have 00:14:06.910 --> 00:14:08.700 align:start position:0% that I showed earlier where you have this<00:14:07.030> set<00:14:07.240> price<00:14:07.450> function<00:14:07.930> through<00:14:08.560> which 00:14:08.700 --> 00:14:08.710 align:start position:0% this set price function through which 00:14:08.710 --> 00:14:10.980 align:start position:0% this set price function through which the<00:14:08.980> owner<00:14:09.160> can<00:14:09.520> change<00:14:09.760> the<00:14:09.910> price<00:14:10.120> and<00:14:10.480> you 00:14:10.980 --> 00:14:10.990 align:start position:0% the owner can change the price and you 00:14:10.990 --> 00:14:13.110 align:start position:0% the owner can change the price and you also<00:14:11.110> have<00:14:11.380> this<00:14:11.560> sell<00:14:11.830> token<00:14:12.190> which<00:14:12.670> is<00:14:12.880> meant 00:14:13.110 --> 00:14:13.120 align:start position:0% also have this sell token which is meant 00:14:13.120 --> 00:14:16.320 align:start position:0% also have this sell token which is meant to<00:14:13.180> be<00:14:13.330> used<00:14:13.480> by<00:14:13.660> the<00:14:13.720> by<00:14:14.140> the<00:14:14.200> user<00:14:15.090> so<00:14:16.090> if<00:14:16.210> you 00:14:16.320 --> 00:14:16.330 align:start position:0% to be used by the by the user so if you 00:14:16.330 --> 00:14:18.870 align:start position:0% to be used by the by the user so if you click<00:14:16.480> formally<00:14:16.840> verify<00:14:17.260> you<00:14:18.250> can<00:14:18.400> see<00:14:18.640> here 00:14:18.870 --> 00:14:18.880 align:start position:0% click formally verify you can see here 00:14:18.880 --> 00:14:22.110 align:start position:0% click formally verify you can see here that<00:14:18.910> the<00:14:19.800> that<00:14:20.800> that<00:14:21.070> transaction<00:14:21.970> may 00:14:22.110 --> 00:14:22.120 align:start position:0% that the that that transaction may 00:14:22.120 --> 00:14:24.330 align:start position:0% that the that that transaction may affect<00:14:22.510> either<00:14:22.720> amount<00:14:23.260> so<00:14:23.740> this<00:14:23.920> is<00:14:24.100> a<00:14:24.130> case 00:14:24.330 --> 00:14:24.340 align:start position:0% affect either amount so this is a case 00:14:24.340 --> 00:14:26.550 align:start position:0% affect either amount so this is a case of<00:14:24.370> transaction<00:14:25.240> reordering<00:14:25.720> because<00:14:26.020> the 00:14:26.550 --> 00:14:26.560 align:start position:0% of transaction reordering because the 00:14:26.560 --> 00:14:28.620 align:start position:0% of transaction reordering because the unknown<00:14:26.980> that<00:14:27.100> can<00:14:27.280> be<00:14:27.400> sent<00:14:27.670> depends<00:14:28.180> on<00:14:28.270> on 00:14:28.620 --> 00:14:28.630 align:start position:0% unknown that can be sent depends on on 00:14:28.630 --> 00:14:31.580 align:start position:0% unknown that can be sent depends on on the<00:14:28.750> variable<00:14:29.170> which<00:14:29.770> is<00:14:29.950> not<00:14:30.100> constant<00:14:30.550> so 00:14:31.580 --> 00:14:31.590 align:start position:0% the variable which is not constant so 00:14:31.590 --> 00:14:34.680 align:start position:0% the variable which is not constant so here<00:14:32.590> a<00:14:32.620> quick<00:14:33.430> fix<00:14:33.670> would<00:14:33.910> be<00:14:33.970> to<00:14:34.090> just<00:14:34.420> decide 00:14:34.680 --> 00:14:34.690 align:start position:0% here a quick fix would be to just decide 00:14:34.690 --> 00:14:36.510 align:start position:0% here a quick fix would be to just decide that<00:14:34.870> the<00:14:34.960> price<00:14:35.140> is<00:14:35.350> constant<00:14:35.770> and<00:14:35.920> remove 00:14:36.510 --> 00:14:36.520 align:start position:0% that the price is constant and remove 00:14:36.520 --> 00:14:39.660 align:start position:0% that the price is constant and remove any<00:14:36.730> ability<00:14:37.210> to<00:14:37.860> to<00:14:38.860> change<00:14:39.040> the<00:14:39.250> price<00:14:39.460> in 00:14:39.660 --> 00:14:39.670 align:start position:0% any ability to to change the price in 00:14:39.670 --> 00:14:44.580 align:start position:0% any ability to to change the price in the<00:14:39.760> future<00:14:42.810> so<00:14:43.810> if<00:14:43.930> we<00:14:44.050> click<00:14:44.170> formally 00:14:44.580 --> 00:14:44.590 align:start position:0% the future so if we click formally 00:14:44.590 --> 00:14:46.830 align:start position:0% the future so if we click formally verify<00:14:44.980> again<00:14:45.280> we<00:14:45.760> can<00:14:45.910> make<00:14:46.300> sure<00:14:46.480> that<00:14:46.510> this 00:14:46.830 --> 00:14:46.840 align:start position:0% verify again we can make sure that this 00:14:46.840 --> 00:14:49.950 align:start position:0% verify again we can make sure that this pattern<00:14:47.080> is<00:14:47.470> checked<00:14:48.250> so<00:14:48.640> of<00:14:49.180> course<00:14:49.420> in<00:14:49.660> that 00:14:49.950 --> 00:14:49.960 align:start position:0% pattern is checked so of course in that 00:14:49.960 --> 00:14:52.770 align:start position:0% pattern is checked so of course in that precise<00:14:50.380> case<00:14:50.620> it<00:14:51.250> it<00:14:51.850> removes<00:14:52.240> one<00:14:52.540> feature 00:14:52.770 --> 00:14:52.780 align:start position:0% precise case it it removes one feature 00:14:52.780 --> 00:14:55.560 align:start position:0% precise case it it removes one feature of<00:14:53.050> the<00:14:53.260> of<00:14:53.650> the<00:14:54.610> of<00:14:54.820> the<00:14:54.910> contract<00:14:55.330> that<00:14:55.390> is 00:14:55.560 --> 00:14:55.570 align:start position:0% of the of the of the contract that is 00:14:55.570 --> 00:14:56.850 align:start position:0% of the of the of the contract that is changing<00:14:55.930> the<00:14:56.050> price<00:14:56.260> so<00:14:56.440> you<00:14:56.560> will<00:14:56.710> need<00:14:56.800> to 00:14:56.850 --> 00:14:56.860 align:start position:0% changing the price so you will need to 00:14:56.860 --> 00:15:04.400 align:start position:0% changing the price so you will need to do<00:14:57.340> a<00:14:57.370> bit<00:14:57.610> more<00:14:57.640> to<00:14:58.330> keep<00:14:58.870> this<00:14:58.990> feature 00:15:04.400 --> 00:15:04.410 align:start position:0% 00:15:04.410 --> 00:15:33.350 align:start position:0% that's<00:15:05.410> it<00:15:05.590> for<00:15:05.770> the<00:15:05.860> demo 00:15:33.350 --> 00:15:33.360 align:start position:0% 00:15:33.360 --> 00:15:35.300 align:start position:0% so<00:15:33.750> now<00:15:33.870> let's<00:15:34.170> talk<00:15:34.290> a<00:15:34.350> bit<00:15:34.589> about<00:15:34.709> what's 00:15:35.300 --> 00:15:35.310 align:start position:0% so now let's talk a bit about what's 00:15:35.310 --> 00:15:38.840 align:start position:0% so now let's talk a bit about what's under<00:15:35.550> the<00:15:35.670> hood<00:15:35.699> of<00:15:35.970> sakura<00:15:36.389> phi<00:15:36.980> so<00:15:37.980> first<00:15:38.490> as 00:15:38.840 --> 00:15:38.850 align:start position:0% under the hood of sakura phi so first as 00:15:38.850 --> 00:15:40.579 align:start position:0% under the hood of sakura phi so first as I<00:15:39.029> said<00:15:39.209> earlier<00:15:39.540> Sakura<00:15:39.959> fireworks<00:15:40.350> on<00:15:40.560> the 00:15:40.579 --> 00:15:40.589 align:start position:0% I said earlier Sakura fireworks on the 00:15:40.589 --> 00:15:42.769 align:start position:0% I said earlier Sakura fireworks on the EVM<00:15:41.100> code<00:15:41.399> so<00:15:41.610> you<00:15:41.639> can<00:15:41.820> exit<00:15:42.180> the<00:15:42.300> idiom 00:15:42.769 --> 00:15:42.779 align:start position:0% EVM code so you can exit the idiom 00:15:42.779 --> 00:15:45.290 align:start position:0% EVM code so you can exit the idiom binary<00:15:43.259> that<00:15:43.920> you<00:15:44.100> obtained<00:15:44.370> for<00:15:44.940> instance<00:15:45.209> by 00:15:45.290 --> 00:15:45.300 align:start position:0% binary that you obtained for instance by 00:15:45.300 --> 00:15:47.060 align:start position:0% binary that you obtained for instance by combination<00:15:45.570> of<00:15:45.959> the<00:15:46.050> obvious<00:15:46.470> solidity<00:15:46.769> code 00:15:47.060 --> 00:15:47.070 align:start position:0% combination of the obvious solidity code 00:15:47.070 --> 00:15:49.519 align:start position:0% combination of the obvious solidity code and<00:15:47.310> using<00:15:48.180> this<00:15:48.329> Sakura<00:15:48.839> is<00:15:49.050> going<00:15:49.199> to<00:15:49.259> obtain 00:15:49.519 --> 00:15:49.529 align:start position:0% and using this Sakura is going to obtain 00:15:49.529 --> 00:15:51.139 align:start position:0% and using this Sakura is going to obtain an<00:15:49.709> intermediate<00:15:50.220> representation<00:15:50.610> this 00:15:51.139 --> 00:15:51.149 align:start position:0% an intermediate representation this 00:15:51.149 --> 00:15:53.059 align:start position:0% an intermediate representation this intermediate<00:15:52.079> representation<00:15:52.740> is<00:15:52.889> only 00:15:53.059 --> 00:15:53.069 align:start position:0% intermediate representation is only 00:15:53.069 --> 00:15:55.850 align:start position:0% intermediate representation is only meant<00:15:53.310> to<00:15:53.430> be<00:15:53.579> easier<00:15:54.000> to<00:15:54.839> process<00:15:55.079> by<00:15:55.410> static 00:15:55.850 --> 00:15:55.860 align:start position:0% meant to be easier to process by static 00:15:55.860 --> 00:15:58.579 align:start position:0% meant to be easier to process by static analysis<00:15:56.459> the<00:15:57.120> static<00:15:57.449> analysis<00:15:57.959> provides 00:15:58.579 --> 00:15:58.589 align:start position:0% analysis the static analysis provides 00:15:58.589 --> 00:16:01.460 align:start position:0% analysis the static analysis provides you<00:15:58.709> with<00:15:58.860> a<00:15:59.190> set<00:15:59.639> of<00:15:59.790> basic<00:16:00.690> facts<00:16:01.079> about<00:16:01.319> your 00:16:01.460 --> 00:16:01.470 align:start position:0% you with a set of basic facts about your 00:16:01.470 --> 00:16:03.829 align:start position:0% you with a set of basic facts about your code<00:16:01.680> for<00:16:01.920> instance<00:16:02.250> you<00:16:02.759> have<00:16:02.880> you<00:16:03.240> you<00:16:03.690> know 00:16:03.829 --> 00:16:03.839 align:start position:0% code for instance you have you you know 00:16:03.839 --> 00:16:05.629 align:start position:0% code for instance you have you you know that<00:16:03.990> this<00:16:04.259> variable<00:16:04.620> is<00:16:04.769> a<00:16:04.800> constant<00:16:05.310> or<00:16:05.490> you 00:16:05.629 --> 00:16:05.639 align:start position:0% that this variable is a constant or you 00:16:05.639 --> 00:16:07.280 align:start position:0% that this variable is a constant or you know<00:16:05.730> that<00:16:05.910> this<00:16:06.000> variable<00:16:06.540> is<00:16:06.630> a<00:16:06.660> balance<00:16:07.050> and 00:16:07.280 --> 00:16:07.290 align:start position:0% know that this variable is a balance and 00:16:07.290 --> 00:16:11.990 align:start position:0% know that this variable is a balance and so<00:16:07.889> all<00:16:08.250> these<00:16:08.850> basic<00:16:09.420> facts<00:16:09.899> are<00:16:10.170> the<00:16:11.000> number 00:16:11.990 --> 00:16:12.000 align:start position:0% so all these basic facts are the number 00:16:12.000 --> 00:16:15.069 align:start position:0% so all these basic facts are the number 0<00:16:12.300> of<00:16:12.389> your<00:16:12.750> iterations<00:16:13.319> that<00:16:13.440> you<00:16:13.589> can<00:16:13.819> run<00:16:14.819> to 00:16:15.069 --> 00:16:15.079 align:start position:0% 0 of your iterations that you can run to 00:16:15.079 --> 00:16:18.199 align:start position:0% 0 of your iterations that you can run to have<00:16:16.079> more<00:16:16.589> and<00:16:16.800> more<00:16:16.829> facts<00:16:17.310> so<00:16:17.819> basically 00:16:18.199 --> 00:16:18.209 align:start position:0% have more and more facts so basically 00:16:18.209 --> 00:16:20.660 align:start position:0% have more and more facts so basically you<00:16:18.360> have<00:16:18.449> a<00:16:18.509> set<00:16:18.930> of<00:16:18.990> inference<00:16:19.709> rules<00:16:20.040> that 00:16:20.660 --> 00:16:20.670 align:start position:0% you have a set of inference rules that 00:16:20.670 --> 00:16:23.720 align:start position:0% you have a set of inference rules that is<00:16:20.819> for<00:16:21.480> instance<00:16:21.750> if<00:16:21.899> a<00:16:22.170> is<00:16:22.649> a<00:16:22.680> constant<00:16:22.829> B<00:16:23.670> is 00:16:23.720 --> 00:16:23.730 align:start position:0% is for instance if a is a constant B is 00:16:23.730 --> 00:16:27.199 align:start position:0% is for instance if a is a constant B is a<00:16:23.819> constant<00:16:24.300> and<00:16:24.480> C<00:16:24.990> depends<00:16:25.829> only<00:16:25.980> on<00:16:26.130> a<00:16:26.459> and<00:16:26.850> B 00:16:27.199 --> 00:16:27.209 align:start position:0% a constant and C depends only on a and B 00:16:27.209 --> 00:16:29.389 align:start position:0% a constant and C depends only on a and B you<00:16:27.660> will<00:16:27.810> know<00:16:27.990> that<00:16:28.019> that<00:16:28.769> C<00:16:28.980> is<00:16:29.100> a<00:16:29.130> constant 00:16:29.389 --> 00:16:29.399 align:start position:0% you will know that that C is a constant 00:16:29.399 --> 00:16:31.850 align:start position:0% you will know that that C is a constant as<00:16:29.730> well<00:16:29.880> so<00:16:30.120> you<00:16:30.540> can<00:16:30.660> imagine<00:16:30.899> this<00:16:31.470> sort<00:16:31.709> of 00:16:31.850 --> 00:16:31.860 align:start position:0% as well so you can imagine this sort of 00:16:31.860 --> 00:16:33.860 align:start position:0% as well so you can imagine this sort of infants<00:16:32.370> rules<00:16:32.610> that<00:16:32.850> we<00:16:33.000> have<00:16:33.180> in<00:16:33.209> Sakura<00:16:33.690> Phi 00:16:33.860 --> 00:16:33.870 align:start position:0% infants rules that we have in Sakura Phi 00:16:33.870 --> 00:16:36.319 align:start position:0% infants rules that we have in Sakura Phi to<00:16:34.350> obtain<00:16:34.620> more<00:16:34.920> and<00:16:35.130> more<00:16:35.339> useful<00:16:35.970> facts 00:16:36.319 --> 00:16:36.329 align:start position:0% to obtain more and more useful facts 00:16:36.329 --> 00:16:40.100 align:start position:0% to obtain more and more useful facts about<00:16:36.569> the<00:16:36.690> code<00:16:37.519> so<00:16:38.750> iterating<00:16:39.750> over<00:16:39.870> this 00:16:40.100 --> 00:16:40.110 align:start position:0% about the code so iterating over this 00:16:40.110 --> 00:16:42.500 align:start position:0% about the code so iterating over this you<00:16:40.529> finally<00:16:41.250> obtain<00:16:41.519> a<00:16:41.699> set<00:16:41.940> of<00:16:42.089> facts<00:16:42.329> which 00:16:42.500 --> 00:16:42.510 align:start position:0% you finally obtain a set of facts which 00:16:42.510 --> 00:16:44.300 align:start position:0% you finally obtain a set of facts which is<00:16:42.660> a<00:16:42.690> fixed<00:16:43.139> point<00:16:43.410> with<00:16:43.680> respect<00:16:43.889> to<00:16:44.220> these 00:16:44.300 --> 00:16:44.310 align:start position:0% is a fixed point with respect to these 00:16:44.310 --> 00:16:47.449 align:start position:0% is a fixed point with respect to these inference<00:16:44.910> rules<00:16:45.149> and<00:16:45.420> so<00:16:46.230> from<00:16:46.920> from<00:16:47.279> all 00:16:47.449 --> 00:16:47.459 align:start position:0% inference rules and so from from all 00:16:47.459 --> 00:16:49.519 align:start position:0% inference rules and so from from all these<00:16:47.670> facts<00:16:47.940> you<00:16:48.060> can<00:16:48.149> infer<00:16:48.630> the<00:16:49.050> security 00:16:49.519 --> 00:16:49.529 align:start position:0% these facts you can infer the security 00:16:49.529 --> 00:16:51.819 align:start position:0% these facts you can infer the security report<00:16:49.920> that<00:16:50.250> I<00:16:50.279> showed<00:16:50.550> to<00:16:50.699> you<00:16:50.730> earlier<00:16:51.240> and 00:16:51.819 --> 00:16:51.829 align:start position:0% report that I showed to you earlier and 00:16:51.829 --> 00:16:54.949 align:start position:0% report that I showed to you earlier and which<00:16:52.829> so<00:16:53.459> basically<00:16:53.730> you<00:16:53.940> match<00:16:54.149> the<00:16:54.690> facts 00:16:54.949 --> 00:16:54.959 align:start position:0% which so basically you match the facts 00:16:54.959 --> 00:16:57.829 align:start position:0% which so basically you match the facts against<00:16:55.470> patterns<00:16:55.949> security<00:16:56.760> patterns<00:16:57.209> so<00:16:57.660> we 00:16:57.829 --> 00:16:57.839 align:start position:0% against patterns security patterns so we 00:16:57.839 --> 00:16:59.960 align:start position:0% against patterns security patterns so we have<00:16:57.959> a<00:16:57.990> few<00:16:58.290> now<00:16:58.529> and<00:16:58.740> we<00:16:58.860> hope<00:16:59.279> to<00:16:59.490> increase 00:16:59.960 --> 00:16:59.970 align:start position:0% have a few now and we hope to increase 00:16:59.970 --> 00:17:02.600 align:start position:0% have a few now and we hope to increase the<00:17:00.149> number<00:17:00.449> in<00:17:00.779> a<00:17:00.990> coming<00:17:01.319> in<00:17:02.250> the<00:17:02.339> coming 00:17:02.600 --> 00:17:02.610 align:start position:0% the number in a coming in the coming 00:17:02.610 --> 00:17:05.870 align:start position:0% the number in a coming in the coming months<00:17:03.169> so<00:17:04.169> what<00:17:04.620> is<00:17:04.770> what<00:17:05.370> is<00:17:05.459> important<00:17:05.819> to 00:17:05.870 --> 00:17:05.880 align:start position:0% months so what is what is important to 00:17:05.880 --> 00:17:08.480 align:start position:0% months so what is what is important to remember<00:17:06.000> here<00:17:06.480> is<00:17:06.600> that<00:17:06.630> you<00:17:07.350> this<00:17:08.130> is<00:17:08.309> fully 00:17:08.480 --> 00:17:08.490 align:start position:0% remember here is that you this is fully 00:17:08.490 --> 00:17:10.280 align:start position:0% remember here is that you this is fully automated<00:17:08.819> that<00:17:09.120> is<00:17:09.299> the<00:17:09.659> only<00:17:09.780> thing<00:17:09.959> you<00:17:10.020> do 00:17:10.280 --> 00:17:10.290 align:start position:0% automated that is the only thing you do 00:17:10.290 --> 00:17:11.929 align:start position:0% automated that is the only thing you do is<00:17:10.470> at<00:17:10.709> the<00:17:10.799> beginning<00:17:10.890> providing<00:17:11.579> the<00:17:11.730> source 00:17:11.929 --> 00:17:11.939 align:start position:0% is at the beginning providing the source 00:17:11.939 --> 00:17:14.240 align:start position:0% is at the beginning providing the source code<00:17:12.179> of<00:17:12.360> of<00:17:13.020> your<00:17:13.230> contract<00:17:13.620> and<00:17:13.949> then 00:17:14.240 --> 00:17:14.250 align:start position:0% code of of your contract and then 00:17:14.250 --> 00:17:16.579 align:start position:0% code of of your contract and then sacrifice<00:17:15.120> is<00:17:15.240> gonna<00:17:15.390> do<00:17:15.569> all<00:17:15.809> this<00:17:16.049> part<00:17:16.409> and 00:17:16.579 --> 00:17:16.589 align:start position:0% sacrifice is gonna do all this part and 00:17:16.589 --> 00:17:18.319 align:start position:0% sacrifice is gonna do all this part and provides<00:17:16.949> provide<00:17:17.400> you<00:17:17.490> with<00:17:17.669> the<00:17:17.850> security 00:17:18.319 --> 00:17:18.329 align:start position:0% provides provide you with the security 00:17:18.329 --> 00:17:20.659 align:start position:0% provides provide you with the security report<00:17:19.079> and<00:17:19.260> this<00:17:19.740> is<00:17:19.919> easily<00:17:20.370> extensible 00:17:20.659 --> 00:17:20.669 align:start position:0% report and this is easily extensible 00:17:20.669 --> 00:17:23.689 align:start position:0% report and this is easily extensible because<00:17:21.510> you<00:17:21.600> can<00:17:21.750> add<00:17:21.900> new<00:17:22.350> patterns<00:17:22.770> along 00:17:23.689 --> 00:17:23.699 align:start position:0% because you can add new patterns along 00:17:23.699 --> 00:17:25.939 align:start position:0% because you can add new patterns along the<00:17:23.880> way<00:17:24.059> so<00:17:24.120> in<00:17:24.839> our<00:17:24.990> experience<00:17:25.439> so<00:17:25.559> far<00:17:25.589> it 00:17:25.939 --> 00:17:25.949 align:start position:0% the way so in our experience so far it 00:17:25.949 --> 00:17:29.780 align:start position:0% the way so in our experience so far it was<00:17:26.130> easy<00:17:26.880> and<00:17:27.319> quite<00:17:28.319> quite<00:17:29.070> quick<00:17:29.400> to<00:17:29.580> add 00:17:29.780 --> 00:17:29.790 align:start position:0% was easy and quite quite quick to add 00:17:29.790 --> 00:17:32.060 align:start position:0% was easy and quite quite quick to add new<00:17:29.970> patterns<00:17:30.360> because<00:17:30.750> the<00:17:30.780> the<00:17:31.620> platform 00:17:32.060 --> 00:17:32.070 align:start position:0% new patterns because the the platform 00:17:32.070 --> 00:17:35.330 align:start position:0% new patterns because the the platform provides<00:17:32.400> any<00:17:33.049> sufficient<00:17:34.049> primitives<00:17:34.830> so 00:17:35.330 --> 00:17:35.340 align:start position:0% provides any sufficient primitives so 00:17:35.340 --> 00:17:37.850 align:start position:0% provides any sufficient primitives so our<00:17:35.700> hope<00:17:35.909> is<00:17:36.059> that<00:17:36.299> we<00:17:36.809> won't<00:17:37.140> have<00:17:37.290> to<00:17:37.440> modify 00:17:37.850 --> 00:17:37.860 align:start position:0% our hope is that we won't have to modify 00:17:37.860 --> 00:17:39.770 align:start position:0% our hope is that we won't have to modify sacrified<00:17:38.669> that<00:17:38.820> much<00:17:39.000> in<00:17:39.179> the<00:17:39.270> future<00:17:39.419> to 00:17:39.770 --> 00:17:39.780 align:start position:0% sacrified that much in the future to 00:17:39.780 --> 00:17:45.799 align:start position:0% sacrified that much in the future to provide<00:17:40.280> to<00:17:41.280> provide<00:17:41.610> a<00:17:41.790> new<00:17:42.210> new<00:17:42.809> patterns 00:17:45.799 --> 00:17:45.809 align:start position:0% 00:17:45.809 --> 00:17:48.660 align:start position:0% so<00:17:46.809> following<00:17:47.260> this<00:17:47.559> experience<00:17:48.190> we<00:17:48.309> Sakura 00:17:48.660 --> 00:17:48.670 align:start position:0% so following this experience we Sakura 00:17:48.670 --> 00:17:51.510 align:start position:0% so following this experience we Sakura fine<00:17:48.850> automated<00:17:49.750> tools<00:17:50.020> to<00:17:50.650> analyze<00:17:51.070> smart 00:17:51.510 --> 00:17:51.520 align:start position:0% fine automated tools to analyze smart 00:17:51.520 --> 00:17:53.010 align:start position:0% fine automated tools to analyze smart contracts<00:17:51.880> a<00:17:52.030> story<00:17:52.270> was<00:17:52.480> created<00:17:52.900> in 00:17:53.010 --> 00:17:53.020 align:start position:0% contracts a story was created in 00:17:53.020 --> 00:17:56.400 align:start position:0% contracts a story was created in Switzerland<00:17:53.730> to<00:17:54.730> audit<00:17:55.420> block<00:17:55.809> chains<00:17:56.110> and 00:17:56.400 --> 00:17:56.410 align:start position:0% Switzerland to audit block chains and 00:17:56.410 --> 00:17:58.680 align:start position:0% Switzerland to audit block chains and and<00:17:56.830> smart<00:17:57.250> contracts<00:17:57.670> and<00:17:57.910> the<00:17:58.390> loop<00:17:58.540> is 00:17:58.680 --> 00:17:58.690 align:start position:0% and smart contracts and the loop is 00:17:58.690 --> 00:18:00.870 align:start position:0% and smart contracts and the loop is really<00:17:58.929> between<00:17:59.230> auditing<00:18:00.220> contracts<00:18:00.670> and 00:18:00.870 --> 00:18:00.880 align:start position:0% really between auditing contracts and 00:18:00.880 --> 00:18:04.190 align:start position:0% really between auditing contracts and seeing<00:18:01.630> the<00:18:01.809> common<00:18:02.110> patterns<00:18:02.470> and<00:18:03.400> try<00:18:03.850> to 00:18:04.190 --> 00:18:04.200 align:start position:0% seeing the common patterns and try to 00:18:04.200 --> 00:18:07.799 align:start position:0% seeing the common patterns and try to extract<00:18:05.200> the<00:18:05.679> the<00:18:06.130> routine<00:18:06.520> out<00:18:06.730> of<00:18:06.880> it<00:18:07.030> and<00:18:07.270> so 00:18:07.799 --> 00:18:07.809 align:start position:0% extract the the routine out of it and so 00:18:07.809 --> 00:18:09.870 align:start position:0% extract the the routine out of it and so this<00:18:08.049> is<00:18:08.260> release<00:18:08.980> this<00:18:09.160> feedback<00:18:09.340> loop<00:18:09.549> that 00:18:09.870 --> 00:18:09.880 align:start position:0% this is release this feedback loop that 00:18:09.880 --> 00:18:12.150 align:start position:0% this is release this feedback loop that we<00:18:10.000> try<00:18:10.210> to<00:18:10.270> to<00:18:10.900> maintain<00:18:11.049> to<00:18:11.650> develop<00:18:11.950> new 00:18:12.150 --> 00:18:12.160 align:start position:0% we try to to maintain to develop new 00:18:12.160 --> 00:18:14.669 align:start position:0% we try to to maintain to develop new tools<00:18:12.400> that<00:18:12.520> will<00:18:12.760> they<00:18:13.480> will<00:18:13.660> improve<00:18:14.049> on<00:18:14.380> the 00:18:14.669 --> 00:18:14.679 align:start position:0% tools that will they will improve on the 00:18:14.679 --> 00:18:16.890 align:start position:0% tools that will they will improve on the current<00:18:14.980> state<00:18:15.160> of<00:18:15.309> art<00:18:15.490> so<00:18:16.059> you<00:18:16.150> can<00:18:16.299> check 00:18:16.890 --> 00:18:16.900 align:start position:0% current state of art so you can check 00:18:16.900 --> 00:18:18.780 align:start position:0% current state of art so you can check out<00:18:17.049> the<00:18:17.169> information<00:18:17.559> about<00:18:18.040> chain<00:18:18.250> security 00:18:18.780 --> 00:18:18.790 align:start position:0% out the information about chain security 00:18:18.790 --> 00:18:21.870 align:start position:0% out the information about chain security if<00:18:19.210> you're<00:18:19.450> interested<00:18:19.900> on<00:18:20.110> this<00:18:20.320> website<00:18:20.880> so 00:18:21.870 --> 00:18:21.880 align:start position:0% if you're interested on this website so 00:18:21.880 --> 00:18:24.000 align:start position:0% if you're interested on this website so to<00:18:21.910> summarize<00:18:22.510> a<00:18:22.840> presidency<00:18:23.350> clarify<00:18:23.830> which 00:18:24.000 --> 00:18:24.010 align:start position:0% to summarize a presidency clarify which 00:18:24.010 --> 00:18:26.549 align:start position:0% to summarize a presidency clarify which is<00:18:24.250> fully<00:18:24.910> automated<00:18:25.270> provide<00:18:26.230> strong 00:18:26.549 --> 00:18:26.559 align:start position:0% is fully automated provide strong 00:18:26.559 --> 00:18:28.350 align:start position:0% is fully automated provide strong guarantees<00:18:26.980> that<00:18:27.010> is<00:18:27.400> when<00:18:27.910> it<00:18:28.030> tells<00:18:28.210> you 00:18:28.350 --> 00:18:28.360 align:start position:0% guarantees that is when it tells you 00:18:28.360 --> 00:18:30.930 align:start position:0% guarantees that is when it tells you that<00:18:28.480> you're<00:18:29.169> the<00:18:29.440> bug<00:18:29.770> doesn't<00:18:30.190> exist<00:18:30.549> they 00:18:30.930 --> 00:18:30.940 align:start position:0% that you're the bug doesn't exist they 00:18:30.940 --> 00:18:31.980 align:start position:0% that you're the bug doesn't exist they didn't<00:18:31.120> means<00:18:31.270> that<00:18:31.419> it<00:18:31.540> really<00:18:31.780> doesn't 00:18:31.980 --> 00:18:31.990 align:start position:0% didn't means that it really doesn't 00:18:31.990 --> 00:18:34.110 align:start position:0% didn't means that it really doesn't exist<00:18:32.410> in<00:18:32.530> your<00:18:32.559> contract<00:18:32.980> and<00:18:33.429> it's<00:18:33.880> also 00:18:34.110 --> 00:18:34.120 align:start position:0% exist in your contract and it's also 00:18:34.120 --> 00:18:35.880 align:start position:0% exist in your contract and it's also extensible<00:18:34.809> via<00:18:35.260> a<00:18:35.410> domain-specific 00:18:35.880 --> 00:18:35.890 align:start position:0% extensible via a domain-specific 00:18:35.890 --> 00:18:38.370 align:start position:0% extensible via a domain-specific language<00:18:36.700> to<00:18:37.179> create<00:18:37.480> new<00:18:37.600> patterns<00:18:37.809> using 00:18:38.370 --> 00:18:38.380 align:start position:0% language to create new patterns using 00:18:38.380 --> 00:18:41.030 align:start position:0% language to create new patterns using the<00:18:38.679> primitives<00:18:39.100> already<00:18:39.460> implemented 00:18:41.030 --> 00:18:41.040 align:start position:0% the primitives already implemented 00:18:41.040 --> 00:18:44.210 align:start position:0% the primitives already implemented following<00:18:42.040> the<00:18:42.160> experience<00:18:43.090> we<00:18:43.210> secured<00:18:43.510> if<00:18:43.630> I 00:18:44.210 --> 00:18:44.220 align:start position:0% following the experience we secured if I 00:18:44.220 --> 00:18:48.060 align:start position:0% following the experience we secured if I contact<00:18:45.220> chain<00:18:45.790> security<00:18:46.299> was<00:18:46.500> was<00:18:47.500> created<00:18:47.919> a 00:18:48.060 --> 00:18:48.070 align:start position:0% contact chain security was was created a 00:18:48.070 --> 00:18:50.390 align:start position:0% contact chain security was was created a startup<00:18:48.490> that<00:18:48.700> specializes<00:18:49.510> in<00:18:49.540> audit<00:18:50.080> of 00:18:50.390 --> 00:18:50.400 align:start position:0% startup that specializes in audit of 00:18:50.400 --> 00:18:53.010 align:start position:0% startup that specializes in audit of small<00:18:51.400> contracts<00:18:51.820> and<00:18:52.090> automated<00:18:52.690> program 00:18:53.010 --> 00:18:53.020 align:start position:0% small contracts and automated program 00:18:53.020 --> 00:18:55.049 align:start position:0% small contracts and automated program analysis<00:18:53.440> and<00:18:53.679> with<00:18:54.250> this<00:18:54.370> thank<00:18:54.760> you<00:18:54.850> for 00:18:55.049 --> 00:18:55.059 align:start position:0% analysis and with this thank you for 00:18:55.059 --> 00:18:58.740 align:start position:0% analysis and with this thank you for your<00:18:55.150> attention 00:18:58.740 --> 00:18:58.750 align:start position:0% 00:18:58.750 --> 00:19:06.329 align:start position:0% [Music]