WEBVTT Kind: captions Language: en 00:00:09.190 --> 00:00:14.940 align:start position:0% [Music] 00:00:14.940 --> 00:00:14.950 align:start position:0% [Music] 00:00:14.950 --> 00:00:16.330 align:start position:0% [Music] Thanks 00:00:16.330 --> 00:00:16.340 align:start position:0% Thanks 00:00:16.340 --> 00:00:18.100 align:start position:0% Thanks good<00:00:16.699> afternoon<00:00:16.910> everyone<00:00:17.240> my<00:00:17.510> name<00:00:18.020> is 00:00:18.100 --> 00:00:18.110 align:start position:0% good afternoon everyone my name is 00:00:18.110 --> 00:00:20.760 align:start position:0% good afternoon everyone my name is Laurie<00:00:18.350> I'm<00:00:18.590> a<00:00:18.980> cooperative<00:00:19.460> cable<00:00:19.880> network<00:00:20.180> a 00:00:20.760 --> 00:00:20.770 align:start position:0% Laurie I'm a cooperative cable network a 00:00:20.770 --> 00:00:23.200 align:start position:0% Laurie I'm a cooperative cable network a decentralized<00:00:21.770> you<00:00:22.460> know<00:00:22.520> it<00:00:22.640> changed<00:00:23.030> for 00:00:23.200 --> 00:00:23.210 align:start position:0% decentralized you know it changed for 00:00:23.210 --> 00:00:25.750 align:start position:0% decentralized you know it changed for the<00:00:23.510> cryptocurrency<00:00:23.900> and<00:00:24.140> tokens<00:00:24.560> but<00:00:25.490> today 00:00:25.750 --> 00:00:25.760 align:start position:0% the cryptocurrency and tokens but today 00:00:25.760 --> 00:00:27.190 align:start position:0% the cryptocurrency and tokens but today I'm<00:00:25.880> not<00:00:25.910> going<00:00:26.210> to<00:00:26.300> talk<00:00:26.480> about<00:00:26.540> Kaiba 00:00:27.190 --> 00:00:27.200 align:start position:0% I'm not going to talk about Kaiba 00:00:27.200 --> 00:00:29.500 align:start position:0% I'm not going to talk about Kaiba I'm<00:00:27.440> going<00:00:28.010> to<00:00:28.070> talk<00:00:28.250> well<00:00:28.430> Oriente<00:00:28.970> the<00:00:29.300> work 00:00:29.500 --> 00:00:29.510 align:start position:0% I'm going to talk well Oriente the work 00:00:29.510 --> 00:00:34.150 align:start position:0% I'm going to talk well Oriente the work that<00:00:29.750> I<00:00:29.780> did<00:00:29.990> before<00:00:30.170> Khyber<00:00:30.850> and<00:00:32.920> Ont<00:00:33.920> is<00:00:33.980> now 00:00:34.150 --> 00:00:34.160 align:start position:0% that I did before Khyber and Ont is now 00:00:34.160 --> 00:00:37.050 align:start position:0% that I did before Khyber and Ont is now maintained<00:00:34.700> and<00:00:34.880> supported<00:00:35.000> by<00:00:35.360> melon<00:00:35.810> pot 00:00:37.050 --> 00:00:37.060 align:start position:0% maintained and supported by melon pot 00:00:37.060 --> 00:00:42.520 align:start position:0% maintained and supported by melon pot right<00:00:38.060> so<00:00:38.360> what<00:00:38.690> is<00:00:38.780> int<00:00:39.820> I<00:00:41.320> think<00:00:42.320> it's<00:00:42.410> not 00:00:42.520 --> 00:00:42.530 align:start position:0% right so what is int I think it's not 00:00:42.530 --> 00:00:57.319 align:start position:0% right so what is int I think it's not working 00:00:57.319 --> 00:00:57.329 align:start position:0% 00:00:57.329 --> 00:01:06.080 align:start position:0% right<00:01:02.570> right<00:01:03.570> so<00:01:03.840> what<00:01:04.199> is<00:01:04.290> int<00:01:04.760> orient<00:01:05.760> is<00:01:05.880> a 00:01:06.080 --> 00:01:06.090 align:start position:0% right right so what is int orient is a 00:01:06.090 --> 00:01:08.450 align:start position:0% right right so what is int orient is a smart<00:01:06.450> contract<00:01:06.630> analyzer<00:01:07.170> that<00:01:07.710> you<00:01:08.340> know 00:01:08.450 --> 00:01:08.460 align:start position:0% smart contract analyzer that you know 00:01:08.460 --> 00:01:11.210 align:start position:0% smart contract analyzer that you know based<00:01:09.210> on<00:01:09.330> symbolic<00:01:09.570> execution<00:01:09.869> so<00:01:10.860> basically 00:01:11.210 --> 00:01:11.220 align:start position:0% based on symbolic execution so basically 00:01:11.220 --> 00:01:13.520 align:start position:0% based on symbolic execution so basically you<00:01:11.820> know<00:01:11.909> given<00:01:12.240> a<00:01:12.330> smart<00:01:12.600> contract<00:01:12.750> event<00:01:13.409> a 00:01:13.520 --> 00:01:13.530 align:start position:0% you know given a smart contract event a 00:01:13.530 --> 00:01:16.160 align:start position:0% you know given a smart contract event a can<00:01:13.770> just<00:01:13.800> you<00:01:14.400> know<00:01:14.430> scan<00:01:14.820> oh<00:01:15.030> you<00:01:15.659> know<00:01:15.750> went 00:01:16.160 --> 00:01:16.170 align:start position:0% can just you know scan oh you know went 00:01:16.170 --> 00:01:17.930 align:start position:0% can just you know scan oh you know went through<00:01:16.320> the<00:01:16.500> contract<00:01:17.130> and<00:01:17.310> you<00:01:17.369> know<00:01:17.640> find 00:01:17.930 --> 00:01:17.940 align:start position:0% through the contract and you know find 00:01:17.940 --> 00:01:20.540 align:start position:0% through the contract and you know find all<00:01:18.180> the<00:01:18.330> possible<00:01:19.100> vulnerabilities<00:01:20.100> in<00:01:20.400> your 00:01:20.540 --> 00:01:20.550 align:start position:0% all the possible vulnerabilities in your 00:01:20.550 --> 00:01:23.930 align:start position:0% all the possible vulnerabilities in your smart<00:01:20.820> contract<00:01:21.320> so<00:01:22.320> we<00:01:22.680> released<00:01:23.280> the<00:01:23.520> first 00:01:23.930 --> 00:01:23.940 align:start position:0% smart contract so we released the first 00:01:23.940 --> 00:01:27.740 align:start position:0% smart contract so we released the first version<00:01:24.090> of<00:01:24.360> int<00:01:24.750> back<00:01:24.930> into<00:01:25.259> the<00:01:25.350> 2016<00:01:26.750> you 00:01:27.740 --> 00:01:27.750 align:start position:0% version of int back into the 2016 you 00:01:27.750 --> 00:01:29.090 align:start position:0% version of int back into the 2016 you know<00:01:27.840> with<00:01:28.080> my<00:01:28.229> team<00:01:28.409> from<00:01:28.680> National 00:01:29.090 --> 00:01:29.100 align:start position:0% know with my team from National 00:01:29.100 --> 00:01:31.730 align:start position:0% know with my team from National University<00:01:29.130> of<00:01:29.640> Singapore<00:01:29.729> and<00:01:30.300> I<00:01:30.740> first 00:01:31.730 --> 00:01:31.740 align:start position:0% University of Singapore and I first 00:01:31.740 --> 00:01:34.310 align:start position:0% University of Singapore and I first present-oriented<00:01:32.580> DEFCON<00:01:33.270> two<00:01:33.479> in<00:01:33.930> Shanghai 00:01:34.310 --> 00:01:34.320 align:start position:0% present-oriented DEFCON two in Shanghai 00:01:34.320 --> 00:01:37.460 align:start position:0% present-oriented DEFCON two in Shanghai last<00:01:34.590> year<00:01:34.800> and<00:01:34.979> after<00:01:35.940> after<00:01:36.780> my 00:01:37.460 --> 00:01:37.470 align:start position:0% last year and after after my 00:01:37.470 --> 00:01:38.240 align:start position:0% last year and after after my presentation 00:01:38.240 --> 00:01:38.250 align:start position:0% presentation 00:01:38.250 --> 00:01:40.790 align:start position:0% presentation Mellon<00:01:38.759> port<00:01:39.000> you<00:01:39.929> know<00:01:39.960> Rachel<00:01:40.410> and<00:01:40.619> they 00:01:40.790 --> 00:01:40.800 align:start position:0% Mellon port you know Rachel and they 00:01:40.800 --> 00:01:42.139 align:start position:0% Mellon port you know Rachel and they wanted<00:01:41.220> to<00:01:41.310> support<00:01:41.670> the<00:01:41.820> development 00:01:42.139 --> 00:01:42.149 align:start position:0% wanted to support the development 00:01:42.149 --> 00:01:47.120 align:start position:0% wanted to support the development appointee<00:01:42.899> so<00:01:43.700> and<00:01:44.700> today<00:01:45.660> o<00:01:46.649> enter<00:01:47.039> is 00:01:47.120 --> 00:01:47.130 align:start position:0% appointee so and today o enter is 00:01:47.130 --> 00:01:50.060 align:start position:0% appointee so and today o enter is available<00:01:47.640> online<00:01:47.820> at<00:01:48.420> this<00:01:48.690> URL<00:01:49.350> if<00:01:49.770> you<00:01:49.950> are 00:01:50.060 --> 00:01:50.070 align:start position:0% available online at this URL if you are 00:01:50.070 --> 00:01:51.620 align:start position:0% available online at this URL if you are if<00:01:50.250> you<00:01:50.340> have<00:01:50.369> your<00:01:50.640> laptop<00:01:50.940> with<00:01:51.149> you<00:01:51.179> you<00:01:51.479> can 00:01:51.620 --> 00:01:51.630 align:start position:0% if you have your laptop with you you can 00:01:51.630 --> 00:01:55.219 align:start position:0% if you have your laptop with you you can check<00:01:52.350> it<00:01:52.470> out<00:01:52.560> so<00:01:53.490> here's<00:01:54.270> a<00:01:54.330> github<00:01:54.690> URL 00:01:55.219 --> 00:01:55.229 align:start position:0% check it out so here's a github URL 00:01:55.229 --> 00:01:59.359 align:start position:0% check it out so here's a github URL Oriente<00:01:56.070> as<00:01:56.159> well<00:01:56.369> is<00:01:57.300> I<00:01:57.869> mean<00:01:58.470> Oriente<00:01:59.070> still 00:01:59.359 --> 00:01:59.369 align:start position:0% Oriente as well is I mean Oriente still 00:01:59.369 --> 00:02:01.910 align:start position:0% Oriente as well is I mean Oriente still under<00:01:59.670> active<00:02:00.000> development<00:02:00.060> so<00:02:00.869> if<00:02:01.470> you<00:02:01.679> have 00:02:01.910 --> 00:02:01.920 align:start position:0% under active development so if you have 00:02:01.920 --> 00:02:04.550 align:start position:0% under active development so if you have you<00:02:02.429> know<00:02:02.550> you<00:02:03.330> wanted<00:02:03.630> to<00:02:03.690> contribute<00:02:04.050> feel 00:02:04.550 --> 00:02:04.560 align:start position:0% you know you wanted to contribute feel 00:02:04.560 --> 00:02:09.309 align:start position:0% you know you wanted to contribute feel free<00:02:04.709> to<00:02:04.739> go<00:02:05.489> to<00:02:05.520> github<00:02:05.970> and<00:02:06.119> start<00:02:06.959> exploring 00:02:09.309 --> 00:02:09.319 align:start position:0% free to go to github and start exploring 00:02:09.319 --> 00:02:11.750 align:start position:0% free to go to github and start exploring right<00:02:10.319> so<00:02:10.530> first<00:02:10.830> of<00:02:10.920> all<00:02:11.009> what<00:02:11.190> is<00:02:11.310> symbolic 00:02:11.750 --> 00:02:11.760 align:start position:0% right so first of all what is symbolic 00:02:11.760 --> 00:02:14.479 align:start position:0% right so first of all what is symbolic execution<00:02:12.230> the<00:02:13.230> techniques<00:02:13.650> Baha'i<00:02:13.980> Oriente 00:02:14.479 --> 00:02:14.489 align:start position:0% execution the techniques Baha'i Oriente 00:02:14.489 --> 00:02:17.630 align:start position:0% execution the techniques Baha'i Oriente so<00:02:15.420> I<00:02:15.450> will<00:02:15.750> use<00:02:15.900> a<00:02:16.110> simple<00:02:16.560> function<00:02:17.220> here 00:02:17.630 --> 00:02:17.640 align:start position:0% so I will use a simple function here 00:02:17.640 --> 00:02:20.839 align:start position:0% so I will use a simple function here that<00:02:17.760> you<00:02:18.270> know<00:02:18.390> get<00:02:18.690> the<00:02:18.840> bonus<00:02:19.550> given<00:02:20.550> some 00:02:20.839 --> 00:02:20.849 align:start position:0% that you know get the bonus given some 00:02:20.849 --> 00:02:22.670 align:start position:0% that you know get the bonus given some you<00:02:21.120> know<00:02:21.330> contribution<00:02:21.870> amount<00:02:22.230> in<00:02:22.470> some 00:02:22.670 --> 00:02:22.680 align:start position:0% you know contribution amount in some 00:02:22.680 --> 00:02:24.350 align:start position:0% you know contribution amount in some token<00:02:22.950> sale<00:02:23.130> right 00:02:24.350 --> 00:02:24.360 align:start position:0% token sale right 00:02:24.360 --> 00:02:27.530 align:start position:0% token sale right so<00:02:25.200> if<00:02:25.560> the<00:02:25.800> amount<00:02:26.069> is<00:02:26.400> like<00:02:26.760> greater<00:02:27.300> than 00:02:27.530 --> 00:02:27.540 align:start position:0% so if the amount is like greater than 00:02:27.540 --> 00:02:29.510 align:start position:0% so if the amount is like greater than hundred<00:02:27.690> Eater<00:02:28.080> then<00:02:28.500> the<00:02:28.650> bonus<00:02:28.800> is<00:02:29.069> 15% 00:02:29.510 --> 00:02:29.520 align:start position:0% hundred Eater then the bonus is 15% 00:02:29.520 --> 00:02:31.610 align:start position:0% hundred Eater then the bonus is 15% otherwise<00:02:30.300> you<00:02:30.569> know<00:02:30.690> if<00:02:31.110> the<00:02:31.319> mouse<00:02:31.590> is 00:02:31.610 --> 00:02:31.620 align:start position:0% otherwise you know if the mouse is 00:02:31.620 --> 00:02:34.460 align:start position:0% otherwise you know if the mouse is greater<00:02:32.580> than<00:02:32.760> 50<00:02:33.090> Eater<00:02:33.239> then<00:02:33.720> you<00:02:33.989> get<00:02:34.170> 10% 00:02:34.460 --> 00:02:34.470 align:start position:0% greater than 50 Eater then you get 10% 00:02:34.470 --> 00:02:36.589 align:start position:0% greater than 50 Eater then you get 10% bonus<00:02:34.739> otherwise<00:02:35.580> there's<00:02:35.879> no<00:02:36.030> bonus<00:02:36.209> for<00:02:36.480> you 00:02:36.589 --> 00:02:36.599 align:start position:0% bonus otherwise there's no bonus for you 00:02:36.599 --> 00:02:39.470 align:start position:0% bonus otherwise there's no bonus for you so<00:02:37.230> if<00:02:37.500> you<00:02:37.590> look<00:02:37.800> at<00:02:37.950> this<00:02:38.040> function<00:02:38.480> there 00:02:39.470 --> 00:02:39.480 align:start position:0% so if you look at this function there 00:02:39.480 --> 00:02:43.010 align:start position:0% so if you look at this function there are<00:02:39.510> three<00:02:39.840> means<00:02:41.540> there<00:02:42.540> are<00:02:42.629> three<00:02:42.840> main 00:02:43.010 --> 00:02:43.020 align:start position:0% are three means there are three main 00:02:43.020 --> 00:02:46.610 align:start position:0% are three means there are three main branches<00:02:43.530> in<00:02:43.770> the<00:02:44.430> entire<00:02:44.819> function<00:02:45.720> you<00:02:46.500> know 00:02:46.610 --> 00:02:46.620 align:start position:0% branches in the entire function you know 00:02:46.620 --> 00:02:51.020 align:start position:0% branches in the entire function you know H<00:02:46.860> is<00:02:47.040> greater<00:02:47.220> than<00:02:47.810> 100<00:02:48.810> and<00:02:49.069> you<00:02:50.069> know<00:02:50.190> H<00:02:50.849> is 00:02:51.020 --> 00:02:51.030 align:start position:0% H is greater than 100 and you know H is 00:02:51.030 --> 00:02:53.509 align:start position:0% H is greater than 100 and you know H is greater<00:02:51.180> than<00:02:51.599> 50<00:02:51.870> and<00:02:52.080> less<00:02:52.230> than<00:02:52.379> 100<00:02:52.620> and<00:02:52.980> X 00:02:53.509 --> 00:02:53.519 align:start position:0% greater than 50 and less than 100 and X 00:02:53.519 --> 00:02:56.479 align:start position:0% greater than 50 and less than 100 and X is<00:02:53.670> less<00:02:53.700> than<00:02:54.000> 50<00:02:54.450> eater<00:02:54.569> so<00:02:55.489> symbolic 00:02:56.479 --> 00:02:56.489 align:start position:0% is less than 50 eater so symbolic 00:02:56.489 --> 00:02:59.360 align:start position:0% is less than 50 eater so symbolic execution<00:02:56.750> allows<00:02:57.750> us<00:02:57.959> to<00:02:58.230> explore<00:02:58.769> the 00:02:59.360 --> 00:02:59.370 align:start position:0% execution allows us to explore the 00:02:59.370 --> 00:03:02.420 align:start position:0% execution allows us to explore the possible<00:02:59.760> parts<00:03:00.120> of<00:03:00.300> the<00:03:00.540> program<00:03:00.900> of<00:03:01.430> your 00:03:02.420 --> 00:03:02.430 align:start position:0% possible parts of the program of your 00:03:02.430 --> 00:03:04.290 align:start position:0% possible parts of the program of your functions<00:03:02.879> and 00:03:04.290 --> 00:03:04.300 align:start position:0% functions and 00:03:04.300 --> 00:03:06.990 align:start position:0% functions and it<00:03:04.840> will<00:03:05.080> record<00:03:05.440> all<00:03:05.740> the<00:03:05.920> you<00:03:06.280> know<00:03:06.310> contract 00:03:06.990 --> 00:03:07.000 align:start position:0% it will record all the you know contract 00:03:07.000 --> 00:03:10.740 align:start position:0% it will record all the you know contract behaviors<00:03:07.420> in<00:03:07.690> its<00:03:07.870> part<00:03:08.140> right<00:03:08.650> and<00:03:09.570> it<00:03:10.570> will 00:03:10.740 --> 00:03:10.750 align:start position:0% behaviors in its part right and it will 00:03:10.750 --> 00:03:13.080 align:start position:0% behaviors in its part right and it will summarize<00:03:11.260> all<00:03:11.560> the<00:03:11.680> behaviors<00:03:12.220> in<00:03:12.520> something 00:03:13.080 --> 00:03:13.090 align:start position:0% summarize all the behaviors in something 00:03:13.090 --> 00:03:16.020 align:start position:0% summarize all the behaviors in something called<00:03:13.300> a<00:03:13.510> part<00:03:13.750> condition<00:03:14.400> here<00:03:15.400> you<00:03:15.880> will 00:03:16.020 --> 00:03:16.030 align:start position:0% called a part condition here you will 00:03:16.030 --> 00:03:17.730 align:start position:0% called a part condition here you will see<00:03:16.150> that<00:03:16.300> for<00:03:16.480> every<00:03:16.540> part<00:03:17.020> we<00:03:17.320> will<00:03:17.470> have<00:03:17.620> the 00:03:17.730 --> 00:03:17.740 align:start position:0% see that for every part we will have the 00:03:17.740 --> 00:03:20.160 align:start position:0% see that for every part we will have the condition<00:03:18.160> for<00:03:18.310> the<00:03:18.430> input<00:03:18.790> to<00:03:19.510> drive<00:03:19.810> the 00:03:20.160 --> 00:03:20.170 align:start position:0% condition for the input to drive the 00:03:20.170 --> 00:03:22.500 align:start position:0% condition for the input to drive the contract<00:03:20.620> or<00:03:20.770> the<00:03:20.830> program<00:03:21.310> to<00:03:21.790> that<00:03:22.120> part 00:03:22.500 --> 00:03:22.510 align:start position:0% contract or the program to that part 00:03:22.510 --> 00:03:26.850 align:start position:0% contract or the program to that part right<00:03:24.030> so<00:03:25.030> with<00:03:25.600> this<00:03:25.720> summer<00:03:26.020> right<00:03:26.230> part 00:03:26.850 --> 00:03:26.860 align:start position:0% right so with this summer right part 00:03:26.860 --> 00:03:31.260 align:start position:0% right so with this summer right part volition<00:03:28.050> with<00:03:29.050> this<00:03:29.170> summer<00:03:29.410> right<00:03:30.270> heart 00:03:31.260 --> 00:03:31.270 align:start position:0% volition with this summer right heart 00:03:31.270 --> 00:03:33.240 align:start position:0% volition with this summer right heart condition<00:03:31.660> we<00:03:31.810> can<00:03:31.960> we<00:03:32.350> can<00:03:32.500> easily<00:03:32.680> check<00:03:33.070> if 00:03:33.240 --> 00:03:33.250 align:start position:0% condition we can we can easily check if 00:03:33.250 --> 00:03:37.500 align:start position:0% condition we can we can easily check if some<00:03:33.460> prob<00:03:33.670> some<00:03:34.150> property<00:03:34.570> is<00:03:34.840> violated<00:03:36.510> so 00:03:37.500 --> 00:03:37.510 align:start position:0% some prob some property is violated so 00:03:37.510 --> 00:03:39.420 align:start position:0% some prob some property is violated so for<00:03:37.780> example<00:03:38.080> we<00:03:38.200> can<00:03:38.320> check<00:03:38.560> whether<00:03:38.770> if<00:03:39.100> you 00:03:39.420 --> 00:03:39.430 align:start position:0% for example we can check whether if you 00:03:39.430 --> 00:03:41.910 align:start position:0% for example we can check whether if you know<00:03:39.550> H<00:03:39.730> is<00:03:39.970> less<00:03:40.210> than<00:03:40.450> 50<00:03:40.840> and<00:03:41.050> you<00:03:41.680> know<00:03:41.770> the 00:03:41.910 --> 00:03:41.920 align:start position:0% know H is less than 50 and you know the 00:03:41.920 --> 00:03:44.700 align:start position:0% know H is less than 50 and you know the bonus<00:03:42.190> is<00:03:42.370> still<00:03:42.610> greater<00:03:42.850> than<00:03:43.090> zero<00:03:43.270> so<00:03:44.260> the 00:03:44.700 --> 00:03:44.710 align:start position:0% bonus is still greater than zero so the 00:03:44.710 --> 00:03:46.890 align:start position:0% bonus is still greater than zero so the way<00:03:44.860> we<00:03:45.040> do<00:03:45.160> it<00:03:45.310> is<00:03:45.490> that<00:03:45.730> we<00:03:45.790> encode<00:03:46.480> or<00:03:46.690> the 00:03:46.890 --> 00:03:46.900 align:start position:0% way we do it is that we encode or the 00:03:46.900 --> 00:03:49.050 align:start position:0% way we do it is that we encode or the part<00:03:47.140> condition<00:03:47.620> and<00:03:47.860> also<00:03:48.160> the<00:03:48.460> property 00:03:49.050 --> 00:03:49.060 align:start position:0% part condition and also the property 00:03:49.060 --> 00:03:51.990 align:start position:0% part condition and also the property that<00:03:49.600> we<00:03:49.750> want<00:03:49.930> to<00:03:49.960> check<00:03:50.260> in<00:03:50.890> some<00:03:51.310> Terim 00:03:51.990 --> 00:03:52.000 align:start position:0% that we want to check in some Terim 00:03:52.000 --> 00:03:54.840 align:start position:0% that we want to check in some Terim proofing<00:03:52.330> language<00:03:52.390> and<00:03:53.020> and<00:03:53.860> you<00:03:54.400> know<00:03:54.520> we 00:03:54.840 --> 00:03:54.850 align:start position:0% proofing language and and you know we 00:03:54.850 --> 00:03:56.490 align:start position:0% proofing language and and you know we use<00:03:55.030> some<00:03:55.240> tour<00:03:55.420> improver<00:03:55.840> or<00:03:56.050> server<00:03:56.260> to 00:03:56.490 --> 00:03:56.500 align:start position:0% use some tour improver or server to 00:03:56.500 --> 00:04:07.650 align:start position:0% use some tour improver or server to check<00:03:56.530> the<00:03:56.980> feasibility<00:04:06.090> right<00:04:07.090> so<00:04:07.420> we<00:04:07.630> can 00:04:07.650 --> 00:04:07.660 align:start position:0% check the feasibility right so we can 00:04:07.660 --> 00:04:09.690 align:start position:0% check the feasibility right so we can check<00:04:07.990> we<00:04:08.380> can<00:04:08.410> use<00:04:08.650> the<00:04:08.890> theorem<00:04:09.340> provers 00:04:09.690 --> 00:04:09.700 align:start position:0% check we can use the theorem provers 00:04:09.700 --> 00:04:12.750 align:start position:0% check we can use the theorem provers over<00:04:10.209> to<00:04:10.420> check<00:04:10.630> the<00:04:10.870> feasibility<00:04:11.739> of<00:04:12.010> you 00:04:12.750 --> 00:04:12.760 align:start position:0% over to check the feasibility of you 00:04:12.760 --> 00:04:17.599 align:start position:0% over to check the feasibility of you know<00:04:12.880> the<00:04:13.090> you<00:04:13.930> know<00:04:14.050> property<00:04:14.709> violation 00:04:17.599 --> 00:04:17.609 align:start position:0% 00:04:17.609 --> 00:04:20.940 align:start position:0% right<00:04:18.609> so<00:04:18.970> this<00:04:19.720> is<00:04:19.780> the<00:04:20.049> main<00:04:20.230> architecture 00:04:20.940 --> 00:04:20.950 align:start position:0% right so this is the main architecture 00:04:20.950 --> 00:04:23.730 align:start position:0% right so this is the main architecture int<00:04:21.489> so<00:04:22.060> our<00:04:22.480> intake<00:04:22.750> works<00:04:23.020> with<00:04:23.380> you<00:04:23.650> know 00:04:23.730 --> 00:04:23.740 align:start position:0% int so our intake works with you know 00:04:23.740 --> 00:04:27.090 align:start position:0% int so our intake works with you know the<00:04:23.980> EVM<00:04:24.340> by<00:04:24.490> code<00:04:24.760> and<00:04:25.260> it<00:04:26.260> also<00:04:26.410> detect<00:04:26.950> the 00:04:27.090 --> 00:04:27.100 align:start position:0% the EVM by code and it also detect the 00:04:27.100 --> 00:04:30.750 align:start position:0% the EVM by code and it also detect the interim<00:04:27.580> state<00:04:27.820> into<00:04:28.690> account<00:04:29.250> so<00:04:30.250> given<00:04:30.640> the 00:04:30.750 --> 00:04:30.760 align:start position:0% interim state into account so given the 00:04:30.760 --> 00:04:33.900 align:start position:0% interim state into account so given the by<00:04:30.880> code<00:04:31.180> it<00:04:31.720> will<00:04:31.980> generate<00:04:32.980> the<00:04:33.280> control 00:04:33.900 --> 00:04:33.910 align:start position:0% by code it will generate the control 00:04:33.910 --> 00:04:36.750 align:start position:0% by code it will generate the control flow<00:04:34.090> graph<00:04:34.120> of<00:04:34.600> the<00:04:34.750> contract<00:04:35.200> and<00:04:35.430> if<00:04:36.430> we<00:04:36.580> use 00:04:36.750 --> 00:04:36.760 align:start position:0% flow graph of the contract and if we use 00:04:36.760 --> 00:04:38.580 align:start position:0% flow graph of the contract and if we use simpler<00:04:37.120> execution<00:04:37.660> to<00:04:37.840> explore<00:04:38.260> the 00:04:38.580 --> 00:04:38.590 align:start position:0% simpler execution to explore the 00:04:38.590 --> 00:04:40.590 align:start position:0% simpler execution to explore the possible<00:04:38.980> part<00:04:39.250> and<00:04:39.490> you<00:04:40.120> know<00:04:40.210> for<00:04:40.390> every 00:04:40.590 --> 00:04:40.600 align:start position:0% possible part and you know for every 00:04:40.600 --> 00:04:43.680 align:start position:0% possible part and you know for every part<00:04:40.870> we<00:04:41.530> will<00:04:41.680> just<00:04:42.010> analyze<00:04:42.280> to<00:04:43.210> see<00:04:43.390> whether 00:04:43.680 --> 00:04:43.690 align:start position:0% part we will just analyze to see whether 00:04:43.690 --> 00:04:48.540 align:start position:0% part we will just analyze to see whether you<00:04:44.320> know<00:04:44.440> some<00:04:44.740> properties<00:04:45.310> violated<00:04:46.169> and<00:04:47.550> of 00:04:48.540 --> 00:04:48.550 align:start position:0% you know some properties violated and of 00:04:48.550 --> 00:04:50.790 align:start position:0% you know some properties violated and of course<00:04:48.790> we<00:04:49.030> use<00:04:49.330> the<00:04:49.510> theorems<00:04:49.870> software<00:04:50.560> here 00:04:50.790 --> 00:04:50.800 align:start position:0% course we use the theorems software here 00:04:50.800 --> 00:04:55.800 align:start position:0% course we use the theorems software here to<00:04:51.070> check<00:04:51.490> that<00:04:51.960> and<00:04:52.960> if<00:04:53.800> if<00:04:54.669> I<00:04:55.030> want<00:04:55.300> a<00:04:55.419> flux 00:04:55.800 --> 00:04:55.810 align:start position:0% to check that and if if I want a flux 00:04:55.810 --> 00:04:57.690 align:start position:0% to check that and if if I want a flux and<00:04:56.080> above<00:04:56.320> then<00:04:56.590> there<00:04:56.830> is<00:04:56.919> a<00:04:56.950> validator 00:04:57.690 --> 00:04:57.700 align:start position:0% and above then there is a validator 00:04:57.700 --> 00:05:00.180 align:start position:0% and above then there is a validator component<00:04:58.690> to<00:04:58.840> check<00:04:59.080> whether<00:04:59.350> the<00:04:59.590> buck<00:05:00.040> is 00:05:00.180 --> 00:05:00.190 align:start position:0% component to check whether the buck is 00:05:00.190 --> 00:05:05.340 align:start position:0% component to check whether the buck is you<00:05:00.460> know<00:05:00.550> found<00:05:00.730> positive<00:05:00.970> on<00:05:01.390> our<00:05:03.480> so<00:05:04.480> what 00:05:05.340 --> 00:05:05.350 align:start position:0% you know found positive on our so what 00:05:05.350 --> 00:05:07.650 align:start position:0% you know found positive on our so what is<00:05:05.440> the<00:05:05.560> main<00:05:05.710> difference<00:05:06.100> between<00:05:06.419> int<00:05:07.419> and 00:05:07.650 --> 00:05:07.660 align:start position:0% is the main difference between int and 00:05:07.660 --> 00:05:08.880 align:start position:0% is the main difference between int and you<00:05:07.930> know<00:05:08.020> other<00:05:08.200> formal<00:05:08.620> verification 00:05:08.880 --> 00:05:08.890 align:start position:0% you know other formal verification 00:05:08.890 --> 00:05:12.810 align:start position:0% you know other formal verification technique<00:05:09.580> so<00:05:10.240> Oriente<00:05:11.460> basically<00:05:12.460> you<00:05:12.700> know 00:05:12.810 --> 00:05:12.820 align:start position:0% technique so Oriente basically you know 00:05:12.820 --> 00:05:14.940 align:start position:0% technique so Oriente basically you know try<00:05:13.120> to<00:05:13.180> find<00:05:13.600> all<00:05:13.840> the<00:05:14.020> possible<00:05:14.200> part<00:05:14.680> in<00:05:14.860> the 00:05:14.940 --> 00:05:14.950 align:start position:0% try to find all the possible part in the 00:05:14.950 --> 00:05:17.159 align:start position:0% try to find all the possible part in the program<00:05:15.310> and<00:05:15.460> see<00:05:16.150> whether<00:05:16.419> you<00:05:16.690> know<00:05:16.810> some 00:05:17.159 --> 00:05:17.169 align:start position:0% program and see whether you know some 00:05:17.169 --> 00:05:18.159 align:start position:0% program and see whether you know some buck<00:05:17.470> or<00:05:17.680> some 00:05:18.159 --> 00:05:18.169 align:start position:0% buck or some 00:05:18.169 --> 00:05:21.550 align:start position:0% buck or some property<00:05:18.560> is<00:05:18.800> violated<00:05:19.900> on<00:05:20.900> the<00:05:21.080> other<00:05:21.259> hand 00:05:21.550 --> 00:05:21.560 align:start position:0% property is violated on the other hand 00:05:21.560 --> 00:05:23.469 align:start position:0% property is violated on the other hand you<00:05:21.770> know<00:05:21.860> form<00:05:22.129> of<00:05:22.249> verification<00:05:22.400> allows<00:05:23.330> you 00:05:23.469 --> 00:05:23.479 align:start position:0% you know form of verification allows you 00:05:23.479 --> 00:05:26.200 align:start position:0% you know form of verification allows you to<00:05:23.689> formally<00:05:24.169> prove<00:05:24.409> that<00:05:24.740> you<00:05:25.009> know<00:05:25.099> if<00:05:25.310> you 00:05:26.200 --> 00:05:26.210 align:start position:0% to formally prove that you know if you 00:05:26.210 --> 00:05:28.119 align:start position:0% to formally prove that you know if you know<00:05:26.270> some<00:05:26.509> the<00:05:26.990> the<00:05:27.349> correctness<00:05:27.710> of<00:05:27.919> some 00:05:28.119 --> 00:05:28.129 align:start position:0% know some the the correctness of some 00:05:28.129 --> 00:05:29.920 align:start position:0% know some the the correctness of some runtime<00:05:28.460> property<00:05:29.029> of<00:05:29.180> your<00:05:29.330> contract<00:05:29.810> a 00:05:29.920 --> 00:05:29.930 align:start position:0% runtime property of your contract a 00:05:29.930 --> 00:05:34.499 align:start position:0% runtime property of your contract a program<00:05:30.319> right<00:05:31.039> so<00:05:31.460> orient<00:05:31.849> it<00:05:31.969> doesn't 00:05:34.499 --> 00:05:34.509 align:start position:0% program right so orient it doesn't 00:05:34.509 --> 00:05:36.760 align:start position:0% program right so orient it doesn't orient<00:05:35.509> it<00:05:35.629> doesn't<00:05:35.930> guarantee<00:05:36.050> the<00:05:36.469> the 00:05:36.760 --> 00:05:36.770 align:start position:0% orient it doesn't guarantee the the 00:05:36.770 --> 00:05:38.679 align:start position:0% orient it doesn't guarantee the the absence<00:05:37.279> of<00:05:37.460> some<00:05:37.699> buck<00:05:37.849> right<00:05:38.150> it<00:05:38.360> to<00:05:38.479> say<00:05:38.659> you 00:05:38.679 --> 00:05:38.689 align:start position:0% absence of some buck right it to say you 00:05:38.689 --> 00:05:40.959 align:start position:0% absence of some buck right it to say you know<00:05:39.020> I<00:05:39.259> have<00:05:39.680> checked<00:05:40.159> you<00:05:40.310> know<00:05:40.430> this<00:05:40.699> many 00:05:40.959 --> 00:05:40.969 align:start position:0% know I have checked you know this many 00:05:40.969 --> 00:05:43.809 align:start position:0% know I have checked you know this many part<00:05:41.330> in<00:05:41.479> the<00:05:41.629> program<00:05:41.990> and<00:05:42.229> you<00:05:42.529> know<00:05:42.819> these 00:05:43.809 --> 00:05:43.819 align:start position:0% part in the program and you know these 00:05:43.819 --> 00:05:46.929 align:start position:0% part in the program and you know these are<00:05:43.879> the<00:05:44.240> bucks<00:05:44.629> that<00:05:44.749> I<00:05:44.900> found<00:05:45.550> on<00:05:46.550> the<00:05:46.789> other 00:05:46.929 --> 00:05:46.939 align:start position:0% are the bucks that I found on the other 00:05:46.939 --> 00:05:50.140 align:start position:0% are the bucks that I found on the other you<00:05:47.300> know<00:05:47.419> eientei<00:05:48.259> is<00:05:48.469> easy<00:05:49.310> to<00:05:49.520> use<00:05:49.550> and<00:05:49.969> you 00:05:50.140 --> 00:05:50.150 align:start position:0% you know eientei is easy to use and you 00:05:50.150 --> 00:05:51.850 align:start position:0% you know eientei is easy to use and you know<00:05:50.180> goes<00:05:50.479> for<00:05:50.689> most<00:05:50.779> of<00:05:50.960> the<00:05:51.050> existing<00:05:51.650> smart 00:05:51.850 --> 00:05:51.860 align:start position:0% know goes for most of the existing smart 00:05:51.860 --> 00:05:54.790 align:start position:0% know goes for most of the existing smart contract<00:05:52.900> but<00:05:53.900> for<00:05:54.199> form<00:05:54.499> of<00:05:54.620> verification 00:05:54.790 --> 00:05:54.800 align:start position:0% contract but for form of verification 00:05:54.800 --> 00:05:57.279 align:start position:0% contract but for form of verification you<00:05:55.580> know<00:05:55.699> sometime<00:05:56.120> you<00:05:56.599> know<00:05:56.719> it<00:05:56.870> doesn't<00:05:57.169> go 00:05:57.279 --> 00:05:57.289 align:start position:0% you know sometime you know it doesn't go 00:05:57.289 --> 00:05:59.950 align:start position:0% you know sometime you know it doesn't go automatically<00:05:57.949> so<00:05:58.849> maybe<00:05:59.180> it<00:05:59.360> requires<00:05:59.539> some 00:05:59.950 --> 00:05:59.960 align:start position:0% automatically so maybe it requires some 00:05:59.960 --> 00:06:02.529 align:start position:0% automatically so maybe it requires some people<00:06:00.199> like<00:06:00.379> Joey<00:06:00.650> or<00:06:01.279> you<00:06:01.490> know<00:06:01.610> some<00:06:02.449> other 00:06:02.529 --> 00:06:02.539 align:start position:0% people like Joey or you know some other 00:06:02.539 --> 00:06:05.320 align:start position:0% people like Joey or you know some other people's<00:06:03.529> presenter<00:06:04.009> to<00:06:04.370> -<00:06:05.029> you<00:06:05.300> know 00:06:05.320 --> 00:06:05.330 align:start position:0% people's presenter to - you know 00:06:05.330 --> 00:06:08.170 align:start position:0% people's presenter to - you know configure<00:06:05.900> the<00:06:06.139> program<00:06:06.349> and<00:06:06.770> you<00:06:07.129> know<00:06:07.249> run 00:06:08.170 --> 00:06:08.180 align:start position:0% configure the program and you know run 00:06:08.180 --> 00:06:15.459 align:start position:0% configure the program and you know run it<00:06:08.210> with<00:06:08.509> a<00:06:08.539> tool<00:06:10.539> and<00:06:11.680> right<00:06:12.999> so<00:06:14.259> what<00:06:15.259> are<00:06:15.379> the 00:06:15.459 --> 00:06:15.469 align:start position:0% it with a tool and right so what are the 00:06:15.469 --> 00:06:17.950 align:start position:0% it with a tool and right so what are the new<00:06:15.589> features<00:06:15.620> that<00:06:15.979> we<00:06:16.490> support<00:06:17.180> in<00:06:17.389> Oriente 00:06:17.950 --> 00:06:17.960 align:start position:0% new features that we support in Oriente 00:06:17.960 --> 00:06:20.769 align:start position:0% new features that we support in Oriente after<00:06:18.439> the<00:06:18.620> DEF<00:06:18.770> CON<00:06:18.919> presentation<00:06:19.580> I<00:06:20.419> will 00:06:20.769 --> 00:06:20.779 align:start position:0% after the DEF CON presentation I will 00:06:20.779 --> 00:06:24.129 align:start position:0% after the DEF CON presentation I will quickly<00:06:20.960> walk<00:06:21.259> through<00:06:21.289> all<00:06:21.680> of<00:06:21.710> them<00:06:21.979> so<00:06:23.139> the 00:06:24.129 --> 00:06:24.139 align:start position:0% quickly walk through all of them so the 00:06:24.139 --> 00:06:25.839 align:start position:0% quickly walk through all of them so the first<00:06:24.169> one<00:06:24.529> that<00:06:24.560> we<00:06:24.830> support<00:06:25.219> is<00:06:25.399> you<00:06:25.729> know 00:06:25.839 --> 00:06:25.849 align:start position:0% first one that we support is you know 00:06:25.849 --> 00:06:29.589 align:start position:0% first one that we support is you know checking<00:06:26.419> the<00:06:26.629> assertion<00:06:27.199> violation<00:06:28.300> in<00:06:29.300> in 00:06:29.589 --> 00:06:29.599 align:start position:0% checking the assertion violation in in 00:06:29.599 --> 00:06:34.389 align:start position:0% checking the assertion violation in in the<00:06:29.750> program<00:06:31.089> so<00:06:32.089> you<00:06:32.389> know<00:06:33.159> developers<00:06:34.159> they 00:06:34.389 --> 00:06:34.399 align:start position:0% the program so you know developers they 00:06:34.399 --> 00:06:36.010 align:start position:0% the program so you know developers they you<00:06:34.610> know<00:06:34.699> sometimes<00:06:35.089> they<00:06:35.210> make<00:06:35.419> some<00:06:35.629> subtle 00:06:36.010 --> 00:06:36.020 align:start position:0% you know sometimes they make some subtle 00:06:36.020 --> 00:06:37.959 align:start position:0% you know sometimes they make some subtle mistakes<00:06:36.500> right<00:06:36.740> they<00:06:37.490> are<00:06:37.520> not<00:06:37.699> even<00:06:37.909> aware 00:06:37.959 --> 00:06:37.969 align:start position:0% mistakes right they are not even aware 00:06:37.969 --> 00:06:40.889 align:start position:0% mistakes right they are not even aware of<00:06:38.180> that<00:06:38.389> so<00:06:39.110> for<00:06:39.500> example<00:06:39.889> this<00:06:40.129> is<00:06:40.310> a<00:06:40.460> simple 00:06:40.889 --> 00:06:40.899 align:start position:0% of that so for example this is a simple 00:06:40.899 --> 00:06:43.959 align:start position:0% of that so for example this is a simple function<00:06:41.899> that<00:06:42.409> transfer<00:06:43.279> the<00:06:43.430> token<00:06:43.759> from 00:06:43.959 --> 00:06:43.969 align:start position:0% function that transfer the token from 00:06:43.969 --> 00:06:47.790 align:start position:0% function that transfer the token from you<00:06:44.330> know<00:06:44.449> the<00:06:44.629> sender<00:06:45.349> to<00:06:45.620> the<00:06:45.649> receiver<00:06:45.800> so 00:06:47.790 --> 00:06:47.800 align:start position:0% you know the sender to the receiver so 00:06:47.800 --> 00:06:51.219 align:start position:0% you know the sender to the receiver so any<00:06:48.800> of<00:06:48.979> you<00:06:49.129> can<00:06:49.339> detect<00:06:49.729> you<00:06:49.939> know<00:06:50.060> the<00:06:50.629> major 00:06:51.219 --> 00:06:51.229 align:start position:0% any of you can detect you know the major 00:06:51.229 --> 00:07:07.730 align:start position:0% any of you can detect you know the major problem<00:06:51.710> in<00:06:51.889> this<00:06:52.009> function 00:07:07.730 --> 00:07:07.740 align:start position:0% 00:07:07.740 --> 00:07:11.390 align:start position:0% oh<00:07:07.770> oh<00:07:08.550> sorry<00:07:08.790> this<00:07:09.270> is<00:07:09.480> this<00:07:09.780> will<00:07:09.960> be<00:07:10.020> -<00:07:10.740> sorry 00:07:11.390 --> 00:07:11.400 align:start position:0% oh oh sorry this is this will be - sorry 00:07:11.400 --> 00:07:16.370 align:start position:0% oh oh sorry this is this will be - sorry yeah<00:07:13.160> right<00:07:14.160> that<00:07:14.190> so<00:07:15.000> I<00:07:15.330> can<00:07:16.080> just<00:07:16.230> quickly 00:07:16.370 --> 00:07:16.380 align:start position:0% yeah right that so I can just quickly 00:07:16.380 --> 00:07:25.150 align:start position:0% yeah right that so I can just quickly fix<00:07:16.710> it<00:07:16.860> but<00:07:17.400> there's<00:07:17.760> an<00:07:18.000> right<00:07:21.830> right 00:07:25.150 --> 00:07:25.160 align:start position:0% 00:07:25.160 --> 00:07:28.130 align:start position:0% sorry<00:07:26.160> this<00:07:26.370> is<00:07:26.520> the<00:07:26.640> naive<00:07:26.970> but<00:07:27.180> right<00:07:27.510> there 00:07:28.130 --> 00:07:28.140 align:start position:0% sorry this is the naive but right there 00:07:28.140 --> 00:07:38.900 align:start position:0% sorry this is the naive but right there is<00:07:28.230> more<00:07:28.530> subtle<00:07:28.950> but<00:07:32.210> sorry<00:07:33.210> what<00:07:37.310> right<00:07:38.310> this 00:07:38.900 --> 00:07:38.910 align:start position:0% is more subtle but sorry what right this 00:07:38.910 --> 00:07:47.270 align:start position:0% is more subtle but sorry what right this is<00:07:39.120> another<00:07:39.330> naive<00:07:39.720> box<00:07:39.960> sorry<00:07:43.880> yeah<00:07:46.280> um 00:07:47.270 --> 00:07:47.280 align:start position:0% is another naive box sorry yeah um 00:07:47.280 --> 00:07:54.610 align:start position:0% is another naive box sorry yeah um another<00:07:48.150> naive<00:07:48.510> buck 00:07:54.610 --> 00:07:54.620 align:start position:0% 00:07:54.620 --> 00:07:59.530 align:start position:0% mmm<00:07:55.620> not<00:07:55.830> really 00:07:59.530 --> 00:07:59.540 align:start position:0% 00:07:59.540 --> 00:08:04.550 align:start position:0% okay<00:08:02.000> right<00:08:03.000> so<00:08:03.390> what<00:08:03.660> happens<00:08:03.960> if<00:08:04.080> sender<00:08:04.440> and 00:08:04.550 --> 00:08:04.560 align:start position:0% okay right so what happens if sender and 00:08:04.560 --> 00:08:08.480 align:start position:0% okay right so what happens if sender and receiver<00:08:04.980> are<00:08:05.010> the<00:08:05.160> same<00:08:06.260> so<00:08:07.260> this<00:08:07.770> guy<00:08:08.010> can 00:08:08.480 --> 00:08:08.490 align:start position:0% receiver are the same so this guy can 00:08:08.490 --> 00:08:10.460 align:start position:0% receiver are the same so this guy can just<00:08:08.520> you<00:08:08.820> know<00:08:08.880> print<00:08:09.210> more<00:08:09.510> token<00:08:09.960> out<00:08:10.170> of 00:08:10.460 --> 00:08:10.470 align:start position:0% just you know print more token out of 00:08:10.470 --> 00:08:14.420 align:start position:0% just you know print more token out of thin<00:08:10.650> air<00:08:10.770> right<00:08:12.440> so<00:08:13.440> this<00:08:13.650> is<00:08:13.830> really<00:08:13.980> subtle 00:08:14.420 --> 00:08:14.430 align:start position:0% thin air right so this is really subtle 00:08:14.430 --> 00:08:16.130 align:start position:0% thin air right so this is really subtle and<00:08:14.640> you<00:08:14.880> know<00:08:15.000> it<00:08:15.180> happens<00:08:15.510> in<00:08:15.750> one<00:08:15.780> of<00:08:15.960> the 00:08:16.130 --> 00:08:16.140 align:start position:0% and you know it happens in one of the 00:08:16.140 --> 00:08:19.940 align:start position:0% and you know it happens in one of the contract<00:08:16.560> that<00:08:16.620> we<00:08:16.830> have<00:08:17.280> audited<00:08:17.700> before<00:08:18.950> so 00:08:19.940 --> 00:08:19.950 align:start position:0% contract that we have audited before so 00:08:19.950 --> 00:08:24.530 align:start position:0% contract that we have audited before so with<00:08:20.670> int<00:08:21.650> it<00:08:22.650> can<00:08:22.950> check<00:08:23.220> you<00:08:23.460> know<00:08:23.580> the<00:08:23.820> this 00:08:24.530 --> 00:08:24.540 align:start position:0% with int it can check you know the this 00:08:24.540 --> 00:08:26.390 align:start position:0% with int it can check you know the this you<00:08:24.780> know<00:08:24.870> if<00:08:25.050> we<00:08:25.200> add<00:08:25.380> some<00:08:25.710> assertion<00:08:26.220> there 00:08:26.390 --> 00:08:26.400 align:start position:0% you know if we add some assertion there 00:08:26.400 --> 00:08:28.310 align:start position:0% you know if we add some assertion there and<00:08:26.700> Oriente<00:08:27.480> can<00:08:27.690> check<00:08:27.930> whether<00:08:28.140> this 00:08:28.310 --> 00:08:28.320 align:start position:0% and Oriente can check whether this 00:08:28.320 --> 00:08:30.710 align:start position:0% and Oriente can check whether this assertion<00:08:28.740> is<00:08:29.010> violated<00:08:29.700> before<00:08:30.180> you<00:08:30.540> even 00:08:30.710 --> 00:08:30.720 align:start position:0% assertion is violated before you even 00:08:30.720 --> 00:08:32.570 align:start position:0% assertion is violated before you even deploy<00:08:31.080> the<00:08:31.500> contract<00:08:31.860> on<00:08:31.980> the<00:08:32.100> main<00:08:32.250> air<00:08:32.400> or 00:08:32.570 --> 00:08:32.580 align:start position:0% deploy the contract on the main air or 00:08:32.580 --> 00:08:34.700 align:start position:0% deploy the contract on the main air or test<00:08:32.820> net<00:08:33.000> so<00:08:33.750> I<00:08:33.780> can<00:08:33.960> just<00:08:34.170> quickly<00:08:34.350> show<00:08:34.680> you 00:08:34.700 --> 00:08:34.710 align:start position:0% test net so I can just quickly show you 00:08:34.710 --> 00:08:44.290 align:start position:0% test net so I can just quickly show you the<00:08:34.980> demo<00:08:35.730> right<00:08:40.910> this<00:08:41.910> is<00:08:42.060> another<00:08:42.330> no<00:08:42.870> bug 00:08:44.290 --> 00:08:44.300 align:start position:0% the demo right this is another no bug 00:08:44.300 --> 00:08:50.510 align:start position:0% the demo right this is another no bug right<00:08:45.300> so<00:08:46.170> this<00:08:46.320> is<00:08:46.500> the<00:08:48.380> the<00:08:49.380> live<00:08:49.860> version<00:08:50.220> of 00:08:50.510 --> 00:08:50.520 align:start position:0% right so this is the the live version of 00:08:50.520 --> 00:08:53.630 align:start position:0% right so this is the the live version of int<00:08:51.000> it's<00:08:51.300> a<00:08:51.570> you<00:08:52.140> know<00:08:52.260> oriented<00:08:52.770> Melander 00:08:53.630 --> 00:08:53.640 align:start position:0% int it's a you know oriented Melander 00:08:53.640 --> 00:09:00.110 align:start position:0% int it's a you know oriented Melander network<00:08:55.580> so<00:08:56.580> you<00:08:56.610> can<00:08:56.970> just<00:08:57.120> click<00:08:57.450> to<00:08:59.120> compile 00:09:00.110 --> 00:09:00.120 align:start position:0% network so you can just click to compile 00:09:00.120 --> 00:09:12.320 align:start position:0% network so you can just click to compile with<00:09:01.910> right<00:09:02.910> click<00:09:03.420> to<00:09:03.630> int<00:09:03.930> and<00:09:04.110> analyze 00:09:12.320 --> 00:09:12.330 align:start position:0% 00:09:12.330 --> 00:09:25.820 align:start position:0% Oh<00:09:12.470> something's<00:09:13.470> wrong<00:09:23.690> sorry<00:09:24.690> I<00:09:24.780> get<00:09:25.560> back<00:09:25.680> to 00:09:25.820 --> 00:09:25.830 align:start position:0% Oh something's wrong sorry I get back to 00:09:25.830 --> 00:09:30.050 align:start position:0% Oh something's wrong sorry I get back to it<00:09:25.920> later<00:09:25.950> but<00:09:26.640> you<00:09:26.910> know<00:09:28.400> right 00:09:30.050 --> 00:09:30.060 align:start position:0% it later but you know right 00:09:30.060 --> 00:09:31.850 align:start position:0% it later but you know right but<00:09:30.390> basically<00:09:30.570> you<00:09:30.870> know<00:09:30.990> you<00:09:31.020> can<00:09:31.290> with 00:09:31.850 --> 00:09:31.860 align:start position:0% but basically you know you can with 00:09:31.860 --> 00:09:33.230 align:start position:0% but basically you know you can with oriented<00:09:32.250> you<00:09:32.370> can<00:09:32.520> shake<00:09:32.730> you<00:09:32.910> know<00:09:32.940> whether 00:09:33.230 --> 00:09:33.240 align:start position:0% oriented you can shake you know whether 00:09:33.240 --> 00:09:36.740 align:start position:0% oriented you can shake you know whether some<00:09:34.070> assertion<00:09:35.070> is<00:09:35.190> violated<00:09:35.760> before<00:09:36.240> you 00:09:36.740 --> 00:09:36.750 align:start position:0% some assertion is violated before you 00:09:36.750 --> 00:09:38.990 align:start position:0% some assertion is violated before you know<00:09:36.870> you<00:09:37.230> evenly<00:09:37.530> deploy<00:09:37.920> the<00:09:38.100> contract<00:09:38.490> to 00:09:38.990 --> 00:09:39.000 align:start position:0% know you evenly deploy the contract to 00:09:39.000 --> 00:09:44.230 align:start position:0% know you evenly deploy the contract to the<00:09:39.030> manor<00:09:39.750> or<00:09:39.990> test<00:09:40.230> net<00:09:42.470> another<00:09:43.470> another 00:09:44.230 --> 00:09:44.240 align:start position:0% the manor or test net another another 00:09:44.240 --> 00:09:46.610 align:start position:0% the manor or test net another another feature<00:09:45.240> that<00:09:45.360> we<00:09:45.540> support<00:09:45.990> is<00:09:46.170> you-know-who 00:09:46.610 --> 00:09:46.620 align:start position:0% feature that we support is you-know-who 00:09:46.620 --> 00:09:49.100 align:start position:0% feature that we support is you-know-who loop<00:09:47.070> handling<00:09:47.640> so<00:09:48.210> if<00:09:48.450> you<00:09:48.570> ever<00:09:48.780> you<00:09:49.080> know 00:09:49.100 --> 00:09:49.110 align:start position:0% loop handling so if you ever you know 00:09:49.110 --> 00:09:51.800 align:start position:0% loop handling so if you ever you know work<00:09:49.440> with<00:09:49.470> you<00:09:49.890> know<00:09:50.010> program<00:09:51.000> and<00:09:51.240> analysis 00:09:51.800 --> 00:09:51.810 align:start position:0% work with you know program and analysis 00:09:51.810 --> 00:09:53.180 align:start position:0% work with you know program and analysis you<00:09:52.050> will<00:09:52.140> know<00:09:52.290> that<00:09:52.320> you<00:09:52.650> know<00:09:52.740> handling 00:09:53.180 --> 00:09:53.190 align:start position:0% you will know that you know handling 00:09:53.190 --> 00:09:55.310 align:start position:0% you will know that you know handling loop<00:09:53.430> is<00:09:53.670> you<00:09:54.060> know<00:09:54.180> a<00:09:54.420> nightmare 00:09:55.310 --> 00:09:55.320 align:start position:0% loop is you know a nightmare 00:09:55.320 --> 00:09:57.560 align:start position:0% loop is you know a nightmare right<00:09:55.500> because<00:09:56.190> basically<00:09:56.790> you<00:09:57.090> know<00:09:57.210> loop 00:09:57.560 --> 00:09:57.570 align:start position:0% right because basically you know loop 00:09:57.570 --> 00:10:00.380 align:start position:0% right because basically you know loop can<00:09:58.410> just<00:09:58.650> force<00:09:58.950> the<00:09:59.310> analyzer<00:09:59.940> to<00:10:00.210> run 00:10:00.380 --> 00:10:00.390 align:start position:0% can just force the analyzer to run 00:10:00.390 --> 00:10:03.980 align:start position:0% can just force the analyzer to run forever<00:10:01.040> and<00:10:02.040> you<00:10:02.970> know<00:10:03.000> did<00:10:03.420> make<00:10:03.630> the 00:10:03.980 --> 00:10:03.990 align:start position:0% forever and you know did make the 00:10:03.990 --> 00:10:06.740 align:start position:0% forever and you know did make the program<00:10:04.710> termination<00:10:05.130> non-deterministic<00:10:05.910> so 00:10:06.740 --> 00:10:06.750 align:start position:0% program termination non-deterministic so 00:10:06.750 --> 00:10:09.350 align:start position:0% program termination non-deterministic so this<00:10:06.990> simple<00:10:07.380> function<00:10:08.250> here<00:10:08.280> can<00:10:08.970> just<00:10:09.180> make 00:10:09.350 --> 00:10:09.360 align:start position:0% this simple function here can just make 00:10:09.360 --> 00:10:11.960 align:start position:0% this simple function here can just make you<00:10:09.570> know<00:10:09.600> eientei<00:10:10.110> run<00:10:10.350> forever<00:10:10.620> because<00:10:11.220> we 00:10:11.960 --> 00:10:11.970 align:start position:0% you know eientei run forever because we 00:10:11.970 --> 00:10:13.880 align:start position:0% you know eientei run forever because we have<00:10:12.180> like<00:10:12.420> no<00:10:12.450> idea<00:10:12.900> like<00:10:13.110> what<00:10:13.440> is<00:10:13.530> the<00:10:13.650> land 00:10:13.880 --> 00:10:13.890 align:start position:0% have like no idea like what is the land 00:10:13.890 --> 00:10:16.520 align:start position:0% have like no idea like what is the land here<00:10:14.760> right<00:10:15.090> what<00:10:15.720> did<00:10:15.840> the<00:10:15.990> lands<00:10:16.260> at<00:10:16.410> the 00:10:16.520 --> 00:10:16.530 align:start position:0% here right what did the lands at the 00:10:16.530 --> 00:10:22.190 align:start position:0% here right what did the lands at the value<00:10:16.770> X<00:10:17.660> array<00:10:18.660> X<00:10:19.430> so<00:10:20.430> in<00:10:20.760> Oriente<00:10:21.240> we<00:10:21.510> handle 00:10:22.190 --> 00:10:22.200 align:start position:0% value X array X so in Oriente we handle 00:10:22.200 --> 00:10:26.480 align:start position:0% value X array X so in Oriente we handle loops<00:10:22.560> in<00:10:22.830> different<00:10:23.370> ways<00:10:24.380> so<00:10:25.380> first<00:10:26.280> of<00:10:26.400> all 00:10:26.480 --> 00:10:26.490 align:start position:0% loops in different ways so first of all 00:10:26.490 --> 00:10:29.840 align:start position:0% loops in different ways so first of all we<00:10:26.730> allow<00:10:27.690> the<00:10:28.320> user<00:10:28.350> to<00:10:28.650> specify<00:10:28.920> the<00:10:29.340> gasps 00:10:29.840 --> 00:10:29.850 align:start position:0% we allow the user to specify the gasps 00:10:29.850 --> 00:10:32.960 align:start position:0% we allow the user to specify the gasps limit<00:10:30.210> so<00:10:31.140> oriented<00:10:31.590> we<00:10:31.710> just<00:10:31.890> keep<00:10:32.520> exploring 00:10:32.960 --> 00:10:32.970 align:start position:0% limit so oriented we just keep exploring 00:10:32.970 --> 00:10:35.690 align:start position:0% limit so oriented we just keep exploring the<00:10:33.330> program<00:10:33.690> until<00:10:34.140> the<00:10:34.320> gasps<00:10:34.560> limits<00:10:34.890> is<00:10:35.100> a 00:10:35.690 --> 00:10:35.700 align:start position:0% the program until the gasps limits is a 00:10:35.700 --> 00:10:39.260 align:start position:0% the program until the gasps limits is a rich<00:10:36.650> we<00:10:37.650> also<00:10:38.070> like<00:10:38.340> allow<00:10:38.580> user<00:10:38.910> to<00:10:38.940> specify 00:10:39.260 --> 00:10:39.270 align:start position:0% rich we also like allow user to specify 00:10:39.270 --> 00:10:42.080 align:start position:0% rich we also like allow user to specify the<00:10:40.170> number<00:10:40.350> of<00:10:40.560> iteration<00:10:41.220> that<00:10:41.550> they<00:10:41.850> want 00:10:42.080 --> 00:10:42.090 align:start position:0% the number of iteration that they want 00:10:42.090 --> 00:10:47.420 align:start position:0% the number of iteration that they want they<00:10:42.420> look<00:10:42.600> to<00:10:42.750> be<00:10:42.830> to<00:10:43.830> run<00:10:44.400> right<00:10:45.560> so<00:10:46.560> here's 00:10:47.420 --> 00:10:47.430 align:start position:0% they look to be to run right so here's 00:10:47.430 --> 00:10:50.810 align:start position:0% they look to be to run right so here's the<00:10:47.610> argument<00:10:47.850> that<00:10:48.210> you<00:10:48.690> can<00:10:48.870> use<00:10:49.760> orient<00:10:50.760> a 00:10:50.810 --> 00:10:50.820 align:start position:0% the argument that you can use orient a 00:10:50.820 --> 00:10:53.410 align:start position:0% the argument that you can use orient a user<00:10:51.660> can<00:10:51.810> also<00:10:51.840> like<00:10:52.200> specify<00:10:52.470> the<00:10:52.740> time<00:10:53.070> out 00:10:53.410 --> 00:10:53.420 align:start position:0% user can also like specify the time out 00:10:53.420 --> 00:10:56.780 align:start position:0% user can also like specify the time out that<00:10:54.420> they<00:10:54.750> allow<00:10:55.020> wanted<00:10:55.650> to<00:10:55.770> run<00:10:55.950> so<00:10:56.490> after 00:10:56.780 --> 00:10:56.790 align:start position:0% that they allow wanted to run so after 00:10:56.790 --> 00:10:58.520 align:start position:0% that they allow wanted to run so after that<00:10:56.910> time<00:10:57.120> I<00:10:57.240> oriented<00:10:58.020> with<00:10:58.170> this<00:10:58.290> you<00:10:58.440> know 00:10:58.520 --> 00:10:58.530 align:start position:0% that time I oriented with this you know 00:10:58.530 --> 00:11:04.100 align:start position:0% that time I oriented with this you know stop<00:11:01.160> another<00:11:02.180> another<00:11:03.180> thing<00:11:03.300> that<00:11:03.630> we<00:11:03.810> added 00:11:04.100 --> 00:11:04.110 align:start position:0% stop another another thing that we added 00:11:04.110 --> 00:11:07.130 align:start position:0% stop another another thing that we added after<00:11:04.740> the<00:11:04.770> DEF<00:11:05.010> CON<00:11:05.160> to<00:11:05.400> is<00:11:05.670> you<00:11:06.360> know<00:11:06.480> making 00:11:07.130 --> 00:11:07.140 align:start position:0% after the DEF CON to is you know making 00:11:07.140 --> 00:11:11.510 align:start position:0% after the DEF CON to is you know making Oriente<00:11:07.800> more<00:11:08.010> dynamic<00:11:08.580> so<00:11:09.240> so<00:11:09.720> when<00:11:10.590> you<00:11:10.710> when 00:11:11.510 --> 00:11:11.520 align:start position:0% Oriente more dynamic so so when you when 00:11:11.520 --> 00:11:14.780 align:start position:0% Oriente more dynamic so so when you when you<00:11:11.610> analyze<00:11:12.050> so<00:11:13.050> Ont<00:11:13.650> is<00:11:13.740> based<00:11:14.010> based<00:11:14.550> on 00:11:14.780 --> 00:11:14.790 align:start position:0% you analyze so Ont is based based on 00:11:14.790 --> 00:11:17.030 align:start position:0% you analyze so Ont is based based on static<00:11:15.270> a<00:11:15.360> similar<00:11:15.780> execution<00:11:16.380> so<00:11:16.680> that<00:11:16.830> means 00:11:17.030 --> 00:11:17.040 align:start position:0% static a similar execution so that means 00:11:17.040 --> 00:11:19.490 align:start position:0% static a similar execution so that means we<00:11:17.490> only<00:11:17.550> care<00:11:18.000> about<00:11:18.030> the<00:11:18.840> contract<00:11:19.230> itself 00:11:19.490 --> 00:11:19.500 align:start position:0% we only care about the contract itself 00:11:19.500 --> 00:11:21.320 align:start position:0% we only care about the contract itself we<00:11:20.100> do<00:11:20.220> not<00:11:20.340> care<00:11:20.640> much<00:11:20.790> about<00:11:20.850> the 00:11:21.320 --> 00:11:21.330 align:start position:0% we do not care much about the 00:11:21.330 --> 00:11:23.750 align:start position:0% we do not care much about the environment<00:11:22.160> outside<00:11:23.160> of<00:11:23.220> the<00:11:23.340> contract 00:11:23.750 --> 00:11:23.760 align:start position:0% environment outside of the contract 00:11:23.760 --> 00:11:25.580 align:start position:0% environment outside of the contract right<00:11:24.000> so<00:11:24.510> for<00:11:24.660> example<00:11:24.960> if<00:11:25.080> the<00:11:25.200> contract 00:11:25.580 --> 00:11:25.590 align:start position:0% right so for example if the contract 00:11:25.590 --> 00:11:26.120 align:start position:0% right so for example if the contract cost 00:11:26.120 --> 00:11:26.130 align:start position:0% cost 00:11:26.130 --> 00:11:27.980 align:start position:0% cost another<00:11:26.370> contract<00:11:26.880> then<00:11:27.300> we<00:11:27.540> do<00:11:27.660> not<00:11:27.810> like 00:11:27.980 --> 00:11:27.990 align:start position:0% another contract then we do not like 00:11:27.990 --> 00:11:31.010 align:start position:0% another contract then we do not like analyze<00:11:28.410> the<00:11:28.800> the<00:11:29.510> contract<00:11:30.510> that<00:11:30.540> you<00:11:30.930> know 00:11:31.010 --> 00:11:31.020 align:start position:0% analyze the the contract that you know 00:11:31.020 --> 00:11:32.780 align:start position:0% analyze the the contract that you know this<00:11:31.230> contract<00:11:31.560> is<00:11:31.650> calling 00:11:32.780 --> 00:11:32.790 align:start position:0% this contract is calling 00:11:32.790 --> 00:11:35.630 align:start position:0% this contract is calling so<00:11:33.300> with<00:11:33.720> Oriente<00:11:34.110> we<00:11:34.350> allows<00:11:34.680> user<00:11:35.100> to<00:11:35.250> set<00:11:35.550> up 00:11:35.630 --> 00:11:35.640 align:start position:0% so with Oriente we allows user to set up 00:11:35.640 --> 00:11:38.890 align:start position:0% so with Oriente we allows user to set up a<00:11:35.790> customized<00:11:36.420> blockchain<00:11:36.990> or<00:11:37.170> environment 00:11:38.890 --> 00:11:38.900 align:start position:0% a customized blockchain or environment 00:11:38.900 --> 00:11:42.530 align:start position:0% a customized blockchain or environment so<00:11:39.900> you<00:11:40.200> know<00:11:40.550> so<00:11:41.550> you<00:11:41.850> know<00:11:42.150> when<00:11:42.330> this 00:11:42.530 --> 00:11:42.540 align:start position:0% so you know so you know when this 00:11:42.540 --> 00:11:44.240 align:start position:0% so you know so you know when this contract<00:11:43.020> Co<00:11:43.200> another<00:11:43.470> contract<00:11:43.980> then 00:11:44.240 --> 00:11:44.250 align:start position:0% contract Co another contract then 00:11:44.250 --> 00:11:46.730 align:start position:0% contract Co another contract then Oriente<00:11:44.850> will<00:11:45.000> go<00:11:45.180> to<00:11:45.690> that<00:11:45.840> contract<00:11:46.110> SQL<00:11:46.560> and 00:11:46.730 --> 00:11:46.740 align:start position:0% Oriente will go to that contract SQL and 00:11:46.740 --> 00:11:52.220 align:start position:0% Oriente will go to that contract SQL and analyze<00:11:47.220> it<00:11:47.960> so<00:11:49.040> this<00:11:50.040> is<00:11:50.220> how<00:11:50.870> how<00:11:51.870> you<00:11:51.930> can 00:11:52.220 --> 00:11:52.230 align:start position:0% analyze it so this is how how you can 00:11:52.230 --> 00:11:55.100 align:start position:0% analyze it so this is how how you can specify<00:11:52.530> the<00:11:52.800> environment<00:11:53.730> to<00:11:54.570> work<00:11:54.960> with 00:11:55.100 --> 00:11:55.110 align:start position:0% specify the environment to work with 00:11:55.110 --> 00:11:57.620 align:start position:0% specify the environment to work with Oriente<00:11:55.530> so<00:11:56.130> it<00:11:56.430> looks<00:11:57.030> complicated<00:11:57.300> but 00:11:57.620 --> 00:11:57.630 align:start position:0% Oriente so it looks complicated but 00:11:57.630 --> 00:12:00.740 align:start position:0% Oriente so it looks complicated but basically<00:11:58.260> you<00:11:58.500> can<00:11:58.680> specify<00:11:59.550> the<00:12:00.180> gas<00:12:00.390> limit 00:12:00.740 --> 00:12:00.750 align:start position:0% basically you can specify the gas limit 00:12:00.750 --> 00:12:04.160 align:start position:0% basically you can specify the gas limit the<00:12:01.500> difficulty<00:12:02.040> of<00:12:02.070> the<00:12:02.310> block<00:12:02.750> the<00:12:03.750> channel 00:12:04.160 --> 00:12:04.170 align:start position:0% the difficulty of the block the channel 00:12:04.170 --> 00:12:07.700 align:start position:0% the difficulty of the block the channel data<00:12:04.340> that<00:12:05.340> you<00:12:05.670> know<00:12:05.790> you<00:12:06.090> want<00:12:06.570> to<00:12:06.810> send<00:12:07.650> to 00:12:07.700 --> 00:12:07.710 align:start position:0% data that you know you want to send to 00:12:07.710 --> 00:12:10.370 align:start position:0% data that you know you want to send to the<00:12:07.860> function<00:12:08.250> you<00:12:09.060> can<00:12:09.660> also<00:12:09.780> specify<00:12:10.170> the 00:12:10.370 --> 00:12:10.380 align:start position:0% the function you can also specify the 00:12:10.380 --> 00:12:12.350 align:start position:0% the function you can also specify the archive<00:12:10.800> state<00:12:11.070> including<00:12:11.640> you<00:12:12.000> know<00:12:12.120> the 00:12:12.350 --> 00:12:12.360 align:start position:0% archive state including you know the 00:12:12.360 --> 00:12:17.500 align:start position:0% archive state including you know the balance<00:12:12.720> and<00:12:12.960> the<00:12:13.050> storage<00:12:14.120> of<00:12:15.120> some<00:12:15.360> of<00:12:15.480> cloud 00:12:17.500 --> 00:12:17.510 align:start position:0% balance and the storage of some of cloud 00:12:17.510 --> 00:12:19.850 align:start position:0% balance and the storage of some of cloud so<00:12:18.510> there<00:12:18.990> are<00:12:19.080> a<00:12:19.140> bunch<00:12:19.320> of<00:12:19.500> new<00:12:19.680> features 00:12:19.850 --> 00:12:19.860 align:start position:0% so there are a bunch of new features 00:12:19.860 --> 00:12:22.880 align:start position:0% so there are a bunch of new features that<00:12:20.070> we<00:12:20.520> are<00:12:20.640> planning<00:12:20.880> to<00:12:21.000> air<00:12:21.680> the<00:12:22.680> first 00:12:22.880 --> 00:12:22.890 align:start position:0% that we are planning to air the first 00:12:22.890 --> 00:12:24.970 align:start position:0% that we are planning to air the first one<00:12:23.040> is<00:12:23.220> to<00:12:23.520> generate<00:12:23.940> all<00:12:24.150> the<00:12:24.240> test<00:12:24.480> cases 00:12:24.970 --> 00:12:24.980 align:start position:0% one is to generate all the test cases 00:12:24.980 --> 00:12:27.830 align:start position:0% one is to generate all the test cases because<00:12:25.980> you<00:12:26.010> know<00:12:26.190> Oriente<00:12:26.670> visit<00:12:27.030> order<00:12:27.420> you 00:12:27.830 --> 00:12:27.840 align:start position:0% because you know Oriente visit order you 00:12:27.840 --> 00:12:29.150 align:start position:0% because you know Oriente visit order you know<00:12:27.930> all<00:12:28.080> the<00:12:28.230> possible<00:12:28.620> parts<00:12:28.950> of<00:12:29.040> the 00:12:29.150 --> 00:12:29.160 align:start position:0% know all the possible parts of the 00:12:29.160 --> 00:12:30.980 align:start position:0% know all the possible parts of the program<00:12:29.340> right<00:12:29.790> and<00:12:30.060> it<00:12:30.210> records<00:12:30.720> all<00:12:30.870> the 00:12:30.980 --> 00:12:30.990 align:start position:0% program right and it records all the 00:12:30.990 --> 00:12:33.170 align:start position:0% program right and it records all the behaviors<00:12:31.560> of<00:12:31.830> the<00:12:31.950> program<00:12:32.280> so<00:12:32.850> it<00:12:33.060> is 00:12:33.170 --> 00:12:33.180 align:start position:0% behaviors of the program so it is 00:12:33.180 --> 00:12:35.780 align:start position:0% behaviors of the program so it is possible<00:12:33.690> for<00:12:33.720> oriented<00:12:34.380> to<00:12:34.620> generate<00:12:35.580> the 00:12:35.780 --> 00:12:35.790 align:start position:0% possible for oriented to generate the 00:12:35.790 --> 00:12:37.940 align:start position:0% possible for oriented to generate the corresponding<00:12:36.090> input<00:12:36.870> that<00:12:37.230> drives<00:12:37.650> the 00:12:37.940 --> 00:12:37.950 align:start position:0% corresponding input that drives the 00:12:37.950 --> 00:12:41.240 align:start position:0% corresponding input that drives the program<00:12:38.390> to<00:12:39.390> the<00:12:39.660> same<00:12:39.930> part<00:12:40.170> so<00:12:40.980> basically 00:12:41.240 --> 00:12:41.250 align:start position:0% program to the same part so basically 00:12:41.250 --> 00:12:43.370 align:start position:0% program to the same part so basically you<00:12:41.700> can<00:12:41.880> you<00:12:42.240> know<00:12:42.330> use<00:12:42.570> all<00:12:42.870> the<00:12:43.050> other 00:12:43.370 --> 00:12:43.380 align:start position:0% you can you know use all the other 00:12:43.380 --> 00:12:47.330 align:start position:0% you can you know use all the other generated<00:12:44.190> input<00:12:45.020> as<00:12:46.020> a<00:12:46.080> test<00:12:46.470> guy<00:12:46.650> for<00:12:47.220> your 00:12:47.330 --> 00:12:47.340 align:start position:0% generated input as a test guy for your 00:12:47.340 --> 00:12:48.980 align:start position:0% generated input as a test guy for your smart<00:12:47.610> contract<00:12:47.970> and<00:12:48.150> use<00:12:48.360> it<00:12:48.540> in<00:12:48.750> other 00:12:48.980 --> 00:12:48.990 align:start position:0% smart contract and use it in other 00:12:48.990 --> 00:12:54.290 align:start position:0% smart contract and use it in other framework<00:12:49.410> like<00:12:49.590> shuffle<00:12:52.580> we<00:12:53.580> also<00:12:53.940> plan<00:12:54.270> to 00:12:54.290 --> 00:12:54.300 align:start position:0% framework like shuffle we also plan to 00:12:54.300 --> 00:12:56.660 align:start position:0% framework like shuffle we also plan to like<00:12:54.630> simply<00:12:55.020> simplify<00:12:55.620> all<00:12:56.040> the<00:12:56.160> constrain 00:12:56.660 --> 00:12:56.670 align:start position:0% like simply simplify all the constrain 00:12:56.670 --> 00:12:59.660 align:start position:0% like simply simplify all the constrain in<00:12:57.330> the<00:12:57.480> park<00:12:57.690> condition<00:12:58.140> so<00:12:58.650> for<00:12:59.100> example<00:12:59.460> if 00:12:59.660 --> 00:12:59.670 align:start position:0% in the park condition so for example if 00:12:59.670 --> 00:13:02.420 align:start position:0% in the park condition so for example if you<00:12:59.970> you<00:13:00.690> have<00:13:00.930> to<00:13:01.200> condition<00:13:02.040> like<00:13:02.220> you<00:13:02.340> know 00:13:02.420 --> 00:13:02.430 align:start position:0% you you have to condition like you know 00:13:02.430 --> 00:13:04.850 align:start position:0% you you have to condition like you know actually<00:13:03.090> it's<00:13:03.180> greater<00:13:03.390> than<00:13:03.540> zero<00:13:03.870> and<00:13:03.960> Isis 00:13:04.850 --> 00:13:04.860 align:start position:0% actually it's greater than zero and Isis 00:13:04.860 --> 00:13:08.120 align:start position:0% actually it's greater than zero and Isis small<00:13:05.550> less<00:13:05.970> than<00:13:06.150> 2<00:13:06.390> then<00:13:06.630> we<00:13:07.230> can<00:13:07.380> simplify 00:13:08.120 --> 00:13:08.130 align:start position:0% small less than 2 then we can simplify 00:13:08.130 --> 00:13:11.150 align:start position:0% small less than 2 then we can simplify it<00:13:08.370> to<00:13:08.670> you<00:13:09.120> know<00:13:09.210> X<00:13:09.420> equal<00:13:09.840> to<00:13:09.930> 1<00:13:10.110> so<00:13:10.800> that<00:13:10.830> will 00:13:11.150 --> 00:13:11.160 align:start position:0% it to you know X equal to 1 so that will 00:13:11.160 --> 00:13:13.700 align:start position:0% it to you know X equal to 1 so that will reduce<00:13:11.340> the<00:13:11.820> term<00:13:12.000> that<00:13:12.240> we<00:13:12.390> query<00:13:12.660> the<00:13:12.780> server 00:13:13.700 --> 00:13:13.710 align:start position:0% reduce the term that we query the server 00:13:13.710 --> 00:13:18.740 align:start position:0% reduce the term that we query the server or<00:13:14.070> the<00:13:14.460> theorem<00:13:14.910> prover<00:13:16.880> we<00:13:17.880> also<00:13:18.000> Li<00:13:18.180> want<00:13:18.600> to 00:13:18.740 --> 00:13:18.750 align:start position:0% or the theorem prover we also Li want to 00:13:18.750 --> 00:13:20.990 align:start position:0% or the theorem prover we also Li want to reduce<00:13:19.080> the<00:13:19.320> number<00:13:19.860> of<00:13:19.890> font<00:13:20.190> positive 00:13:20.990 --> 00:13:21.000 align:start position:0% reduce the number of font positive 00:13:21.000 --> 00:13:24.410 align:start position:0% reduce the number of font positive reports<00:13:22.100> in<00:13:23.100> order<00:13:23.250> to<00:13:23.490> provide<00:13:23.850> more<00:13:24.060> helpful 00:13:24.410 --> 00:13:24.420 align:start position:0% reports in order to provide more helpful 00:13:24.420 --> 00:13:29.690 align:start position:0% reports in order to provide more helpful feedback<00:13:24.630> to<00:13:24.960> the<00:13:25.080> developers<00:13:27.920> so<00:13:28.920> these<00:13:29.430> are 00:13:29.690 --> 00:13:29.700 align:start position:0% feedback to the developers so these are 00:13:29.700 --> 00:13:31.790 align:start position:0% feedback to the developers so these are all<00:13:29.940> the<00:13:30.120> other<00:13:30.330> new<00:13:31.020> features<00:13:31.050> that<00:13:31.620> we<00:13:31.770> are 00:13:31.790 --> 00:13:31.800 align:start position:0% all the other new features that we are 00:13:31.800 --> 00:13:35.020 align:start position:0% all the other new features that we are going<00:13:32.160> to<00:13:32.280> add<00:13:32.520> in<00:13:32.790> the<00:13:32.850> in<00:13:33.210> the<00:13:33.360> near<00:13:33.930> future 00:13:35.020 --> 00:13:35.030 align:start position:0% going to add in the in the near future 00:13:35.030 --> 00:13:37.880 align:start position:0% going to add in the in the near future right<00:13:36.030> so<00:13:36.390> with<00:13:36.660> that<00:13:36.780> I<00:13:36.839> want<00:13:37.080> to<00:13:37.140> conclude<00:13:37.800> my 00:13:37.880 --> 00:13:37.890 align:start position:0% right so with that I want to conclude my 00:13:37.890 --> 00:13:39.350 align:start position:0% right so with that I want to conclude my presentation 00:13:39.350 --> 00:13:39.360 align:start position:0% presentation 00:13:39.360 --> 00:13:42.470 align:start position:0% presentation again<00:13:39.720> this<00:13:40.200> is<00:13:40.380> the<00:13:40.500> URL<00:13:40.769> to<00:13:41.130> the<00:13:41.250> github<00:13:41.480> repo 00:13:42.470 --> 00:13:42.480 align:start position:0% again this is the URL to the github repo 00:13:42.480 --> 00:13:45.860 align:start position:0% again this is the URL to the github repo and<00:13:42.980> eientei<00:13:43.980> is<00:13:44.100> available<00:13:44.640> online 00:13:45.860 --> 00:13:45.870 align:start position:0% and eientei is available online 00:13:45.870 --> 00:13:48.230 align:start position:0% and eientei is available online these<00:13:46.290> are<00:13:46.500> automated<00:13:47.040> developer<00:13:47.459> volunteers 00:13:48.230 --> 00:13:48.240 align:start position:0% these are automated developer volunteers 00:13:48.240 --> 00:13:51.139 align:start position:0% these are automated developer volunteers that<00:13:48.839> have<00:13:49.019> you<00:13:49.829> know<00:13:49.950> been<00:13:50.160> contributing<00:13:51.120> to 00:13:51.139 --> 00:13:51.149 align:start position:0% that have you know been contributing to 00:13:51.149 --> 00:13:53.780 align:start position:0% that have you know been contributing to the<00:13:51.300> project<00:13:51.570> and<00:13:51.959> again<00:13:52.890> thanks<00:13:53.250> to<00:13:53.279> Mellon 00:13:53.780 --> 00:13:53.790 align:start position:0% the project and again thanks to Mellon 00:13:53.790 --> 00:13:56.210 align:start position:0% the project and again thanks to Mellon port<00:13:54.000> for<00:13:54.180> sponsoring<00:13:54.630> and<00:13:54.899> you<00:13:55.709> know<00:13:55.829> further 00:13:56.210 --> 00:13:56.220 align:start position:0% port for sponsoring and you know further 00:13:56.220 --> 00:13:59.460 align:start position:0% port for sponsoring and you know further supports<00:13:56.880> over 00:13:59.460 --> 00:13:59.470 align:start position:0% 00:13:59.470 --> 00:14:04.060 align:start position:0% [Applause] 00:14:04.060 --> 00:14:04.070 align:start position:0% [Applause] 00:14:04.070 --> 00:14:11.649 align:start position:0% [Applause] [Music]