WEBVTT Kind: captions Language: en 00:00:00.210 --> 00:00:18.630 align:start position:0% [Music] 00:00:18.630 --> 00:00:18.640 align:start position:0% 00:00:18.640 --> 00:00:21.160 align:start position:0% all<00:00:19.640> right<00:00:19.790> hope<00:00:20.270> everyone's<00:00:20.720> doing<00:00:20.780> good 00:00:21.160 --> 00:00:21.170 align:start position:0% all right hope everyone's doing good 00:00:21.170 --> 00:00:23.980 align:start position:0% all right hope everyone's doing good today<00:00:21.800> we're<00:00:22.130> going<00:00:22.400> to<00:00:22.520> talk<00:00:22.700> about<00:00:22.990> writing 00:00:23.980 --> 00:00:23.990 align:start position:0% today we're going to talk about writing 00:00:23.990 --> 00:00:25.260 align:start position:0% today we're going to talk about writing secure 00:00:25.260 --> 00:00:25.270 align:start position:0% secure 00:00:25.270 --> 00:00:27.300 align:start position:0% secure writing 00:00:27.300 --> 00:00:27.310 align:start position:0% writing 00:00:27.310 --> 00:00:31.330 align:start position:0% writing secure<00:00:28.310> and<00:00:28.640> correct<00:00:29.119> smart<00:00:29.420> contracts<00:00:30.130> so<00:00:31.130> in 00:00:31.330 --> 00:00:31.340 align:start position:0% secure and correct smart contracts so in 00:00:31.340 --> 00:00:32.950 align:start position:0% secure and correct smart contracts so in particular<00:00:31.520> I'm<00:00:31.939> going<00:00:31.970> to<00:00:32.119> talk<00:00:32.180> about<00:00:32.480> some 00:00:32.950 --> 00:00:32.960 align:start position:0% particular I'm going to talk about some 00:00:32.960 --> 00:00:34.480 align:start position:0% particular I'm going to talk about some directions<00:00:33.500> and<00:00:33.680> some<00:00:33.860> problems<00:00:34.310> we've<00:00:34.460> been 00:00:34.480 --> 00:00:34.490 align:start position:0% directions and some problems we've been 00:00:34.490 --> 00:00:36.640 align:start position:0% directions and some problems we've been thinking<00:00:34.820> about<00:00:34.880> in<00:00:35.150> academia<00:00:35.720> and<00:00:35.930> I'll<00:00:36.440> also 00:00:36.640 --> 00:00:36.650 align:start position:0% thinking about in academia and I'll also 00:00:36.650 --> 00:00:38.050 align:start position:0% thinking about in academia and I'll also try<00:00:36.829> to<00:00:37.010> tie<00:00:37.220> it<00:00:37.280> into<00:00:37.550> an<00:00:37.790> industry 00:00:38.050 --> 00:00:38.060 align:start position:0% try to tie it into an industry 00:00:38.060 --> 00:00:39.640 align:start position:0% try to tie it into an industry perspective<00:00:38.360> for<00:00:38.989> those<00:00:39.200> of<00:00:39.350> you<00:00:39.440> who<00:00:39.560> are 00:00:39.640 --> 00:00:39.650 align:start position:0% perspective for those of you who are 00:00:39.650 --> 00:00:42.760 align:start position:0% perspective for those of you who are smart<00:00:39.920> contract<00:00:40.370> practitioners<00:00:41.140> alright<00:00:42.140> so 00:00:42.760 --> 00:00:42.770 align:start position:0% smart contract practitioners alright so 00:00:42.770 --> 00:00:45.970 align:start position:0% smart contract practitioners alright so let's<00:00:43.160> start<00:00:43.250> out<00:00:43.520> with<00:00:43.550> who<00:00:43.790> is<00:00:43.970> IC<00:00:44.480> 3<00:00:44.660> IC<00:00:45.590> 3<00:00:45.860> is 00:00:45.970 --> 00:00:45.980 align:start position:0% let's start out with who is IC 3 IC 3 is 00:00:45.980 --> 00:00:47.710 align:start position:0% let's start out with who is IC 3 IC 3 is sort<00:00:46.190> of<00:00:46.250> a<00:00:46.370> research<00:00:46.700> hub<00:00:46.970> centered<00:00:47.630> around 00:00:47.710 --> 00:00:47.720 align:start position:0% sort of a research hub centered around 00:00:47.720 --> 00:00:49.780 align:start position:0% sort of a research hub centered around the<00:00:47.960> universities<00:00:48.470> you<00:00:48.590> see<00:00:48.770> they're<00:00:48.980> mostly 00:00:49.780 --> 00:00:49.790 align:start position:0% the universities you see they're mostly 00:00:49.790 --> 00:00:52.150 align:start position:0% the universities you see they're mostly Cornell<00:00:50.180> University<00:00:50.780> also<00:00:50.990> UI<00:00:51.320> UC<00:00:51.680> Berkeley 00:00:52.150 --> 00:00:52.160 align:start position:0% Cornell University also UI UC Berkeley 00:00:52.160 --> 00:00:54.760 align:start position:0% Cornell University also UI UC Berkeley Cornell<00:00:52.490> Tech<00:00:52.700> and<00:00:52.910> the<00:00:53.180> Technion<00:00:53.590> we've<00:00:54.590> got 00:00:54.760 --> 00:00:54.770 align:start position:0% Cornell Tech and the Technion we've got 00:00:54.770 --> 00:00:56.650 align:start position:0% Cornell Tech and the Technion we've got 12<00:00:55.070> faculty<00:00:55.610> at<00:00:55.730> the<00:00:55.820> last<00:00:56.000> count<00:00:56.300> and<00:00:56.510> we're 00:00:56.650 --> 00:00:56.660 align:start position:0% 12 faculty at the last count and we're 00:00:56.660 --> 00:00:58.210 align:start position:0% 12 faculty at the last count and we're adding<00:00:56.960> more<00:00:56.990> all<00:00:57.260> the<00:00:57.380> time<00:00:57.620> in<00:00:57.890> the<00:00:58.040> last 00:00:58.210 --> 00:00:58.220 align:start position:0% adding more all the time in the last 00:00:58.220 --> 00:00:59.800 align:start position:0% adding more all the time in the last month<00:00:58.520> we've<00:00:58.730> added<00:00:58.940> at<00:00:59.120> least<00:00:59.390> two<00:00:59.660> or<00:00:59.780> three 00:00:59.800 --> 00:00:59.810 align:start position:0% month we've added at least two or three 00:00:59.810 --> 00:01:02.800 align:start position:0% month we've added at least two or three faculty<00:01:00.440> and<00:01:00.650> we've<00:01:01.490> got<00:01:01.730> many<00:01:02.000> many<00:01:02.300> students 00:01:02.800 --> 00:01:02.810 align:start position:0% faculty and we've got many many students 00:01:02.810 --> 00:01:05.550 align:start position:0% faculty and we've got many many students at<00:01:02.990> all<00:01:03.290> levels<00:01:03.320> of<00:01:03.800> education 00:01:05.550 --> 00:01:05.560 align:start position:0% at all levels of education 00:01:05.560 --> 00:01:08.350 align:start position:0% at all levels of education so<00:01:06.560> before<00:01:07.430> I<00:01:07.460> start<00:01:07.790> I'd<00:01:07.909> like<00:01:07.939> to<00:01:08.090> give<00:01:08.330> a 00:01:08.350 --> 00:01:08.360 align:start position:0% so before I start I'd like to give a 00:01:08.360 --> 00:01:09.730 align:start position:0% so before I start I'd like to give a special<00:01:08.600> thanks<00:01:09.020> to<00:01:09.080> the<00:01:09.350> etherium 00:01:09.730 --> 00:01:09.740 align:start position:0% special thanks to the etherium 00:01:09.740 --> 00:01:11.620 align:start position:0% special thanks to the etherium foundation<00:01:10.280> for<00:01:10.640> inviting<00:01:11.030> us<00:01:11.150> here<00:01:11.180> and 00:01:11.620 --> 00:01:11.630 align:start position:0% foundation for inviting us here and 00:01:11.630 --> 00:01:12.999 align:start position:0% foundation for inviting us here and putting<00:01:11.960> in<00:01:12.049> all<00:01:12.140> the<00:01:12.259> work<00:01:12.409> to<00:01:12.710> bring<00:01:12.890> us 00:01:12.999 --> 00:01:13.009 align:start position:0% putting in all the work to bring us 00:01:13.009 --> 00:01:15.190 align:start position:0% putting in all the work to bring us together<00:01:13.159> and<00:01:14.000> also<00:01:14.360> to<00:01:14.509> our<00:01:14.750> industry 00:01:15.190 --> 00:01:15.200 align:start position:0% together and also to our industry 00:01:15.200 --> 00:01:18.219 align:start position:0% together and also to our industry partners<00:01:15.619> at<00:01:15.890> chain<00:01:16.310> digital<00:01:17.180> asset<00:01:17.600> and<00:01:17.810> IBM 00:01:18.219 --> 00:01:18.229 align:start position:0% partners at chain digital asset and IBM 00:01:18.229 --> 00:01:19.750 align:start position:0% partners at chain digital asset and IBM thank<00:01:18.680> you<00:01:18.770> guys<00:01:18.920> very<00:01:19.070> much<00:01:19.280> for<00:01:19.670> your 00:01:19.750 --> 00:01:19.760 align:start position:0% thank you guys very much for your 00:01:19.760 --> 00:01:21.520 align:start position:0% thank you guys very much for your continued<00:01:20.150> support<00:01:20.330> of<00:01:20.600> smart<00:01:21.080> contract 00:01:21.520 --> 00:01:21.530 align:start position:0% continued support of smart contract 00:01:21.530 --> 00:01:24.070 align:start position:0% continued support of smart contract research<00:01:22.000> will<00:01:23.000> also<00:01:23.270> be<00:01:23.390> announcing<00:01:23.900> more 00:01:24.070 --> 00:01:24.080 align:start position:0% research will also be announcing more 00:01:24.080 --> 00:01:26.500 align:start position:0% research will also be announcing more partners<00:01:24.470> in<00:01:24.770> the<00:01:24.920> coming<00:01:25.220> weeks<00:01:25.400> and<00:01:25.730> we'd 00:01:26.500 --> 00:01:26.510 align:start position:0% partners in the coming weeks and we'd 00:01:26.510 --> 00:01:27.820 align:start position:0% partners in the coming weeks and we'd love<00:01:26.659> to<00:01:26.720> have<00:01:26.900> you<00:01:27.080> guys<00:01:27.200> as<00:01:27.409> a<00:01:27.440> partner<00:01:27.800> I 00:01:27.820 --> 00:01:27.830 align:start position:0% love to have you guys as a partner I 00:01:27.830 --> 00:01:29.290 align:start position:0% love to have you guys as a partner I know<00:01:27.980> there<00:01:28.280> are<00:01:28.370> a<00:01:28.400> lot<00:01:28.460> of<00:01:28.670> companies<00:01:29.060> here 00:01:29.290 --> 00:01:29.300 align:start position:0% know there are a lot of companies here 00:01:29.300 --> 00:01:31.210 align:start position:0% know there are a lot of companies here who<00:01:29.480> are<00:01:29.600> interested<00:01:30.260> in<00:01:30.350> the<00:01:30.830> correctness 00:01:31.210 --> 00:01:31.220 align:start position:0% who are interested in the correctness 00:01:31.220 --> 00:01:33.310 align:start position:0% who are interested in the correctness and<00:01:31.490> performance<00:01:31.550> of<00:01:32.210> crypto<00:01:32.870> currencies 00:01:33.310 --> 00:01:33.320 align:start position:0% and performance of crypto currencies 00:01:33.320 --> 00:01:35.500 align:start position:0% and performance of crypto currencies blog<00:01:33.620> chains<00:01:33.950> and<00:01:34.100> smart<00:01:34.340> contracts<00:01:34.790> so<00:01:35.390> if 00:01:35.500 --> 00:01:35.510 align:start position:0% blog chains and smart contracts so if 00:01:35.510 --> 00:01:37.060 align:start position:0% blog chains and smart contracts so if that's<00:01:35.659> you<00:01:35.930> please<00:01:36.260> feel<00:01:36.470> free<00:01:36.560> to<00:01:36.740> check<00:01:36.920> out 00:01:37.060 --> 00:01:37.070 align:start position:0% that's you please feel free to check out 00:01:37.070 --> 00:01:39.190 align:start position:0% that's you please feel free to check out our<00:01:37.220> website<00:01:37.400> at<00:01:37.790> an<00:01:37.880> its<00:01:38.030> e3<00:01:38.180> organ<00:01:38.780> contact 00:01:39.190 --> 00:01:39.200 align:start position:0% our website at an its e3 organ contact 00:01:39.200 --> 00:01:42.730 align:start position:0% our website at an its e3 organ contact us<00:01:39.550> alright<00:01:40.760> so<00:01:41.000> here<00:01:41.690> is<00:01:41.840> the<00:01:42.020> work<00:01:42.140> that<00:01:42.170> IC<00:01:42.590> 3 00:01:42.730 --> 00:01:42.740 align:start position:0% us alright so here is the work that IC 3 00:01:42.740 --> 00:01:44.590 align:start position:0% us alright so here is the work that IC 3 is<00:01:42.920> doing<00:01:43.220> as<00:01:43.400> far<00:01:43.760> as<00:01:43.880> we<00:01:44.000> see<00:01:44.180> it<00:01:44.299> there<00:01:44.479> are 00:01:44.590 --> 00:01:44.600 align:start position:0% is doing as far as we see it there are 00:01:44.600 --> 00:01:46.480 align:start position:0% is doing as far as we see it there are five<00:01:44.810> Grand<00:01:45.140> Challenges<00:01:45.590> in<00:01:45.650> smart<00:01:46.070> contract 00:01:46.480 --> 00:01:46.490 align:start position:0% five Grand Challenges in smart contract 00:01:46.490 --> 00:01:47.350 align:start position:0% five Grand Challenges in smart contract performance 00:01:47.350 --> 00:01:47.360 align:start position:0% performance 00:01:47.360 --> 00:01:49.480 align:start position:0% performance sorry<00:01:48.110> smart<00:01:48.380> contracts<00:01:48.799> and<00:01:49.100> crypto 00:01:49.480 --> 00:01:49.490 align:start position:0% sorry smart contracts and crypto 00:01:49.490 --> 00:01:51.250 align:start position:0% sorry smart contracts and crypto currencies<00:01:49.909> one<00:01:50.299> of<00:01:50.390> them<00:01:50.540> is<00:01:50.690> scaling<00:01:51.170> in 00:01:51.250 --> 00:01:51.260 align:start position:0% currencies one of them is scaling in 00:01:51.260 --> 00:01:52.930 align:start position:0% currencies one of them is scaling in performance<00:01:51.770> the<00:01:52.370> second<00:01:52.700> one<00:01:52.820> is 00:01:52.930 --> 00:01:52.940 align:start position:0% performance the second one is 00:01:52.940 --> 00:01:55.060 align:start position:0% performance the second one is correctness<00:01:53.360> third<00:01:54.200> one<00:01:54.380> is<00:01:54.500> confidentiality 00:01:55.060 --> 00:01:55.070 align:start position:0% correctness third one is confidentiality 00:01:55.070 --> 00:01:57.910 align:start position:0% correctness third one is confidentiality the<00:01:55.580> fourth<00:01:56.240> one<00:01:56.450> is<00:01:56.479> authenticated<00:01:57.260> data<00:01:57.560> so 00:01:57.910 --> 00:01:57.920 align:start position:0% the fourth one is authenticated data so 00:01:57.920 --> 00:01:59.649 align:start position:0% the fourth one is authenticated data so getting<00:01:58.220> data<00:01:58.340> sources<00:01:58.700> into<00:01:58.940> these<00:01:59.119> systems 00:01:59.649 --> 00:01:59.659 align:start position:0% getting data sources into these systems 00:01:59.659 --> 00:02:01.450 align:start position:0% getting data sources into these systems and<00:02:00.080> the<00:02:00.500> last<00:02:00.710> one<00:02:00.860> is<00:02:00.979> safety<00:02:01.340> and 00:02:01.450 --> 00:02:01.460 align:start position:0% and the last one is safety and 00:02:01.460 --> 00:02:02.500 align:start position:0% and the last one is safety and compliance<00:02:01.580> which<00:02:02.030> you've<00:02:02.180> heard<00:02:02.210> a<00:02:02.420> little 00:02:02.500 --> 00:02:02.510 align:start position:0% compliance which you've heard a little 00:02:02.510 --> 00:02:04.960 align:start position:0% compliance which you've heard a little bit<00:02:02.630> about<00:02:02.869> today<00:02:03.369> so<00:02:04.369> this<00:02:04.520> talk<00:02:04.729> I'm<00:02:04.880> gonna 00:02:04.960 --> 00:02:04.970 align:start position:0% bit about today so this talk I'm gonna 00:02:04.970 --> 00:02:06.700 align:start position:0% bit about today so this talk I'm gonna be<00:02:05.150> focusing<00:02:05.540> on<00:02:05.690> correctness<00:02:06.170> and<00:02:06.500> its 00:02:06.700 --> 00:02:06.710 align:start position:0% be focusing on correctness and its 00:02:06.710 --> 00:02:08.320 align:start position:0% be focusing on correctness and its relationship<00:02:07.130> to<00:02:07.280> security<00:02:07.820> and<00:02:08.000> how<00:02:08.269> we 00:02:08.320 --> 00:02:08.330 align:start position:0% relationship to security and how we 00:02:08.330 --> 00:02:09.759 align:start position:0% relationship to security and how we write<00:02:08.659> your<00:02:08.869> secure<00:02:09.140> and<00:02:09.259> correct<00:02:09.500> smart 00:02:09.759 --> 00:02:09.769 align:start position:0% write your secure and correct smart 00:02:09.769 --> 00:02:12.160 align:start position:0% write your secure and correct smart contracts<00:02:10.299> so<00:02:11.299> this<00:02:11.420> is<00:02:11.540> intended<00:02:11.810> to<00:02:11.989> be<00:02:12.140> a 00:02:12.160 --> 00:02:12.170 align:start position:0% contracts so this is intended to be a 00:02:12.170 --> 00:02:13.869 align:start position:0% contracts so this is intended to be a high<00:02:12.379> level<00:02:12.409> overview<00:02:12.860> we're<00:02:13.430> not<00:02:13.580> trying<00:02:13.819> to 00:02:13.869 --> 00:02:13.879 align:start position:0% high level overview we're not trying to 00:02:13.879 --> 00:02:15.190 align:start position:0% high level overview we're not trying to be<00:02:13.970> comprehensive<00:02:14.269> here<00:02:14.689> there's<00:02:14.900> a<00:02:14.959> lot<00:02:15.110> of 00:02:15.190 --> 00:02:15.200 align:start position:0% be comprehensive here there's a lot of 00:02:15.200 --> 00:02:17.440 align:start position:0% be comprehensive here there's a lot of work<00:02:15.349> we're<00:02:15.500> not<00:02:15.530> gonna<00:02:15.799> mention<00:02:16.239> we're<00:02:17.239> also 00:02:17.440 --> 00:02:17.450 align:start position:0% work we're not gonna mention we're also 00:02:17.450 --> 00:02:18.970 align:start position:0% work we're not gonna mention we're also going<00:02:17.780> to<00:02:17.840> provide<00:02:18.080> some<00:02:18.290> suggestions<00:02:18.620> for 00:02:18.970 --> 00:02:18.980 align:start position:0% going to provide some suggestions for 00:02:18.980 --> 00:02:20.320 align:start position:0% going to provide some suggestions for practitioners<00:02:19.549> since<00:02:19.819> there<00:02:19.970> are<00:02:20.090> many<00:02:20.239> of 00:02:20.320 --> 00:02:20.330 align:start position:0% practitioners since there are many of 00:02:20.330 --> 00:02:21.490 align:start position:0% practitioners since there are many of you<00:02:20.420> guys<00:02:20.510> in<00:02:20.569> the<00:02:20.750> room<00:02:20.959> writing<00:02:21.170> smart 00:02:21.490 --> 00:02:21.500 align:start position:0% you guys in the room writing smart 00:02:21.500 --> 00:02:23.530 align:start position:0% you guys in the room writing smart contracts<00:02:21.980> and<00:02:22.220> I'm<00:02:22.700> gonna<00:02:22.819> draw<00:02:23.060> frequent 00:02:23.530 --> 00:02:23.540 align:start position:0% contracts and I'm gonna draw frequent 00:02:23.540 --> 00:02:24.970 align:start position:0% contracts and I'm gonna draw frequent parallels<00:02:23.959> to<00:02:24.080> safety<00:02:24.500> critical<00:02:24.620> software 00:02:24.970 --> 00:02:24.980 align:start position:0% parallels to safety critical software 00:02:24.980 --> 00:02:27.300 align:start position:0% parallels to safety critical software whether<00:02:25.490> they<00:02:25.670> be<00:02:25.730> in<00:02:25.880> planes<00:02:26.240> cars 00:02:27.300 --> 00:02:27.310 align:start position:0% whether they be in planes cars 00:02:27.310 --> 00:02:28.860 align:start position:0% whether they be in planes cars power<00:02:27.700> grids<00:02:28.060> or<00:02:28.180> other<00:02:28.330> infrastructure 00:02:28.860 --> 00:02:28.870 align:start position:0% power grids or other infrastructure 00:02:28.870 --> 00:02:32.490 align:start position:0% power grids or other infrastructure systems<00:02:29.520> and<00:02:30.520> software<00:02:31.030> like<00:02:31.209> that<00:02:31.420> all<00:02:32.319> right 00:02:32.490 --> 00:02:32.500 align:start position:0% systems and software like that all right 00:02:32.500 --> 00:02:34.290 align:start position:0% systems and software like that all right so<00:02:32.890> we<00:02:33.099> all<00:02:33.130> know<00:02:33.400> this<00:02:33.520> problem<00:02:33.940> pretty<00:02:34.120> well 00:02:34.290 --> 00:02:34.300 align:start position:0% so we all know this problem pretty well 00:02:34.300 --> 00:02:36.449 align:start position:0% so we all know this problem pretty well by<00:02:34.480> now<00:02:34.630> as<00:02:34.810> a<00:02:34.840> community<00:02:35.319> the<00:02:35.920> problem<00:02:36.220> is<00:02:36.370> you 00:02:36.449 --> 00:02:36.459 align:start position:0% by now as a community the problem is you 00:02:36.459 --> 00:02:38.850 align:start position:0% by now as a community the problem is you have<00:02:36.489> this<00:02:36.790> software<00:02:37.120> bug<00:02:37.330> it<00:02:37.720> leads<00:02:38.290> to<00:02:38.440> money 00:02:38.850 --> 00:02:38.860 align:start position:0% have this software bug it leads to money 00:02:38.860 --> 00:02:41.370 align:start position:0% have this software bug it leads to money being<00:02:39.190> lost<00:02:39.489> or<00:02:39.849> stolen<00:02:40.120> and<00:02:40.510> then<00:02:40.959> people<00:02:41.260> who 00:02:41.370 --> 00:02:41.380 align:start position:0% being lost or stolen and then people who 00:02:41.380 --> 00:02:42.630 align:start position:0% being lost or stolen and then people who write<00:02:41.590> and<00:02:41.800> participate<00:02:42.220> in<00:02:42.340> the<00:02:42.400> smart 00:02:42.630 --> 00:02:42.640 align:start position:0% write and participate in the smart 00:02:42.640 --> 00:02:44.300 align:start position:0% write and participate in the smart contracts<00:02:43.120> cry 00:02:44.300 --> 00:02:44.310 align:start position:0% contracts cry 00:02:44.310 --> 00:02:46.350 align:start position:0% contracts cry so<00:02:45.310> there<00:02:45.519> are<00:02:45.640> some<00:02:45.819> things<00:02:46.000> about<00:02:46.090> this 00:02:46.350 --> 00:02:46.360 align:start position:0% so there are some things about this 00:02:46.360 --> 00:02:47.880 align:start position:0% so there are some things about this challenge<00:02:46.720> that<00:02:46.810> are<00:02:46.930> definitely<00:02:47.110> unique<00:02:47.500> to 00:02:47.880 --> 00:02:47.890 align:start position:0% challenge that are definitely unique to 00:02:47.890 --> 00:02:50.059 align:start position:0% challenge that are definitely unique to the<00:02:47.980> cryptocurrency<00:02:48.280> and<00:02:48.670> smart<00:02:49.000> contract 00:02:50.059 --> 00:02:50.069 align:start position:0% the cryptocurrency and smart contract 00:02:50.069 --> 00:02:52.890 align:start position:0% the cryptocurrency and smart contract ecosystem<00:02:51.069> one<00:02:52.000> of<00:02:52.090> those<00:02:52.239> is<00:02:52.390> that<00:02:52.420> security 00:02:52.890 --> 00:02:52.900 align:start position:0% ecosystem one of those is that security 00:02:52.900 --> 00:02:54.930 align:start position:0% ecosystem one of those is that security is<00:02:53.200> more<00:02:53.440> closely<00:02:53.769> tied<00:02:54.099> to<00:02:54.310> code<00:02:54.519> correctness 00:02:54.930 --> 00:02:54.940 align:start position:0% is more closely tied to code correctness 00:02:54.940 --> 00:02:57.240 align:start position:0% is more closely tied to code correctness than<00:02:55.239> anywhere<00:02:55.599> else<00:02:55.660> so<00:02:56.080> you<00:02:56.800> have<00:02:56.980> this<00:02:57.099> sort 00:02:57.240 --> 00:02:57.250 align:start position:0% than anywhere else so you have this sort 00:02:57.250 --> 00:02:58.830 align:start position:0% than anywhere else so you have this sort of<00:02:57.340> problem<00:02:57.489> that<00:02:57.730> any<00:02:58.000> issue<00:02:58.239> in<00:02:58.450> correctness 00:02:58.830 --> 00:02:58.840 align:start position:0% of problem that any issue in correctness 00:02:58.840 --> 00:03:00.600 align:start position:0% of problem that any issue in correctness which<00:02:59.110> leads<00:02:59.380> to<00:02:59.470> a<00:02:59.590> fault<00:02:59.890> or<00:03:00.069> software<00:03:00.430> bug 00:03:00.600 --> 00:03:00.610 align:start position:0% which leads to a fault or software bug 00:03:00.610 --> 00:03:03.870 align:start position:0% which leads to a fault or software bug may<00:03:01.180> be<00:03:01.239> directly<00:03:01.780> monetizable<00:03:02.760> by<00:03:03.760> an 00:03:03.870 --> 00:03:03.880 align:start position:0% may be directly monetizable by an 00:03:03.880 --> 00:03:06.030 align:start position:0% may be directly monetizable by an attacker<00:03:04.180> and<00:03:04.420> these<00:03:05.230> attackers<00:03:05.530> can<00:03:05.830> also 00:03:06.030 --> 00:03:06.040 align:start position:0% attacker and these attackers can also 00:03:06.040 --> 00:03:09.199 align:start position:0% attacker and these attackers can also anonymously<00:03:06.850> monetize<00:03:07.360> these<00:03:07.860> exploits 00:03:09.199 --> 00:03:09.209 align:start position:0% anonymously monetize these exploits 00:03:09.209 --> 00:03:12.509 align:start position:0% anonymously monetize these exploits untraceable<00:03:10.600> we've<00:03:11.080> also<00:03:11.290> got<00:03:11.590> a<00:03:11.980> unique 00:03:12.509 --> 00:03:12.519 align:start position:0% untraceable we've also got a unique 00:03:12.519 --> 00:03:14.820 align:start position:0% untraceable we've also got a unique adversarial<00:03:13.390> environment<00:03:13.959> here<00:03:14.230> so 00:03:14.820 --> 00:03:14.830 align:start position:0% adversarial environment here so 00:03:14.830 --> 00:03:16.559 align:start position:0% adversarial environment here so everything<00:03:15.519> that<00:03:15.670> runs<00:03:15.790> on<00:03:16.030> these<00:03:16.180> systems 00:03:16.559 --> 00:03:16.569 align:start position:0% everything that runs on these systems 00:03:16.569 --> 00:03:19.199 align:start position:0% everything that runs on these systems from<00:03:16.780> the<00:03:16.840> miners<00:03:17.319> to<00:03:17.530> the<00:03:17.650> node<00:03:17.830> network<00:03:18.250> to 00:03:19.199 --> 00:03:19.209 align:start position:0% from the miners to the node network to 00:03:19.209 --> 00:03:20.550 align:start position:0% from the miners to the node network to the<00:03:19.360> actors<00:03:19.750> that<00:03:19.900> participate<00:03:20.380> in<00:03:20.410> the 00:03:20.550 --> 00:03:20.560 align:start position:0% the actors that participate in the 00:03:20.560 --> 00:03:21.870 align:start position:0% the actors that participate in the contracts<00:03:20.980> could<00:03:21.220> potentially<00:03:21.760> be 00:03:21.870 --> 00:03:21.880 align:start position:0% contracts could potentially be 00:03:21.880 --> 00:03:24.059 align:start position:0% contracts could potentially be adversarial<00:03:22.510> and<00:03:22.780> if<00:03:23.500> it's<00:03:23.650> not<00:03:23.830> bad<00:03:24.010> enough 00:03:24.059 --> 00:03:24.069 align:start position:0% adversarial and if it's not bad enough 00:03:24.069 --> 00:03:26.339 align:start position:0% adversarial and if it's not bad enough already<00:03:24.610> we're<00:03:24.910> looking<00:03:25.150> at<00:03:25.269> public<00:03:25.480> code<00:03:25.870> so 00:03:26.339 --> 00:03:26.349 align:start position:0% already we're looking at public code so 00:03:26.349 --> 00:03:28.320 align:start position:0% already we're looking at public code so in<00:03:26.650> your<00:03:26.739> car<00:03:27.040> or<00:03:27.370> in<00:03:27.519> an<00:03:27.610> airplane<00:03:27.910> you<00:03:28.030> don't 00:03:28.320 --> 00:03:28.330 align:start position:0% in your car or in an airplane you don't 00:03:28.330 --> 00:03:29.670 align:start position:0% in your car or in an airplane you don't have<00:03:28.480> access<00:03:28.660> to<00:03:28.930> the<00:03:29.140> code<00:03:29.319> that's<00:03:29.530> running 00:03:29.670 --> 00:03:29.680 align:start position:0% have access to the code that's running 00:03:29.680 --> 00:03:32.190 align:start position:0% have access to the code that's running to<00:03:29.950> try<00:03:30.099> to<00:03:30.160> test<00:03:30.370> it<00:03:30.580> for<00:03:30.670> exploits<00:03:31.120> but<00:03:32.079> on 00:03:32.190 --> 00:03:32.200 align:start position:0% to try to test it for exploits but on 00:03:32.200 --> 00:03:34.110 align:start position:0% to try to test it for exploits but on smart<00:03:32.500> contracts<00:03:32.950> all<00:03:33.220> code<00:03:33.489> is<00:03:33.640> public<00:03:34.000> on 00:03:34.110 --> 00:03:34.120 align:start position:0% smart contracts all code is public on 00:03:34.120 --> 00:03:36.630 align:start position:0% smart contracts all code is public on the<00:03:34.209> blockchain<00:03:34.420> all<00:03:35.019> right<00:03:36.010> so<00:03:36.310> how<00:03:36.459> do<00:03:36.519> we 00:03:36.630 --> 00:03:36.640 align:start position:0% the blockchain all right so how do we 00:03:36.640 --> 00:03:37.800 align:start position:0% the blockchain all right so how do we start<00:03:36.880> tackling<00:03:37.239> this<00:03:37.450> pretty<00:03:37.630> difficult 00:03:37.800 --> 00:03:37.810 align:start position:0% start tackling this pretty difficult 00:03:37.810 --> 00:03:39.930 align:start position:0% start tackling this pretty difficult problem<00:03:38.380> as<00:03:38.980> far<00:03:39.220> as<00:03:39.250> we<00:03:39.430> see<00:03:39.609> it<00:03:39.700> there<00:03:39.820> are 00:03:39.930 --> 00:03:39.940 align:start position:0% problem as far as we see it there are 00:03:39.940 --> 00:03:42.479 align:start position:0% problem as far as we see it there are three<00:03:39.970> prongs<00:03:40.480> here<00:03:40.780> that<00:03:41.109> will<00:03:41.290> help<00:03:41.410> us<00:03:41.620> sort 00:03:42.479 --> 00:03:42.489 align:start position:0% three prongs here that will help us sort 00:03:42.489 --> 00:03:43.860 align:start position:0% three prongs here that will help us sort of<00:03:42.549> stick<00:03:42.760> a<00:03:42.790> fork<00:03:43.120> in<00:03:43.269> this<00:03:43.420> problem<00:03:43.750> with 00:03:43.860 --> 00:03:43.870 align:start position:0% of stick a fork in this problem with 00:03:43.870 --> 00:03:45.539 align:start position:0% of stick a fork in this problem with smart<00:03:44.140> contract<00:03:44.590> correctness<00:03:44.890> and<00:03:45.100> security 00:03:45.539 --> 00:03:45.549 align:start position:0% smart contract correctness and security 00:03:45.549 --> 00:03:47.490 align:start position:0% smart contract correctness and security the<00:03:46.090> first<00:03:46.299> one<00:03:46.450> is<00:03:46.569> formal<00:03:46.870> verification<00:03:46.989> and 00:03:47.490 --> 00:03:47.500 align:start position:0% the first one is formal verification and 00:03:47.500 --> 00:03:49.830 align:start position:0% the first one is formal verification and specification<00:03:48.190> the<00:03:48.670> second<00:03:49.030> one<00:03:49.150> is<00:03:49.359> escape 00:03:49.830 --> 00:03:49.840 align:start position:0% specification the second one is escape 00:03:49.840 --> 00:03:51.660 align:start position:0% specification the second one is escape hatches<00:03:50.079> or<00:03:50.440> otherwise<00:03:51.130> known<00:03:51.310> as<00:03:51.370> kill 00:03:51.660 --> 00:03:51.670 align:start position:0% hatches or otherwise known as kill 00:03:51.670 --> 00:03:54.000 align:start position:0% hatches or otherwise known as kill switches<00:03:52.060> and<00:03:52.269> the<00:03:52.810> last<00:03:53.019> one<00:03:53.290> is<00:03:53.560> bug 00:03:54.000 --> 00:03:54.010 align:start position:0% switches and the last one is bug 00:03:54.010 --> 00:03:55.220 align:start position:0% switches and the last one is bug bounties 00:03:55.220 --> 00:03:55.230 align:start position:0% bounties 00:03:55.230 --> 00:03:57.569 align:start position:0% bounties so<00:03:56.230> getting<00:03:56.500> right<00:03:56.650> into<00:03:56.799> it<00:03:57.010> we're<00:03:57.430> going<00:03:57.519> to 00:03:57.569 --> 00:03:57.579 align:start position:0% so getting right into it we're going to 00:03:57.579 --> 00:04:00.090 align:start position:0% so getting right into it we're going to talk<00:03:57.790> about<00:03:57.819> formal<00:03:58.420> verification<00:03:58.600> here<00:03:59.260> so 00:04:00.090 --> 00:04:00.100 align:start position:0% talk about formal verification here so 00:04:00.100 --> 00:04:01.860 align:start position:0% talk about formal verification here so formal<00:04:00.459> verification<00:04:00.609> is<00:04:01.329> probably<00:04:01.780> the 00:04:01.860 --> 00:04:01.870 align:start position:0% formal verification is probably the 00:04:01.870 --> 00:04:03.240 align:start position:0% formal verification is probably the hottest<00:04:01.989> topic<00:04:02.500> of<00:04:02.620> these<00:04:02.769> three<00:04:03.069> in<00:04:03.160> the 00:04:03.240 --> 00:04:03.250 align:start position:0% hottest topic of these three in the 00:04:03.250 --> 00:04:04.650 align:start position:0% hottest topic of these three in the community<00:04:03.639> right<00:04:03.790> now<00:04:04.000> there<00:04:04.359> are<00:04:04.450> several 00:04:04.650 --> 00:04:04.660 align:start position:0% community right now there are several 00:04:04.660 --> 00:04:07.140 align:start position:0% community right now there are several talks<00:04:05.100> going<00:04:06.100> on<00:04:06.310> about<00:04:06.549> it<00:04:06.730> at<00:04:06.850> this<00:04:07.000> event 00:04:07.140 --> 00:04:07.150 align:start position:0% talks going on about it at this event 00:04:07.150 --> 00:04:09.000 align:start position:0% talks going on about it at this event and<00:04:07.450> it's<00:04:07.660> a<00:04:07.750> really<00:04:07.930> exciting<00:04:08.260> space<00:04:08.650> to<00:04:08.889> be 00:04:09.000 --> 00:04:09.010 align:start position:0% and it's a really exciting space to be 00:04:09.010 --> 00:04:11.280 align:start position:0% and it's a really exciting space to be in<00:04:09.269> so<00:04:10.269> what<00:04:10.450> do<00:04:10.510> we<00:04:10.569> like<00:04:10.720> about<00:04:10.870> formal 00:04:11.280 --> 00:04:11.290 align:start position:0% in so what do we like about formal 00:04:11.290 --> 00:04:13.020 align:start position:0% in so what do we like about formal verification<00:04:11.440> well<00:04:12.160> first<00:04:12.400> of<00:04:12.519> all<00:04:12.609> I<00:04:12.670> think 00:04:13.020 --> 00:04:13.030 align:start position:0% verification well first of all I think 00:04:13.030 --> 00:04:15.750 align:start position:0% verification well first of all I think specification<00:04:13.989> is<00:04:14.139> a<00:04:14.170> great<00:04:14.440> virtue<00:04:15.069> so<00:04:15.280> by 00:04:15.750 --> 00:04:15.760 align:start position:0% specification is a great virtue so by 00:04:15.760 --> 00:04:17.729 align:start position:0% specification is a great virtue so by rigorously<00:04:16.269> and<00:04:16.479> mathematically<00:04:17.139> specifying 00:04:17.729 --> 00:04:17.739 align:start position:0% rigorously and mathematically specifying 00:04:17.739 --> 00:04:19.440 align:start position:0% rigorously and mathematically specifying what<00:04:18.100> you're<00:04:18.280> building<00:04:18.639> it<00:04:19.030> helps<00:04:19.359> you 00:04:19.440 --> 00:04:19.450 align:start position:0% what you're building it helps you 00:04:19.450 --> 00:04:20.789 align:start position:0% what you're building it helps you understand<00:04:19.959> the<00:04:20.169> systems<00:04:20.530> that<00:04:20.590> you're 00:04:20.789 --> 00:04:20.799 align:start position:0% understand the systems that you're 00:04:20.799 --> 00:04:24.450 align:start position:0% understand the systems that you're making<00:04:21.150> on<00:04:22.150> a<00:04:22.210> deeper<00:04:22.690> level<00:04:22.770> also<00:04:23.770> specifying 00:04:24.450 --> 00:04:24.460 align:start position:0% making on a deeper level also specifying 00:04:24.460 --> 00:04:26.790 align:start position:0% making on a deeper level also specifying the<00:04:24.669> lower<00:04:24.820> levels<00:04:25.300> this<00:04:25.810> rigorously<00:04:26.350> things 00:04:26.790 --> 00:04:26.800 align:start position:0% the lower levels this rigorously things 00:04:26.800 --> 00:04:28.770 align:start position:0% the lower levels this rigorously things like<00:04:27.039> the<00:04:27.220> EVM<00:04:27.639> and<00:04:27.970> the<00:04:28.330> languages<00:04:28.750> that 00:04:28.770 --> 00:04:28.780 align:start position:0% like the EVM and the languages that 00:04:28.780 --> 00:04:31.620 align:start position:0% like the EVM and the languages that we're<00:04:29.050> using<00:04:29.490> helps<00:04:30.490> authors<00:04:30.789> of<00:04:31.180> higher 00:04:31.620 --> 00:04:31.630 align:start position:0% we're using helps authors of higher 00:04:31.630 --> 00:04:33.420 align:start position:0% we're using helps authors of higher level<00:04:31.960> systems<00:04:32.380> know<00:04:32.650> exactly<00:04:33.220> what 00:04:33.420 --> 00:04:33.430 align:start position:0% level systems know exactly what 00:04:33.430 --> 00:04:35.100 align:start position:0% level systems know exactly what guarantees<00:04:33.940> they<00:04:34.180> can<00:04:34.360> expect<00:04:34.720> from<00:04:34.840> these 00:04:35.100 --> 00:04:35.110 align:start position:0% guarantees they can expect from these 00:04:35.110 --> 00:04:37.589 align:start position:0% guarantees they can expect from these systems<00:04:35.560> so<00:04:36.000> specifications<00:04:37.000> are<00:04:37.120> great<00:04:37.360> and 00:04:37.589 --> 00:04:37.599 align:start position:0% systems so specifications are great and 00:04:37.599 --> 00:04:39.240 align:start position:0% systems so specifications are great and the<00:04:37.690> more<00:04:37.870> rigorous<00:04:38.080> these<00:04:38.470> specifications 00:04:39.240 --> 00:04:39.250 align:start position:0% the more rigorous these specifications 00:04:39.250 --> 00:04:41.189 align:start position:0% the more rigorous these specifications are<00:04:39.490> the<00:04:39.789> better<00:04:39.940> we<00:04:40.120> can<00:04:40.240> start<00:04:40.510> to<00:04:40.630> stat 00:04:41.189 --> 00:04:41.199 align:start position:0% are the better we can start to stat 00:04:41.199 --> 00:04:43.019 align:start position:0% are the better we can start to stat start<00:04:41.469> to<00:04:41.560> tackle<00:04:41.800> the<00:04:42.430> problem<00:04:42.759> of<00:04:42.849> writing 00:04:43.019 --> 00:04:43.029 align:start position:0% start to tackle the problem of writing 00:04:43.029 --> 00:04:45.929 align:start position:0% start to tackle the problem of writing correct<00:04:43.419> contracts<00:04:44.189> English<00:04:45.189> specifications 00:04:45.929 --> 00:04:45.939 align:start position:0% correct contracts English specifications 00:04:45.939 --> 00:04:47.519 align:start position:0% correct contracts English specifications are<00:04:46.060> pretty<00:04:46.270> common<00:04:46.599> in<00:04:46.689> the<00:04:46.779> field<00:04:46.990> these<00:04:47.469> are 00:04:47.519 --> 00:04:47.529 align:start position:0% are pretty common in the field these are 00:04:47.529 --> 00:04:49.140 align:start position:0% are pretty common in the field these are definitely<00:04:47.949> not<00:04:48.129> enough<00:04:48.370> they<00:04:48.849> admit 00:04:49.140 --> 00:04:49.150 align:start position:0% definitely not enough they admit 00:04:49.150 --> 00:04:51.179 align:start position:0% definitely not enough they admit ambiguity<00:04:49.779> you<00:04:50.289> want<00:04:50.469> an<00:04:50.529> example<00:04:50.800> of<00:04:51.039> this 00:04:51.179 --> 00:04:51.189 align:start position:0% ambiguity you want an example of this 00:04:51.189 --> 00:04:53.850 align:start position:0% ambiguity you want an example of this check<00:04:51.490> out<00:04:51.639> the<00:04:51.819> ISO<00:04:52.300> c11<00:04:52.900> standard<00:04:53.319> which<00:04:53.680> has 00:04:53.850 --> 00:04:53.860 align:start position:0% check out the ISO c11 standard which has 00:04:53.860 --> 00:04:55.290 align:start position:0% check out the ISO c11 standard which has a<00:04:53.889> whole<00:04:54.099> committee<00:04:54.430> whose<00:04:54.729> job<00:04:54.999> it<00:04:55.150> is<00:04:55.180> to 00:04:55.290 --> 00:04:55.300 align:start position:0% a whole committee whose job it is to 00:04:55.300 --> 00:04:58.499 align:start position:0% a whole committee whose job it is to argue<00:04:55.810> about<00:04:56.219> whether<00:04:57.219> certain<00:04:57.669> programs<00:04:58.270> do 00:04:58.499 --> 00:04:58.509 align:start position:0% argue about whether certain programs do 00:04:58.509 --> 00:05:01.469 align:start position:0% argue about whether certain programs do or<00:04:58.659> do<00:04:58.749> not<00:04:58.779> conform<00:04:59.349> to<00:04:59.590> the<00:04:59.770> standard<00:05:00.479> formal 00:05:01.469 --> 00:05:01.479 align:start position:0% or do not conform to the standard formal 00:05:01.479 --> 00:05:03.360 align:start position:0% or do not conform to the standard formal specifications<00:05:02.229> can<00:05:02.379> also<00:05:02.529> go<00:05:02.770> further<00:05:03.009> in 00:05:03.360 --> 00:05:03.370 align:start position:0% specifications can also go further in 00:05:03.370 --> 00:05:05.550 align:start position:0% specifications can also go further in serving<00:05:03.759> as<00:05:03.849> criterias<00:05:04.389> for<00:05:04.419> Forks<00:05:04.930> so<00:05:05.439> the 00:05:05.550 --> 00:05:05.560 align:start position:0% serving as criterias for Forks so the 00:05:05.560 --> 00:05:07.230 align:start position:0% serving as criterias for Forks so the question<00:05:05.889> of<00:05:06.009> when<00:05:06.219> to<00:05:06.400> fork<00:05:06.669> these<00:05:06.819> systems 00:05:07.230 --> 00:05:07.240 align:start position:0% question of when to fork these systems 00:05:07.240 --> 00:05:09.179 align:start position:0% question of when to fork these systems could<00:05:07.479> be<00:05:07.539> answered<00:05:07.990> by<00:05:08.650> when<00:05:09.039> the 00:05:09.179 --> 00:05:09.189 align:start position:0% could be answered by when the 00:05:09.189 --> 00:05:11.040 align:start position:0% could be answered by when the implementation<00:05:09.909> of<00:05:10.150> the<00:05:10.300> system<00:05:10.449> differs 00:05:11.040 --> 00:05:11.050 align:start position:0% implementation of the system differs 00:05:11.050 --> 00:05:13.290 align:start position:0% implementation of the system differs from<00:05:11.199> its<00:05:11.349> specification<00:05:12.159> in<00:05:12.340> which<00:05:12.879> case<00:05:13.120> you 00:05:13.290 --> 00:05:13.300 align:start position:0% from its specification in which case you 00:05:13.300 --> 00:05:15.050 align:start position:0% from its specification in which case you have<00:05:13.419> a<00:05:13.449> very<00:05:13.569> clear<00:05:13.960> bug 00:05:15.050 --> 00:05:15.060 align:start position:0% have a very clear bug 00:05:15.060 --> 00:05:17.459 align:start position:0% have a very clear bug obviously<00:05:16.060> specifications<00:05:16.960> also<00:05:17.229> give<00:05:17.379> you 00:05:17.459 --> 00:05:17.469 align:start position:0% obviously specifications also give you 00:05:17.469 --> 00:05:19.589 align:start position:0% obviously specifications also give you these<00:05:17.620> other<00:05:17.800> side<00:05:18.129> benefits<00:05:18.610> they<00:05:19.300> can<00:05:19.449> help 00:05:19.589 --> 00:05:19.599 align:start position:0% these other side benefits they can help 00:05:19.599 --> 00:05:21.329 align:start position:0% these other side benefits they can help us<00:05:19.779> find<00:05:19.990> bugs<00:05:20.319> and<00:05:20.650> they<00:05:20.889> can<00:05:21.039> help<00:05:21.159> us 00:05:21.329 --> 00:05:21.339 align:start position:0% us find bugs and they can help us 00:05:21.339 --> 00:05:23.129 align:start position:0% us find bugs and they can help us generate<00:05:21.729> tools<00:05:21.999> that<00:05:22.270> we<00:05:22.360> use<00:05:22.569> to<00:05:22.599> analyze 00:05:23.129 --> 00:05:23.139 align:start position:0% generate tools that we use to analyze 00:05:23.139 --> 00:05:25.589 align:start position:0% generate tools that we use to analyze our<00:05:23.319> contracts<00:05:23.939> all<00:05:24.939> right<00:05:25.089> so<00:05:25.210> let's<00:05:25.389> talk<00:05:25.539> a 00:05:25.589 --> 00:05:25.599 align:start position:0% our contracts all right so let's talk a 00:05:25.599 --> 00:05:26.939 align:start position:0% our contracts all right so let's talk a little<00:05:25.719> bit<00:05:25.960> about<00:05:26.080> the<00:05:26.409> work<00:05:26.589> that's<00:05:26.770> being 00:05:26.939 --> 00:05:26.949 align:start position:0% little bit about the work that's being 00:05:26.949 --> 00:05:29.730 align:start position:0% little bit about the work that's being done<00:05:27.069> here<00:05:27.879> both<00:05:28.240> of<00:05:28.389> these<00:05:28.509> slides<00:05:29.439> are<00:05:29.650> gonna 00:05:29.730 --> 00:05:29.740 align:start position:0% done here both of these slides are gonna 00:05:29.740 --> 00:05:31.140 align:start position:0% done here both of these slides are gonna have<00:05:29.949> later<00:05:30.189> talks<00:05:30.430> on<00:05:30.610> them<00:05:30.729> so<00:05:30.879> I'll<00:05:30.969> be 00:05:31.140 --> 00:05:31.150 align:start position:0% have later talks on them so I'll be 00:05:31.150 --> 00:05:32.939 align:start position:0% have later talks on them so I'll be brief<00:05:31.389> one<00:05:32.050> of<00:05:32.139> them<00:05:32.259> is<00:05:32.379> this<00:05:32.499> tool<00:05:32.740> called 00:05:32.939 --> 00:05:32.949 align:start position:0% brief one of them is this tool called 00:05:32.949 --> 00:05:34.559 align:start position:0% brief one of them is this tool called Oriente<00:05:33.520> out<00:05:33.759> of<00:05:33.879> the<00:05:33.999> university<00:05:34.479> of 00:05:34.559 --> 00:05:34.569 align:start position:0% Oriente out of the university of 00:05:34.569 --> 00:05:36.899 align:start position:0% Oriente out of the university of singapore<00:05:34.779> i<00:05:35.080> believe<00:05:35.439> and<00:05:35.770> what<00:05:36.400> they<00:05:36.430> did<00:05:36.729> is 00:05:36.899 --> 00:05:36.909 align:start position:0% singapore i believe and what they did is 00:05:36.909 --> 00:05:39.329 align:start position:0% singapore i believe and what they did is they<00:05:37.089> took<00:05:37.120> the<00:05:37.569> semantics<00:05:38.289> of<00:05:38.409> the<00:05:38.589> EVM<00:05:38.979> that 00:05:39.329 --> 00:05:39.339 align:start position:0% they took the semantics of the EVM that 00:05:39.339 --> 00:05:41.189 align:start position:0% they took the semantics of the EVM that was<00:05:39.520> very<00:05:39.759> nicely<00:05:40.029> laid<00:05:40.360> out<00:05:40.509> in<00:05:40.689> the<00:05:40.779> etherium 00:05:41.189 --> 00:05:41.199 align:start position:0% was very nicely laid out in the etherium 00:05:41.199 --> 00:05:43.110 align:start position:0% was very nicely laid out in the etherium yellow<00:05:41.710> paper<00:05:41.919> which<00:05:42.550> i<00:05:42.699> think<00:05:42.759> is<00:05:42.999> an 00:05:43.110 --> 00:05:43.120 align:start position:0% yellow paper which i think is an 00:05:43.120 --> 00:05:45.089 align:start position:0% yellow paper which i think is an excellent<00:05:43.270> document<00:05:43.779> and<00:05:44.199> a<00:05:44.620> great<00:05:44.919> way<00:05:45.069> to 00:05:45.089 --> 00:05:45.099 align:start position:0% excellent document and a great way to 00:05:45.099 --> 00:05:47.429 align:start position:0% excellent document and a great way to sort<00:05:45.399> of<00:05:45.490> set<00:05:45.729> the<00:05:45.759> standard<00:05:46.060> for<00:05:46.930> the<00:05:47.259> rigor 00:05:47.429 --> 00:05:47.439 align:start position:0% sort of set the standard for the rigor 00:05:47.439 --> 00:05:49.079 align:start position:0% sort of set the standard for the rigor that<00:05:47.529> we<00:05:47.740> expect<00:05:48.099> from<00:05:48.189> these<00:05:48.370> systems<00:05:48.819> and 00:05:49.079 --> 00:05:49.089 align:start position:0% that we expect from these systems and 00:05:49.089 --> 00:05:51.269 align:start position:0% that we expect from these systems and they<00:05:49.599> built<00:05:49.779> some<00:05:49.990> tools<00:05:50.139> on<00:05:50.409> top<00:05:50.439> of<00:05:50.649> it<00:05:50.949> to 00:05:51.269 --> 00:05:51.279 align:start position:0% they built some tools on top of it to 00:05:51.279 --> 00:05:52.769 align:start position:0% they built some tools on top of it to analyze<00:05:51.610> the<00:05:51.939> block<00:05:52.120> chain<00:05:52.389> to<00:05:52.539> try<00:05:52.719> to 00:05:52.769 --> 00:05:52.779 align:start position:0% analyze the block chain to try to 00:05:52.779 --> 00:05:55.079 align:start position:0% analyze the block chain to try to discover<00:05:53.169> bugs<00:05:53.529> in<00:05:53.889> smart<00:05:54.279> contracts<00:05:54.759> running 00:05:55.079 --> 00:05:55.089 align:start position:0% discover bugs in smart contracts running 00:05:55.089 --> 00:05:57.360 align:start position:0% discover bugs in smart contracts running in<00:05:55.180> the<00:05:55.270> wild<00:05:55.389> so<00:05:56.229> I<00:05:56.620> highly<00:05:56.889> suggest<00:05:57.039> you<00:05:57.250> read 00:05:57.360 --> 00:05:57.370 align:start position:0% in the wild so I highly suggest you read 00:05:57.370 --> 00:05:59.129 align:start position:0% in the wild so I highly suggest you read the<00:05:57.399> paper<00:05:57.639> I<00:05:57.939> love<00:05:58.300> the<00:05:58.479> work<00:05:58.629> that<00:05:58.659> this<00:05:58.899> team 00:05:59.129 --> 00:05:59.139 align:start position:0% the paper I love the work that this team 00:05:59.139 --> 00:06:01.649 align:start position:0% the paper I love the work that this team did<00:05:59.379> I<00:05:59.919> think<00:06:00.250> it's<00:06:00.370> not<00:06:00.520> perfect<00:06:01.000> I<00:06:01.180> do<00:06:01.270> think 00:06:01.649 --> 00:06:01.659 align:start position:0% did I think it's not perfect I do think 00:06:01.659 --> 00:06:03.959 align:start position:0% did I think it's not perfect I do think that<00:06:01.899> there<00:06:02.469> are<00:06:02.500> many<00:06:02.770> false<00:06:03.129> positives<00:06:03.370> that 00:06:03.959 --> 00:06:03.969 align:start position:0% that there are many false positives that 00:06:03.969 --> 00:06:05.850 align:start position:0% that there are many false positives that sort<00:06:04.210> of<00:06:04.270> come<00:06:04.539> with<00:06:04.960> their<00:06:05.110> approach<00:06:05.439> that<00:06:05.770> we 00:06:05.850 --> 00:06:05.860 align:start position:0% sort of come with their approach that we 00:06:05.860 --> 00:06:08.040 align:start position:0% sort of come with their approach that we can<00:06:06.069> further<00:06:06.789> refine<00:06:07.060> and<00:06:07.449> get<00:06:07.569> rid<00:06:07.719> of<00:06:07.750> as 00:06:08.040 --> 00:06:08.050 align:start position:0% can further refine and get rid of as 00:06:08.050 --> 00:06:10.290 align:start position:0% can further refine and get rid of as these<00:06:08.319> tools<00:06:08.560> evolve<00:06:08.919> so<00:06:09.639> if<00:06:09.909> you<00:06:10.029> want<00:06:10.210> to 00:06:10.290 --> 00:06:10.300 align:start position:0% these tools evolve so if you want to 00:06:10.300 --> 00:06:12.209 align:start position:0% these tools evolve so if you want to talk<00:06:10.810> more<00:06:11.020> about<00:06:11.080> this<00:06:11.439> work<00:06:11.680> you<00:06:11.919> can<00:06:12.069> ask 00:06:12.209 --> 00:06:12.219 align:start position:0% talk more about this work you can ask 00:06:12.219 --> 00:06:13.679 align:start position:0% talk more about this work you can ask questions<00:06:12.610> at<00:06:12.729> the<00:06:12.819> presentation<00:06:13.270> that's 00:06:13.679 --> 00:06:13.689 align:start position:0% questions at the presentation that's 00:06:13.689 --> 00:06:15.450 align:start position:0% questions at the presentation that's coming<00:06:13.990> up<00:06:14.050> later<00:06:14.289> in<00:06:14.379> the<00:06:14.469> event<00:06:14.620> or<00:06:14.949> you<00:06:15.339> can 00:06:15.450 --> 00:06:15.460 align:start position:0% coming up later in the event or you can 00:06:15.460 --> 00:06:18.269 align:start position:0% coming up later in the event or you can find<00:06:15.669> me<00:06:15.789> afterwards<00:06:16.560> all<00:06:17.560> right<00:06:17.620> here<00:06:18.159> is 00:06:18.269 --> 00:06:18.279 align:start position:0% find me afterwards all right here is 00:06:18.279 --> 00:06:20.579 align:start position:0% find me afterwards all right here is another<00:06:18.550> great<00:06:18.759> example<00:06:19.110> dr.<00:06:20.110> christian 00:06:20.579 --> 00:06:20.589 align:start position:0% another great example dr. christian 00:06:20.589 --> 00:06:22.260 align:start position:0% another great example dr. christian right<00:06:21.009> weasoner<00:06:21.399> I<00:06:21.580> hope<00:06:21.759> I<00:06:21.879> pronounced<00:06:22.180> that 00:06:22.260 --> 00:06:22.270 align:start position:0% right weasoner I hope I pronounced that 00:06:22.270 --> 00:06:26.309 align:start position:0% right weasoner I hope I pronounced that right<00:06:22.830> with<00:06:23.830> a<00:06:24.069> y3<00:06:24.909> sort<00:06:25.629> of<00:06:25.749> back-end<00:06:25.960> for 00:06:26.309 --> 00:06:26.319 align:start position:0% right with a y3 sort of back-end for 00:06:26.319 --> 00:06:29.399 align:start position:0% right with a y3 sort of back-end for formal<00:06:26.919> verification<00:06:27.159> in<00:06:27.759> solidity<00:06:28.229> so<00:06:29.229> here 00:06:29.399 --> 00:06:29.409 align:start position:0% formal verification in solidity so here 00:06:29.409 --> 00:06:31.379 align:start position:0% formal verification in solidity so here you<00:06:29.529> can<00:06:29.680> see<00:06:29.860> a<00:06:29.889> very<00:06:30.159> simple<00:06:30.430> funds<00:06:30.789> contract 00:06:31.379 --> 00:06:31.389 align:start position:0% you can see a very simple funds contract 00:06:31.389 --> 00:06:33.659 align:start position:0% you can see a very simple funds contract and<00:06:31.659> a<00:06:32.050> specification<00:06:32.469> over<00:06:33.039> this<00:06:33.189> contract 00:06:33.659 --> 00:06:33.669 align:start position:0% and a specification over this contract 00:06:33.669 --> 00:06:37.050 align:start position:0% and a specification over this contract that<00:06:33.939> was<00:06:34.569> presented<00:06:34.990> at<00:06:35.289> the<00:06:35.349> ic3<00:06:36.310> etherion 00:06:37.050 --> 00:06:37.060 align:start position:0% that was presented at the ic3 etherion 00:06:37.060 --> 00:06:40.019 align:start position:0% that was presented at the ic3 etherion boot<00:06:37.240> camp<00:06:37.449> earlier<00:06:38.099> and<00:06:39.099> this<00:06:39.580> contract 00:06:40.019 --> 00:06:40.029 align:start position:0% boot camp earlier and this contract 00:06:40.029 --> 00:06:41.279 align:start position:0% boot camp earlier and this contract allows<00:06:40.300> you<00:06:40.419> to<00:06:40.539> withdraw<00:06:40.839> a<00:06:40.870> certain<00:06:41.169> amount 00:06:41.279 --> 00:06:41.289 align:start position:0% allows you to withdraw a certain amount 00:06:41.289 --> 00:06:42.749 align:start position:0% allows you to withdraw a certain amount of<00:06:41.409> shares<00:06:41.710> and<00:06:42.069> comes<00:06:42.550> with<00:06:42.610> the 00:06:42.749 --> 00:06:42.759 align:start position:0% of shares and comes with the 00:06:42.759 --> 00:06:44.309 align:start position:0% of shares and comes with the specification<00:06:43.449> that<00:06:43.599> the<00:06:43.689> number<00:06:43.960> of<00:06:43.990> shares 00:06:44.309 --> 00:06:44.319 align:start position:0% specification that the number of shares 00:06:44.319 --> 00:06:47.719 align:start position:0% specification that the number of shares preserves<00:06:44.800> the<00:06:44.979> balance<00:06:45.310> of<00:06:45.539> the<00:06:46.539> contract 00:06:47.719 --> 00:06:47.729 align:start position:0% preserves the balance of the contract 00:06:47.729 --> 00:06:51.559 align:start position:0% preserves the balance of the contract so<00:06:48.729> that<00:06:49.599> was<00:06:49.750> the<00:06:49.870> wrong<00:06:49.959> direction 00:06:51.559 --> 00:06:51.569 align:start position:0% so that was the wrong direction 00:06:51.569 --> 00:06:54.119 align:start position:0% so that was the wrong direction so<00:06:52.569> here's<00:06:53.199> another<00:06:53.409> contract<00:06:53.979> that 00:06:54.119 --> 00:06:54.129 align:start position:0% so here's another contract that 00:06:54.129 --> 00:06:57.089 align:start position:0% so here's another contract that satisfies<00:06:54.610> this<00:06:54.819> specification<00:06:55.269> and<00:06:56.099> this 00:06:57.089 --> 00:06:57.099 align:start position:0% satisfies this specification and this 00:06:57.099 --> 00:06:58.769 align:start position:0% satisfies this specification and this sort<00:06:57.339> of<00:06:57.399> helps<00:06:57.669> us<00:06:57.759> illustrate<00:06:57.940> that<00:06:58.389> writing 00:06:58.769 --> 00:06:58.779 align:start position:0% sort of helps us illustrate that writing 00:06:58.779 --> 00:07:00.300 align:start position:0% sort of helps us illustrate that writing complete<00:06:59.050> specifications<00:06:59.860> is<00:07:00.039> pretty 00:07:00.300 --> 00:07:00.310 align:start position:0% complete specifications is pretty 00:07:00.310 --> 00:07:01.860 align:start position:0% complete specifications is pretty difficult<00:07:00.490> so<00:07:01.240> if<00:07:01.389> you're<00:07:01.539> a<00:07:01.569> trained 00:07:01.860 --> 00:07:01.870 align:start position:0% difficult so if you're a trained 00:07:01.870 --> 00:07:03.240 align:start position:0% difficult so if you're a trained developer<00:07:02.319> you're<00:07:02.500> sitting<00:07:02.769> here<00:07:02.860> looking<00:07:03.039> at 00:07:03.240 --> 00:07:03.250 align:start position:0% developer you're sitting here looking at 00:07:03.250 --> 00:07:05.159 align:start position:0% developer you're sitting here looking at a<00:07:03.310> set<00:07:03.519> of<00:07:03.639> specifications<00:07:03.990> just<00:07:04.990> like 00:07:05.159 --> 00:07:05.169 align:start position:0% a set of specifications just like 00:07:05.169 --> 00:07:06.480 align:start position:0% a set of specifications just like writing<00:07:05.469> buggy<00:07:05.800> code<00:07:06.039> there<00:07:06.279> could<00:07:06.459> be 00:07:06.480 --> 00:07:06.490 align:start position:0% writing buggy code there could be 00:07:06.490 --> 00:07:08.369 align:start position:0% writing buggy code there could be something<00:07:06.940> that<00:07:07.060> you<00:07:07.180> miss<00:07:07.389> now<00:07:07.959> this<00:07:08.139> is<00:07:08.259> not 00:07:08.369 --> 00:07:08.379 align:start position:0% something that you miss now this is not 00:07:08.379 --> 00:07:10.529 align:start position:0% something that you miss now this is not intended<00:07:08.740> to<00:07:08.919> say<00:07:09.190> that<00:07:09.550> that<00:07:09.909> this<00:07:10.089> work<00:07:10.330> was 00:07:10.529 --> 00:07:10.539 align:start position:0% intended to say that that this work was 00:07:10.539 --> 00:07:11.969 align:start position:0% intended to say that that this work was intended<00:07:11.050> to<00:07:11.139> catch<00:07:11.289> these<00:07:11.529> sort<00:07:11.740> of<00:07:11.800> cases 00:07:11.969 --> 00:07:11.979 align:start position:0% intended to catch these sort of cases 00:07:11.979 --> 00:07:14.879 align:start position:0% intended to catch these sort of cases this<00:07:12.759> is<00:07:12.879> obviously<00:07:13.209> a<00:07:13.269> trivial<00:07:13.659> example<00:07:13.889> but 00:07:14.879 --> 00:07:14.889 align:start position:0% this is obviously a trivial example but 00:07:14.889 --> 00:07:16.649 align:start position:0% this is obviously a trivial example but the<00:07:14.949> general<00:07:15.310> point<00:07:15.519> is<00:07:15.789> anywhere<00:07:16.389> you<00:07:16.539> look 00:07:16.649 --> 00:07:16.659 align:start position:0% the general point is anywhere you look 00:07:16.659 --> 00:07:19.409 align:start position:0% the general point is anywhere you look in<00:07:16.810> the<00:07:16.899> formal<00:07:17.169> verification<00:07:17.349> space<00:07:18.419> writing 00:07:19.409 --> 00:07:19.419 align:start position:0% in the formal verification space writing 00:07:19.419 --> 00:07:20.969 align:start position:0% in the formal verification space writing these<00:07:19.539> specifications<00:07:20.319> is<00:07:20.469> extremely 00:07:20.969 --> 00:07:20.979 align:start position:0% these specifications is extremely 00:07:20.979 --> 00:07:22.550 align:start position:0% these specifications is extremely difficult 00:07:22.550 --> 00:07:22.560 align:start position:0% difficult 00:07:22.560 --> 00:07:26.219 align:start position:0% difficult so<00:07:23.560> the<00:07:24.310> gaps<00:07:24.519> in<00:07:24.879> this<00:07:25.029> work<00:07:25.240> specification 00:07:26.219 --> 00:07:26.229 align:start position:0% so the gaps in this work specification 00:07:26.229 --> 00:07:27.719 align:start position:0% so the gaps in this work specification is<00:07:26.349> hard<00:07:26.560> some<00:07:26.979> properties<00:07:27.399> can't<00:07:27.639> be 00:07:27.719 --> 00:07:27.729 align:start position:0% is hard some properties can't be 00:07:27.729 --> 00:07:29.279 align:start position:0% is hard some properties can't be specified<00:07:28.180> at<00:07:28.300> all<00:07:28.419> I'm<00:07:28.659> thinking 00:07:29.279 --> 00:07:29.289 align:start position:0% specified at all I'm thinking 00:07:29.289 --> 00:07:30.570 align:start position:0% specified at all I'm thinking specifically<00:07:29.800> about<00:07:30.069> properties<00:07:30.550> of 00:07:30.570 --> 00:07:30.580 align:start position:0% specifically about properties of 00:07:30.580 --> 00:07:32.429 align:start position:0% specifically about properties of incentives<00:07:31.180> game<00:07:31.479> theoretical<00:07:31.779> properties 00:07:32.429 --> 00:07:32.439 align:start position:0% incentives game theoretical properties 00:07:32.439 --> 00:07:34.259 align:start position:0% incentives game theoretical properties and<00:07:32.769> higher-level<00:07:33.219> properties<00:07:33.909> of<00:07:34.060> smart 00:07:34.259 --> 00:07:34.269 align:start position:0% and higher-level properties of smart 00:07:34.269 --> 00:07:35.730 align:start position:0% and higher-level properties of smart contracts<00:07:34.719> that<00:07:35.289> are<00:07:35.439> pretty<00:07:35.589> much 00:07:35.730 --> 00:07:35.740 align:start position:0% contracts that are pretty much 00:07:35.740 --> 00:07:38.429 align:start position:0% contracts that are pretty much impossible<00:07:36.039> to<00:07:36.339> specify<00:07:37.229> often<00:07:38.229> when<00:07:38.349> you 00:07:38.429 --> 00:07:38.439 align:start position:0% impossible to specify often when you 00:07:38.439 --> 00:07:39.569 align:start position:0% impossible to specify often when you have<00:07:38.589> a<00:07:38.620> proof<00:07:38.889> of<00:07:39.009> these<00:07:39.099> kinds<00:07:39.459> of<00:07:39.519> things 00:07:39.569 --> 00:07:39.579 align:start position:0% have a proof of these kinds of things 00:07:39.579 --> 00:07:40.980 align:start position:0% have a proof of these kinds of things you<00:07:39.849> are<00:07:40.089> trusting<00:07:40.569> the<00:07:40.659> tools<00:07:40.870> that 00:07:40.980 --> 00:07:40.990 align:start position:0% you are trusting the tools that 00:07:40.990 --> 00:07:42.389 align:start position:0% you are trusting the tools that outputted<00:07:41.529> the<00:07:41.620> proof<00:07:41.800> which<00:07:42.009> is<00:07:42.039> not<00:07:42.279> an 00:07:42.389 --> 00:07:42.399 align:start position:0% outputted the proof which is not an 00:07:42.399 --> 00:07:44.459 align:start position:0% outputted the proof which is not an ideal<00:07:42.519> situation<00:07:42.959> because<00:07:43.959> these<00:07:44.079> tools<00:07:44.319> are 00:07:44.459 --> 00:07:44.469 align:start position:0% ideal situation because these tools are 00:07:44.469 --> 00:07:45.809 align:start position:0% ideal situation because these tools are very<00:07:44.620> hard<00:07:44.889> to<00:07:44.919> audit<00:07:45.310> and<00:07:45.430> they<00:07:45.490> require 00:07:45.809 --> 00:07:45.819 align:start position:0% very hard to audit and they require 00:07:45.819 --> 00:07:47.639 align:start position:0% very hard to audit and they require significant<00:07:46.449> expertise<00:07:46.930> we<00:07:47.379> don't<00:07:47.529> even 00:07:47.639 --> 00:07:47.649 align:start position:0% significant expertise we don't even 00:07:47.649 --> 00:07:49.110 align:start position:0% significant expertise we don't even really<00:07:47.860> know<00:07:48.009> how<00:07:48.159> to<00:07:48.189> audit<00:07:48.399> them<00:07:48.639> in<00:07:48.759> general 00:07:49.110 --> 00:07:49.120 align:start position:0% really know how to audit them in general 00:07:49.120 --> 00:07:51.389 align:start position:0% really know how to audit them in general a<00:07:49.300> key<00:07:50.199> takeaway<00:07:50.349> I'd<00:07:50.709> like<00:07:50.860> you<00:07:50.979> to<00:07:51.069> get<00:07:51.189> from 00:07:51.389 --> 00:07:51.399 align:start position:0% a key takeaway I'd like you to get from 00:07:51.399 --> 00:07:53.219 align:start position:0% a key takeaway I'd like you to get from this<00:07:51.519> is<00:07:51.699> that<00:07:51.849> any<00:07:52.000> good<00:07:52.209> tool<00:07:52.419> must<00:07:52.719> use<00:07:52.930> some 00:07:53.219 --> 00:07:53.229 align:start position:0% this is that any good tool must use some 00:07:53.229 --> 00:07:55.050 align:start position:0% this is that any good tool must use some sort<00:07:53.469> of<00:07:53.529> semantics<00:07:54.069> that<00:07:54.310> is<00:07:54.430> a<00:07:54.459> definition 00:07:55.050 --> 00:07:55.060 align:start position:0% sort of semantics that is a definition 00:07:55.060 --> 00:07:58.409 align:start position:0% sort of semantics that is a definition of<00:07:55.409> of<00:07:56.409> the<00:07:56.889> lower<00:07:57.159> levels<00:07:57.610> of<00:07:57.879> the<00:07:58.029> language 00:07:58.409 --> 00:07:58.419 align:start position:0% of of the lower levels of the language 00:07:58.419 --> 00:07:59.759 align:start position:0% of of the lower levels of the language and<00:07:58.689> the<00:07:58.870> infrastructure<00:07:59.319> on<00:07:59.439> which<00:07:59.500> they 00:07:59.759 --> 00:07:59.769 align:start position:0% and the infrastructure on which they 00:07:59.769 --> 00:08:01.259 align:start position:0% and the infrastructure on which they operate<00:08:00.189> so<00:08:00.699> when<00:08:00.849> you're<00:08:00.969> trying<00:08:01.149> to 00:08:01.259 --> 00:08:01.269 align:start position:0% operate so when you're trying to 00:08:01.269 --> 00:08:03.300 align:start position:0% operate so when you're trying to evaluate<00:08:01.449> one<00:08:02.079> of<00:08:02.110> these<00:08:02.289> tools<00:08:02.529> ask<00:08:02.829> yourself 00:08:03.300 --> 00:08:03.310 align:start position:0% evaluate one of these tools ask yourself 00:08:03.310 --> 00:08:05.309 align:start position:0% evaluate one of these tools ask yourself what<00:08:03.519> semantics<00:08:04.000> are<00:08:04.089> they<00:08:04.209> using<00:08:04.599> how<00:08:04.990> is<00:08:05.199> it 00:08:05.309 --> 00:08:05.319 align:start position:0% what semantics are they using how is it 00:08:05.319 --> 00:08:06.959 align:start position:0% what semantics are they using how is it audited<00:08:05.680> and<00:08:05.860> what<00:08:06.039> guarantees<00:08:06.459> do<00:08:06.699> we<00:08:06.789> have 00:08:06.959 --> 00:08:06.969 align:start position:0% audited and what guarantees do we have 00:08:06.969 --> 00:08:08.699 align:start position:0% audited and what guarantees do we have that<00:08:07.149> that<00:08:07.300> system<00:08:07.629> will<00:08:07.930> actually<00:08:08.079> conform 00:08:08.699 --> 00:08:08.709 align:start position:0% that that system will actually conform 00:08:08.709 --> 00:08:11.429 align:start position:0% that that system will actually conform to<00:08:08.829> those<00:08:08.949> semantics<00:08:09.719> right<00:08:10.719> now<00:08:10.899> to<00:08:10.959> really 00:08:11.429 --> 00:08:11.439 align:start position:0% to those semantics right now to really 00:08:11.439 --> 00:08:13.170 align:start position:0% to those semantics right now to really formally<00:08:11.769> verify<00:08:12.099> complex<00:08:12.550> systems<00:08:12.909> we<00:08:13.029> need 00:08:13.170 --> 00:08:13.180 align:start position:0% formally verify complex systems we need 00:08:13.180 --> 00:08:15.029 align:start position:0% formally verify complex systems we need experts<00:08:13.419> we<00:08:13.750> need<00:08:13.870> multiple<00:08:14.019> PhDs<00:08:14.709> it's<00:08:14.860> not 00:08:15.029 --> 00:08:15.039 align:start position:0% experts we need multiple PhDs it's not 00:08:15.039 --> 00:08:17.519 align:start position:0% experts we need multiple PhDs it's not an<00:08:15.189> easy<00:08:15.339> problem<00:08:15.779> and<00:08:16.779> there<00:08:16.930> are<00:08:16.959> also<00:08:17.169> some 00:08:17.519 --> 00:08:17.529 align:start position:0% an easy problem and there are also some 00:08:17.529 --> 00:08:19.409 align:start position:0% an easy problem and there are also some famous<00:08:17.949> incompleteness<00:08:18.579> &<00:08:18.879> undecidability 00:08:19.409 --> 00:08:19.419 align:start position:0% famous incompleteness & undecidability 00:08:19.419 --> 00:08:22.379 align:start position:0% famous incompleteness & undecidability results<00:08:20.019> that<00:08:20.169> may<00:08:20.439> suggest<00:08:20.709> that<00:08:21.699> gaps<00:08:22.180> in 00:08:22.379 --> 00:08:22.389 align:start position:0% results that may suggest that gaps in 00:08:22.389 --> 00:08:25.170 align:start position:0% results that may suggest that gaps in these<00:08:22.539> logics<00:08:23.039> could<00:08:24.039> require<00:08:24.399> more<00:08:24.729> work<00:08:24.909> to 00:08:25.170 --> 00:08:25.180 align:start position:0% these logics could require more work to 00:08:25.180 --> 00:08:27.869 align:start position:0% these logics could require more work to achieve<00:08:25.269> a<00:08:25.449> robust<00:08:25.870> system<00:08:26.219> all<00:08:27.219> right<00:08:27.399> so 00:08:27.869 --> 00:08:27.879 align:start position:0% achieve a robust system all right so 00:08:27.879 --> 00:08:29.699 align:start position:0% achieve a robust system all right so escape<00:08:28.449> hatches 00:08:29.699 --> 00:08:29.709 align:start position:0% escape hatches 00:08:29.709 --> 00:08:31.829 align:start position:0% escape hatches this<00:08:29.979> comes<00:08:30.219> out<00:08:30.339> of<00:08:30.490> the<00:08:30.610> need<00:08:30.789> of<00:08:30.819> not<00:08:31.599> always 00:08:31.829 --> 00:08:31.839 align:start position:0% this comes out of the need of not always 00:08:31.839 --> 00:08:34.259 align:start position:0% this comes out of the need of not always being<00:08:32.169> able<00:08:32.349> to<00:08:32.469> verify<00:08:32.709> our<00:08:32.979> contracts<00:08:33.610> so 00:08:34.259 --> 00:08:34.269 align:start position:0% being able to verify our contracts so 00:08:34.269 --> 00:08:35.399 align:start position:0% being able to verify our contracts so what<00:08:34.390> we<00:08:34.479> need<00:08:34.630> here<00:08:34.839> is<00:08:34.899> something<00:08:35.319> they 00:08:35.399 --> 00:08:35.409 align:start position:0% what we need here is something they 00:08:35.409 --> 00:08:36.870 align:start position:0% what we need here is something they figured<00:08:35.709> out<00:08:35.800> very<00:08:35.829> early<00:08:36.399> on<00:08:36.430> in<00:08:36.699> safety 00:08:36.870 --> 00:08:36.880 align:start position:0% figured out very early on in safety 00:08:36.880 --> 00:08:38.610 align:start position:0% figured out very early on in safety critical<00:08:37.149> systems<00:08:37.510> which<00:08:37.930> is<00:08:38.050> we<00:08:38.169> need<00:08:38.289> to<00:08:38.439> put 00:08:38.610 --> 00:08:38.620 align:start position:0% critical systems which is we need to put 00:08:38.620 --> 00:08:40.759 align:start position:0% critical systems which is we need to put a<00:08:38.649> human<00:08:38.919> in<00:08:39.189> the<00:08:39.310> loop<00:08:39.339> at<00:08:39.729> some<00:08:39.969> point 00:08:40.759 --> 00:08:40.769 align:start position:0% a human in the loop at some point 00:08:40.769 --> 00:08:42.839 align:start position:0% a human in the loop at some point it's<00:08:41.769> true<00:08:42.010> that<00:08:42.189> the<00:08:42.279> promise<00:08:42.610> of<00:08:42.729> these 00:08:42.839 --> 00:08:42.849 align:start position:0% it's true that the promise of these 00:08:42.849 --> 00:08:44.939 align:start position:0% it's true that the promise of these systems<00:08:43.269> involves<00:08:43.750> in<00:08:44.019> many<00:08:44.290> cases<00:08:44.649> taking 00:08:44.939 --> 00:08:44.949 align:start position:0% systems involves in many cases taking 00:08:44.949 --> 00:08:46.199 align:start position:0% systems involves in many cases taking the<00:08:45.010> humans<00:08:45.279> out<00:08:45.399> of<00:08:45.459> the<00:08:45.610> loop<00:08:45.760> and<00:08:45.910> I<00:08:46.000> think 00:08:46.199 --> 00:08:46.209 align:start position:0% the humans out of the loop and I think 00:08:46.209 --> 00:08:48.600 align:start position:0% the humans out of the loop and I think in<00:08:46.300> many<00:08:46.480> cases<00:08:46.569> that<00:08:47.050> can<00:08:47.230> be<00:08:47.380> achieved<00:08:47.610> but 00:08:48.600 --> 00:08:48.610 align:start position:0% in many cases that can be achieved but 00:08:48.610 --> 00:08:50.460 align:start position:0% in many cases that can be achieved but we<00:08:48.730> shouldn't<00:08:48.970> necessarily<00:08:49.240> take<00:08:49.899> that<00:08:50.110> as<00:08:50.290> an 00:08:50.460 --> 00:08:50.470 align:start position:0% we shouldn't necessarily take that as an 00:08:50.470 --> 00:08:53.250 align:start position:0% we shouldn't necessarily take that as an absolute<00:08:50.829> if<00:08:51.819> verification<00:08:52.600> or<00:08:52.720> bounties<00:08:53.110> or 00:08:53.250 --> 00:08:53.260 align:start position:0% absolute if verification or bounties or 00:08:53.260 --> 00:08:54.600 align:start position:0% absolute if verification or bounties or the<00:08:53.350> other<00:08:53.500> two<00:08:53.680> prongs<00:08:53.920> of<00:08:54.100> the<00:08:54.189> approaches 00:08:54.600 --> 00:08:54.610 align:start position:0% the other two prongs of the approaches 00:08:54.610 --> 00:08:56.280 align:start position:0% the other two prongs of the approaches fail<00:08:54.819> it's<00:08:55.089> important<00:08:55.569> to<00:08:55.630> have<00:08:55.779> some<00:08:56.019> sort<00:08:56.230> of 00:08:56.280 --> 00:08:56.290 align:start position:0% fail it's important to have some sort of 00:08:56.290 --> 00:08:58.799 align:start position:0% fail it's important to have some sort of failsafe<00:08:56.529> or<00:08:56.949> backup<00:08:57.250> mechanism<00:08:57.689> there<00:08:58.689> are<00:08:58.750> a 00:08:58.799 --> 00:08:58.809 align:start position:0% failsafe or backup mechanism there are a 00:08:58.809 --> 00:09:00.929 align:start position:0% failsafe or backup mechanism there are a lot<00:08:58.929> of<00:08:58.959> parallels<00:08:59.589> to<00:08:59.829> legacy<00:09:00.279> contract<00:09:00.730> law 00:09:00.929 --> 00:09:00.939 align:start position:0% lot of parallels to legacy contract law 00:09:00.939 --> 00:09:02.490 align:start position:0% lot of parallels to legacy contract law here<00:09:01.209> so<00:09:01.420> there<00:09:01.569> are<00:09:01.630> a<00:09:01.660> lot<00:09:01.689> of<00:09:01.870> lessons<00:09:02.079> to<00:09:02.380> be 00:09:02.490 --> 00:09:02.500 align:start position:0% here so there are a lot of lessons to be 00:09:02.500 --> 00:09:04.110 align:start position:0% here so there are a lot of lessons to be learned<00:09:02.740> from<00:09:02.890> how<00:09:03.220> people<00:09:03.670> have<00:09:03.819> done<00:09:03.970> this 00:09:04.110 --> 00:09:04.120 align:start position:0% learned from how people have done this 00:09:04.120 --> 00:09:06.030 align:start position:0% learned from how people have done this previously<00:09:04.540> in<00:09:04.630> contracts<00:09:05.649> and<00:09:05.709> also 00:09:06.030 --> 00:09:06.040 align:start position:0% previously in contracts and also 00:09:06.040 --> 00:09:08.369 align:start position:0% previously in contracts and also parallels<00:09:06.459> to<00:09:06.550> safety<00:09:06.939> critical<00:09:07.089> systems<00:09:07.420> so 00:09:08.369 --> 00:09:08.379 align:start position:0% parallels to safety critical systems so 00:09:08.379 --> 00:09:09.509 align:start position:0% parallels to safety critical systems so I'll<00:09:08.559> pose<00:09:08.769> the<00:09:08.920> question<00:09:09.189> to<00:09:09.309> the<00:09:09.399> audience 00:09:09.509 --> 00:09:09.519 align:start position:0% I'll pose the question to the audience 00:09:09.519 --> 00:09:11.519 align:start position:0% I'll pose the question to the audience would<00:09:10.029> you<00:09:10.149> write<00:09:10.329> a<00:09:10.660> nuclear<00:09:11.230> power<00:09:11.439> plant 00:09:11.519 --> 00:09:11.529 align:start position:0% would you write a nuclear power plant 00:09:11.529 --> 00:09:13.710 align:start position:0% would you write a nuclear power plant software<00:09:12.279> that<00:09:12.639> has<00:09:12.819> no<00:09:13.029> kill<00:09:13.240> switch<00:09:13.449> in<00:09:13.600> it 00:09:13.710 --> 00:09:13.720 align:start position:0% software that has no kill switch in it 00:09:13.720 --> 00:09:16.799 align:start position:0% software that has no kill switch in it probably<00:09:14.619> not<00:09:15.009> and<00:09:15.309> I<00:09:15.759> wouldn't<00:09:16.029> want<00:09:16.240> a<00:09:16.449> multi 00:09:16.799 --> 00:09:16.809 align:start position:0% probably not and I wouldn't want a multi 00:09:16.809 --> 00:09:18.329 align:start position:0% probably not and I wouldn't want a multi hundred<00:09:16.930> million<00:09:17.319> dollar<00:09:17.499> contract<00:09:18.069> not<00:09:18.189> to 00:09:18.329 --> 00:09:18.339 align:start position:0% hundred million dollar contract not to 00:09:18.339 --> 00:09:20.549 align:start position:0% hundred million dollar contract not to have<00:09:18.490> one<00:09:18.639> either<00:09:18.759> so<00:09:19.089> we've<00:09:19.959> been<00:09:20.139> doing<00:09:20.319> some 00:09:20.549 --> 00:09:20.559 align:start position:0% have one either so we've been doing some 00:09:20.559 --> 00:09:22.470 align:start position:0% have one either so we've been doing some work<00:09:20.680> on<00:09:20.800> this<00:09:20.980> and<00:09:21.129> I<00:09:21.189> see<00:09:21.369> three<00:09:21.670> by<00:09:22.240> Bill 00:09:22.470 --> 00:09:22.480 align:start position:0% work on this and I see three by Bill 00:09:22.480 --> 00:09:24.119 align:start position:0% work on this and I see three by Bill merino<00:09:22.839> here<00:09:23.110> I<00:09:23.290> highly<00:09:23.529> suggest<00:09:23.679> you<00:09:23.980> read 00:09:24.119 --> 00:09:24.129 align:start position:0% merino here I highly suggest you read 00:09:24.129 --> 00:09:25.919 align:start position:0% merino here I highly suggest you read the<00:09:24.220> paper<00:09:24.429> for<00:09:24.850> more<00:09:24.999> information<00:09:25.540> since<00:09:25.869> I 00:09:25.919 --> 00:09:25.929 align:start position:0% the paper for more information since I 00:09:25.929 --> 00:09:28.049 align:start position:0% the paper for more information since I don't<00:09:26.110> have<00:09:26.230> much<00:09:26.439> time<00:09:26.649> to<00:09:26.709> discuss<00:09:27.160> it 00:09:28.049 --> 00:09:28.059 align:start position:0% don't have much time to discuss it 00:09:28.059 --> 00:09:30.929 align:start position:0% don't have much time to discuss it and<00:09:28.269> what<00:09:28.420> we<00:09:28.509> did<00:09:28.689> here<00:09:28.990> bill<00:09:29.639> was<00:09:30.639> a<00:09:30.670> lawyer 00:09:30.929 --> 00:09:30.939 align:start position:0% and what we did here bill was a lawyer 00:09:30.939 --> 00:09:32.489 align:start position:0% and what we did here bill was a lawyer by<00:09:31.149> trade<00:09:31.449> and<00:09:31.660> got<00:09:31.779> a<00:09:31.809> master's<00:09:32.199> in<00:09:32.230> computer 00:09:32.489 --> 00:09:32.499 align:start position:0% by trade and got a master's in computer 00:09:32.499 --> 00:09:34.499 align:start position:0% by trade and got a master's in computer science<00:09:32.829> and<00:09:33.220> he<00:09:33.639> looked<00:09:33.850> at<00:09:33.999> parallels 00:09:34.499 --> 00:09:34.509 align:start position:0% science and he looked at parallels 00:09:34.509 --> 00:09:36.929 align:start position:0% science and he looked at parallels between<00:09:34.689> smart<00:09:35.139> contracts<00:09:35.709> and<00:09:36.009> legacy 00:09:36.929 --> 00:09:36.939 align:start position:0% between smart contracts and legacy 00:09:36.939 --> 00:09:38.879 align:start position:0% between smart contracts and legacy contract<00:09:37.420> laws<00:09:37.629> so<00:09:38.350> he<00:09:38.470> looked<00:09:38.649> at<00:09:38.709> all<00:09:38.860> of 00:09:38.879 --> 00:09:38.889 align:start position:0% contract laws so he looked at all of 00:09:38.889 --> 00:09:40.679 align:start position:0% contract laws so he looked at all of these<00:09:39.100> concepts<00:09:39.610> of<00:09:39.759> termination<00:09:40.149> rescission 00:09:40.679 --> 00:09:40.689 align:start position:0% these concepts of termination rescission 00:09:40.689 --> 00:09:42.749 align:start position:0% these concepts of termination rescission and<00:09:40.779> modification<00:09:41.529> that<00:09:42.040> are<00:09:42.189> codified<00:09:42.610> in 00:09:42.749 --> 00:09:42.759 align:start position:0% and modification that are codified in 00:09:42.759 --> 00:09:44.309 align:start position:0% and modification that are codified in the<00:09:42.790> law<00:09:42.970> that<00:09:43.269> have<00:09:43.389> been<00:09:43.569> designed<00:09:43.720> to<00:09:44.050> solve 00:09:44.309 --> 00:09:44.319 align:start position:0% the law that have been designed to solve 00:09:44.319 --> 00:09:46.230 align:start position:0% the law that have been designed to solve problems<00:09:44.889> that<00:09:45.009> have<00:09:45.189> come<00:09:45.399> up<00:09:45.429> in<00:09:45.699> historical 00:09:46.230 --> 00:09:46.240 align:start position:0% problems that have come up in historical 00:09:46.240 --> 00:09:48.540 align:start position:0% problems that have come up in historical precedents<00:09:46.779> and<00:09:47.019> he<00:09:47.529> wrote<00:09:47.709> little<00:09:48.069> etherium 00:09:48.540 --> 00:09:48.550 align:start position:0% precedents and he wrote little etherium 00:09:48.550 --> 00:09:51.030 align:start position:0% precedents and he wrote little etherium libraries<00:09:49.290> sort<00:09:50.290> of<00:09:50.379> mirroring<00:09:50.769> these 00:09:51.030 --> 00:09:51.040 align:start position:0% libraries sort of mirroring these 00:09:51.040 --> 00:09:53.489 align:start position:0% libraries sort of mirroring these concepts<00:09:51.639> in<00:09:51.790> traditional<00:09:52.179> contract<00:09:52.600> law<00:09:52.839> so 00:09:53.489 --> 00:09:53.499 align:start position:0% concepts in traditional contract law so 00:09:53.499 --> 00:09:55.049 align:start position:0% concepts in traditional contract law so if<00:09:53.829> you're<00:09:54.009> writing<00:09:54.160> a<00:09:54.279> high-volume<00:09:54.639> smart 00:09:55.049 --> 00:09:55.059 align:start position:0% if you're writing a high-volume smart 00:09:55.059 --> 00:09:56.400 align:start position:0% if you're writing a high-volume smart contract<00:09:55.480> I<00:09:55.600> highly<00:09:55.779> suggest<00:09:55.959> you<00:09:56.199> take<00:09:56.350> a 00:09:56.400 --> 00:09:56.410 align:start position:0% contract I highly suggest you take a 00:09:56.410 --> 00:09:59.340 align:start position:0% contract I highly suggest you take a look<00:09:56.999> so<00:09:57.999> this<00:09:58.179> is<00:09:58.329> again<00:09:58.540> not<00:09:58.720> problem-free 00:09:59.340 --> 00:09:59.350 align:start position:0% look so this is again not problem-free 00:09:59.350 --> 00:10:00.780 align:start position:0% look so this is again not problem-free we've<00:09:59.769> got<00:09:59.949> a<00:09:59.980> bunch<00:10:00.189> of<00:10:00.279> gaps<00:10:00.519> in<00:10:00.699> this 00:10:00.780 --> 00:10:00.790 align:start position:0% we've got a bunch of gaps in this 00:10:00.790 --> 00:10:02.730 align:start position:0% we've got a bunch of gaps in this approach<00:10:01.119> how<00:10:01.839> do<00:10:01.899> we<00:10:02.050> verify<00:10:02.230> that<00:10:02.470> the 00:10:02.730 --> 00:10:02.740 align:start position:0% approach how do we verify that the 00:10:02.740 --> 00:10:04.889 align:start position:0% approach how do we verify that the escape<00:10:02.889> hatch<00:10:03.189> code<00:10:03.519> is<00:10:03.699> correct<00:10:03.910> what<00:10:04.660> layer 00:10:04.889 --> 00:10:04.899 align:start position:0% escape hatch code is correct what layer 00:10:04.899 --> 00:10:06.929 align:start position:0% escape hatch code is correct what layer do<00:10:05.199> we<00:10:05.290> put<00:10:05.470> the<00:10:05.589> escape<00:10:05.889> hatches<00:10:06.100> in<00:10:06.399> do<00:10:06.850> we 00:10:06.929 --> 00:10:06.939 align:start position:0% do we put the escape hatches in do we 00:10:06.939 --> 00:10:08.790 align:start position:0% do we put the escape hatches in do we want<00:10:07.179> escape<00:10:07.480> hatches<00:10:07.660> in<00:10:07.899> the<00:10:07.990> EVM<00:10:08.350> which 00:10:08.790 --> 00:10:08.800 align:start position:0% want escape hatches in the EVM which 00:10:08.800 --> 00:10:11.220 align:start position:0% want escape hatches in the EVM which would<00:10:09.069> inherently<00:10:09.970> be<00:10:10.269> sort<00:10:10.480> of<00:10:10.540> less<00:10:10.779> general 00:10:11.220 --> 00:10:11.230 align:start position:0% would inherently be sort of less general 00:10:11.230 --> 00:10:12.689 align:start position:0% would inherently be sort of less general since<00:10:11.740> you'd<00:10:11.860> have<00:10:12.009> a<00:10:12.040> specific<00:10:12.519> set<00:10:12.670> of 00:10:12.689 --> 00:10:12.699 align:start position:0% since you'd have a specific set of 00:10:12.699 --> 00:10:14.759 align:start position:0% since you'd have a specific set of hatches<00:10:13.179> or<00:10:13.480> do<00:10:14.050> we<00:10:14.139> want<00:10:14.290> to<00:10:14.350> put<00:10:14.470> them<00:10:14.589> in<00:10:14.679> the 00:10:14.759 --> 00:10:14.769 align:start position:0% hatches or do we want to put them in the 00:10:14.769 --> 00:10:16.199 align:start position:0% hatches or do we want to put them in the compiler<00:10:15.220> which<00:10:15.429> lets<00:10:15.639> us<00:10:15.759> save<00:10:15.970> some 00:10:16.199 --> 00:10:16.209 align:start position:0% compiler which lets us save some 00:10:16.209 --> 00:10:17.910 align:start position:0% compiler which lets us save some generality<00:10:16.839> by<00:10:16.959> deferring<00:10:17.290> the<00:10:17.499> problem<00:10:17.800> to 00:10:17.910 --> 00:10:17.920 align:start position:0% generality by deferring the problem to 00:10:17.920 --> 00:10:19.829 align:start position:0% generality by deferring the problem to the<00:10:17.949> language<00:10:18.370> or<00:10:18.879> do<00:10:19.209> we<00:10:19.300> want<00:10:19.480> to<00:10:19.509> just<00:10:19.689> say 00:10:19.829 --> 00:10:19.839 align:start position:0% the language or do we want to just say 00:10:19.839 --> 00:10:22.110 align:start position:0% the language or do we want to just say contracts<00:10:20.529> use<00:10:20.860> well<00:10:21.160> audited<00:10:21.519> libraries<00:10:21.970> of 00:10:22.110 --> 00:10:22.120 align:start position:0% contracts use well audited libraries of 00:10:22.120 --> 00:10:24.449 align:start position:0% contracts use well audited libraries of escape<00:10:22.389> hatches<00:10:22.629> that<00:10:23.170> you<00:10:23.740> can<00:10:23.889> modify<00:10:24.189> as 00:10:24.449 --> 00:10:24.459 align:start position:0% escape hatches that you can modify as 00:10:24.459 --> 00:10:26.040 align:start position:0% escape hatches that you can modify as you<00:10:24.579> see<00:10:24.759> fit<00:10:24.970> giving<00:10:25.389> us<00:10:25.509> that<00:10:25.749> full 00:10:26.040 --> 00:10:26.050 align:start position:0% you see fit giving us that full 00:10:26.050 --> 00:10:28.799 align:start position:0% you see fit giving us that full generality<00:10:26.379> so<00:10:27.389> it's<00:10:28.389> an<00:10:28.480> open<00:10:28.720> question 00:10:28.799 --> 00:10:28.809 align:start position:0% generality so it's an open question 00:10:28.809 --> 00:10:31.410 align:start position:0% generality so it's an open question there's<00:10:29.800> also<00:10:29.980> a<00:10:30.129> lot<00:10:30.790> of<00:10:30.910> potential<00:10:31.179> for 00:10:31.410 --> 00:10:31.420 align:start position:0% there's also a lot of potential for 00:10:31.420 --> 00:10:33.470 align:start position:0% there's also a lot of potential for abuse<00:10:31.509> and<00:10:31.899> escape<00:10:32.139> hatches<00:10:32.379> so 00:10:33.470 --> 00:10:33.480 align:start position:0% abuse and escape hatches so 00:10:33.480 --> 00:10:36.360 align:start position:0% abuse and escape hatches so a<00:10:34.480> bad<00:10:34.929> actor<00:10:35.259> could<00:10:35.470> perhaps<00:10:35.620> trigger<00:10:36.220> an 00:10:36.360 --> 00:10:36.370 align:start position:0% a bad actor could perhaps trigger an 00:10:36.370 --> 00:10:37.799 align:start position:0% a bad actor could perhaps trigger an escape<00:10:36.639> hatch<00:10:36.819> in<00:10:37.149> a<00:10:37.269> case<00:10:37.480> where<00:10:37.689> it's 00:10:37.799 --> 00:10:37.809 align:start position:0% escape hatch in a case where it's 00:10:37.809 --> 00:10:39.629 align:start position:0% escape hatch in a case where it's profitable<00:10:38.410> for<00:10:38.559> them<00:10:38.649> even<00:10:39.069> if<00:10:39.189> it<00:10:39.309> doesn't 00:10:39.629 --> 00:10:39.639 align:start position:0% profitable for them even if it doesn't 00:10:39.639 --> 00:10:41.129 align:start position:0% profitable for them even if it doesn't follow<00:10:39.790> the<00:10:40.089> intent<00:10:40.420> of<00:10:40.540> the<00:10:40.660> escape<00:10:40.929> hatch 00:10:41.129 --> 00:10:41.139 align:start position:0% follow the intent of the escape hatch 00:10:41.139 --> 00:10:43.319 align:start position:0% follow the intent of the escape hatch that's<00:10:42.040> something<00:10:42.339> we<00:10:42.459> always<00:10:42.850> sort<00:10:43.059> of<00:10:43.149> need 00:10:43.319 --> 00:10:43.329 align:start position:0% that's something we always sort of need 00:10:43.329 --> 00:10:46.110 align:start position:0% that's something we always sort of need to<00:10:43.420> keep<00:10:43.600> in<00:10:43.720> mind<00:10:44.399> okay<00:10:45.399> so<00:10:45.670> can<00:10:45.790> you<00:10:45.850> think<00:10:45.910> of 00:10:46.110 --> 00:10:46.120 align:start position:0% to keep in mind okay so can you think of 00:10:46.120 --> 00:10:48.389 align:start position:0% to keep in mind okay so can you think of a<00:10:46.209> badly<00:10:46.389> made<00:10:46.569> escape<00:10:47.019> hatch<00:10:47.199> there<00:10:47.709> is<00:10:47.800> there 00:10:48.389 --> 00:10:48.399 align:start position:0% a badly made escape hatch there is there 00:10:48.399 --> 00:10:50.009 align:start position:0% a badly made escape hatch there is there have<00:10:48.490> definitely<00:10:48.519> been<00:10:48.970> contracts<00:10:49.629> before 00:10:50.009 --> 00:10:50.019 align:start position:0% have definitely been contracts before 00:10:50.019 --> 00:10:52.319 align:start position:0% have definitely been contracts before that<00:10:50.829> have<00:10:51.040> intended<00:10:51.819> to<00:10:51.970> provide<00:10:52.269> a 00:10:52.319 --> 00:10:52.329 align:start position:0% that have intended to provide a 00:10:52.329 --> 00:10:54.600 align:start position:0% that have intended to provide a mechanism<00:10:52.749> for<00:10:52.929> users<00:10:53.319> to<00:10:53.499> remove<00:10:53.709> funds<00:10:54.129> that 00:10:54.600 --> 00:10:54.610 align:start position:0% mechanism for users to remove funds that 00:10:54.610 --> 00:10:56.460 align:start position:0% mechanism for users to remove funds that have<00:10:54.819> then<00:10:54.970> been<00:10:54.999> abused<00:10:55.749> to<00:10:55.899> drain<00:10:56.199> all<00:10:56.439> of 00:10:56.460 --> 00:10:56.470 align:start position:0% have then been abused to drain all of 00:10:56.470 --> 00:10:58.350 align:start position:0% have then been abused to drain all of the<00:10:56.649> funds<00:10:56.920> out<00:10:57.100> of<00:10:57.129> the<00:10:57.220> system<00:10:57.639> I<00:10:57.879> won't 00:10:58.350 --> 00:10:58.360 align:start position:0% the funds out of the system I won't 00:10:58.360 --> 00:11:00.239 align:start position:0% the funds out of the system I won't mention<00:10:58.509> specifics<00:10:59.170> but<00:10:59.410> it's<00:10:59.589> on<00:10:59.709> line<00:10:59.920> six 00:11:00.239 --> 00:11:00.249 align:start position:0% mention specifics but it's on line six 00:11:00.249 --> 00:11:01.679 align:start position:0% mention specifics but it's on line six six<00:11:00.429> six<00:11:00.579> of<00:11:00.790> the<00:11:00.850> contract<00:11:01.269> that<00:11:01.389> I'm<00:11:01.480> talking 00:11:01.679 --> 00:11:01.689 align:start position:0% six six of the contract that I'm talking 00:11:01.689 --> 00:11:04.379 align:start position:0% six six of the contract that I'm talking about<00:11:02.220> it's<00:11:03.220> also<00:11:03.399> worth<00:11:03.670> noting<00:11:03.879> that<00:11:04.089> that 00:11:04.379 --> 00:11:04.389 align:start position:0% about it's also worth noting that that 00:11:04.389 --> 00:11:06.419 align:start position:0% about it's also worth noting that that Forks<00:11:05.049> of<00:11:05.199> the<00:11:05.290> system<00:11:05.589> in<00:11:05.709> general<00:11:05.860> can<00:11:06.279> be 00:11:06.419 --> 00:11:06.429 align:start position:0% Forks of the system in general can be 00:11:06.429 --> 00:11:08.220 align:start position:0% Forks of the system in general can be viewed<00:11:06.579> as<00:11:06.699> an<00:11:06.790> escape<00:11:07.059> hatch<00:11:07.240> whenever<00:11:08.049> there 00:11:08.220 --> 00:11:08.230 align:start position:0% viewed as an escape hatch whenever there 00:11:08.230 --> 00:11:09.989 align:start position:0% viewed as an escape hatch whenever there is<00:11:08.259> a<00:11:08.350> catastrophic<00:11:08.740> failure<00:11:09.220> involving 00:11:09.989 --> 00:11:09.999 align:start position:0% is a catastrophic failure involving 00:11:09.999 --> 00:11:12.239 align:start position:0% is a catastrophic failure involving multiple<00:11:10.329> aspects<00:11:10.720> of<00:11:10.869> the<00:11:10.959> system<00:11:11.290> you<00:11:12.040> sort 00:11:12.239 --> 00:11:12.249 align:start position:0% multiple aspects of the system you sort 00:11:12.249 --> 00:11:14.160 align:start position:0% multiple aspects of the system you sort of<00:11:12.279> get<00:11:12.459> the<00:11:12.579> social<00:11:12.999> consensus<00:11:13.569> based<00:11:13.809> escape 00:11:14.160 --> 00:11:14.170 align:start position:0% of get the social consensus based escape 00:11:14.170 --> 00:11:16.619 align:start position:0% of get the social consensus based escape hatch<00:11:14.379> that<00:11:14.649> comes<00:11:14.939> with<00:11:15.939> the<00:11:16.269> back<00:11:16.449> end 00:11:16.619 --> 00:11:16.629 align:start position:0% hatch that comes with the back end 00:11:16.629 --> 00:11:18.720 align:start position:0% hatch that comes with the back end architecture<00:11:17.170> of<00:11:17.259> these<00:11:17.379> systems 00:11:18.720 --> 00:11:18.730 align:start position:0% architecture of these systems 00:11:18.730 --> 00:11:21.540 align:start position:0% architecture of these systems all<00:11:19.389> right<00:11:19.959> the<00:11:20.260> last<00:11:20.470> prong<00:11:20.800> of<00:11:21.130> our<00:11:21.250> three 00:11:21.540 --> 00:11:21.550 align:start position:0% all right the last prong of our three 00:11:21.550 --> 00:11:24.660 align:start position:0% all right the last prong of our three three-pronged<00:11:22.269> fork<00:11:22.389> bug<00:11:23.320> bounties<00:11:23.709> so<00:11:24.550> we 00:11:24.660 --> 00:11:24.670 align:start position:0% three-pronged fork bug bounties so we 00:11:24.670 --> 00:11:26.699 align:start position:0% three-pronged fork bug bounties so we believe<00:11:24.970> bug<00:11:25.209> bounties<00:11:25.600> are<00:11:25.779> very<00:11:26.199> important 00:11:26.699 --> 00:11:26.709 align:start position:0% believe bug bounties are very important 00:11:26.709 --> 00:11:29.100 align:start position:0% believe bug bounties are very important because<00:11:27.160> the<00:11:27.519> incentivization<00:11:28.389> structure<00:11:28.870> of 00:11:29.100 --> 00:11:29.110 align:start position:0% because the incentivization structure of 00:11:29.110 --> 00:11:31.500 align:start position:0% because the incentivization structure of developing<00:11:29.709> exploits<00:11:30.190> is<00:11:30.850> pretty<00:11:31.240> broken 00:11:31.500 --> 00:11:31.510 align:start position:0% developing exploits is pretty broken 00:11:31.510 --> 00:11:33.569 align:start position:0% developing exploits is pretty broken without<00:11:31.750> bounties<00:11:32.290> so<00:11:33.040> what<00:11:33.250> do<00:11:33.310> we<00:11:33.339> mean<00:11:33.550> by 00:11:33.569 --> 00:11:33.579 align:start position:0% without bounties so what do we mean by 00:11:33.579 --> 00:11:35.910 align:start position:0% without bounties so what do we mean by this<00:11:33.930> insecurity<00:11:34.930> traditionally<00:11:35.560> we<00:11:35.709> say 00:11:35.910 --> 00:11:35.920 align:start position:0% this insecurity traditionally we say 00:11:35.920 --> 00:11:37.620 align:start position:0% this insecurity traditionally we say it's<00:11:36.190> never<00:11:36.370> impossible<00:11:36.610> to<00:11:37.209> exploit<00:11:37.570> a 00:11:37.620 --> 00:11:37.630 align:start position:0% it's never impossible to exploit a 00:11:37.630 --> 00:11:40.410 align:start position:0% it's never impossible to exploit a system<00:11:38.170> it<00:11:38.380> can<00:11:38.529> only<00:11:38.680> be<00:11:38.889> expensive<00:11:39.490> and<00:11:39.699> when 00:11:40.410 --> 00:11:40.420 align:start position:0% system it can only be expensive and when 00:11:40.420 --> 00:11:42.300 align:start position:0% system it can only be expensive and when you<00:11:40.510> have<00:11:40.690> a<00:11:40.720> cost<00:11:41.110> of<00:11:41.290> exploiting<00:11:41.860> a<00:11:41.949> system 00:11:42.300 --> 00:11:42.310 align:start position:0% you have a cost of exploiting a system 00:11:42.310 --> 00:11:43.920 align:start position:0% you have a cost of exploiting a system that's<00:11:42.550> actually<00:11:43.000> much<00:11:43.209> lower<00:11:43.480> than<00:11:43.779> the 00:11:43.920 --> 00:11:43.930 align:start position:0% that's actually much lower than the 00:11:43.930 --> 00:11:45.120 align:start position:0% that's actually much lower than the amount<00:11:44.110> that's<00:11:44.350> to<00:11:44.500> be<00:11:44.620> gained<00:11:44.860> from 00:11:45.120 --> 00:11:45.130 align:start position:0% amount that's to be gained from 00:11:45.130 --> 00:11:47.579 align:start position:0% amount that's to be gained from exploiting<00:11:45.670> it<00:11:45.790> an<00:11:46.540> exploit<00:11:47.079> and<00:11:47.260> an<00:11:47.320> attack 00:11:47.579 --> 00:11:47.589 align:start position:0% exploiting it an exploit and an attack 00:11:47.589 --> 00:11:50.370 align:start position:0% exploiting it an exploit and an attack will<00:11:47.769> pretty<00:11:47.949> much<00:11:48.040> inevitably<00:11:48.790> surface<00:11:49.380> so 00:11:50.370 --> 00:11:50.380 align:start position:0% will pretty much inevitably surface so 00:11:50.380 --> 00:11:52.650 align:start position:0% will pretty much inevitably surface so in<00:11:50.500> order<00:11:50.589> to<00:11:50.800> fix<00:11:51.010> these<00:11:51.370> sort<00:11:51.850> of<00:11:51.970> issues<00:11:52.389> the 00:11:52.650 --> 00:11:52.660 align:start position:0% in order to fix these sort of issues the 00:11:52.660 --> 00:11:54.150 align:start position:0% in order to fix these sort of issues the general<00:11:52.990> security<00:11:53.170> community<00:11:53.920> has 00:11:54.150 --> 00:11:54.160 align:start position:0% general security community has 00:11:54.160 --> 00:11:56.340 align:start position:0% general security community has recognized<00:11:54.790> the<00:11:54.940> value<00:11:55.089> of<00:11:55.360> providing 00:11:56.340 --> 00:11:56.350 align:start position:0% recognized the value of providing 00:11:56.350 --> 00:11:58.800 align:start position:0% recognized the value of providing bounties<00:11:56.740> to<00:11:57.040> incentivize<00:11:58.029> people<00:11:58.240> to<00:11:58.420> defend 00:11:58.800 --> 00:11:58.810 align:start position:0% bounties to incentivize people to defend 00:11:58.810 --> 00:12:01.350 align:start position:0% bounties to incentivize people to defend the<00:11:58.990> system<00:11:59.350> financially<00:12:00.040> rather<00:12:00.910> than<00:12:01.149> only 00:12:01.350 --> 00:12:01.360 align:start position:0% the system financially rather than only 00:12:01.360 --> 00:12:03.259 align:start position:0% the system financially rather than only financially<00:12:02.019> incentivizing<00:12:02.740> attackers 00:12:03.259 --> 00:12:03.269 align:start position:0% financially incentivizing attackers 00:12:03.269 --> 00:12:05.579 align:start position:0% financially incentivizing attackers without<00:12:04.269> them<00:12:04.510> defenders<00:12:05.019> are<00:12:05.199> really<00:12:05.470> only 00:12:05.579 --> 00:12:05.589 align:start position:0% without them defenders are really only 00:12:05.589 --> 00:12:08.730 align:start position:0% without them defenders are really only motivated<00:12:06.160> by<00:12:06.279> ego<00:12:06.730> or<00:12:07.240> maybe<00:12:07.510> goodwill<00:12:08.019> which 00:12:08.730 --> 00:12:08.740 align:start position:0% motivated by ego or maybe goodwill which 00:12:08.740 --> 00:12:10.829 align:start position:0% motivated by ego or maybe goodwill which as<00:12:09.070> we've<00:12:09.339> seen<00:12:09.550> in<00:12:09.639> the<00:12:09.730> past<00:12:09.880> are<00:12:10.180> not<00:12:10.420> really 00:12:10.829 --> 00:12:10.839 align:start position:0% as we've seen in the past are not really 00:12:10.839 --> 00:12:13.259 align:start position:0% as we've seen in the past are not really powerful<00:12:11.260> motivators<00:12:11.860> to<00:12:12.760> do<00:12:12.910> the<00:12:13.029> type<00:12:13.240> of 00:12:13.259 --> 00:12:13.269 align:start position:0% powerful motivators to do the type of 00:12:13.269 --> 00:12:15.240 align:start position:0% powerful motivators to do the type of work<00:12:13.600> that's<00:12:13.839> required<00:12:14.230> for<00:12:14.529> a<00:12:14.589> full<00:12:14.769> security 00:12:15.240 --> 00:12:15.250 align:start position:0% work that's required for a full security 00:12:15.250 --> 00:12:16.759 align:start position:0% work that's required for a full security audit 00:12:16.759 --> 00:12:16.769 align:start position:0% audit 00:12:16.769 --> 00:12:19.860 align:start position:0% audit so<00:12:17.769> the<00:12:18.610> good<00:12:18.760> about<00:12:18.940> bug<00:12:19.180> bounties<00:12:19.540> we<00:12:19.720> have 00:12:19.860 --> 00:12:19.870 align:start position:0% so the good about bug bounties we have 00:12:19.870 --> 00:12:22.110 align:start position:0% so the good about bug bounties we have the<00:12:20.199> poor<00:12:20.410> man's<00:12:20.649> formal<00:12:21.100> verification<00:12:21.279> or<00:12:21.970> as 00:12:22.110 --> 00:12:22.120 align:start position:0% the poor man's formal verification or as 00:12:22.120 --> 00:12:23.550 align:start position:0% the poor man's formal verification or as we<00:12:22.300> like<00:12:22.480> to<00:12:22.510> call<00:12:22.630> it<00:12:22.930> decentralized 00:12:23.550 --> 00:12:23.560 align:start position:0% we like to call it decentralized 00:12:23.560 --> 00:12:25.019 align:start position:0% we like to call it decentralized censorship<00:12:24.130> resistant<00:12:24.550> anti<00:12:24.790> fragile 00:12:25.019 --> 00:12:25.029 align:start position:0% censorship resistant anti fragile 00:12:25.029 --> 00:12:26.759 align:start position:0% censorship resistant anti fragile incentive<00:12:25.690> compatible<00:12:26.199> crowd-sourced 00:12:26.759 --> 00:12:26.769 align:start position:0% incentive compatible crowd-sourced 00:12:26.769 --> 00:12:29.550 align:start position:0% incentive compatible crowd-sourced verification<00:12:27.899> you<00:12:28.899> can<00:12:29.050> tell<00:12:29.199> that<00:12:29.350> one<00:12:29.529> to 00:12:29.550 --> 00:12:29.560 align:start position:0% verification you can tell that one to 00:12:29.560 --> 00:12:31.170 align:start position:0% verification you can tell that one to your<00:12:29.800> managers<00:12:30.190> and<00:12:30.220> I'm<00:12:30.550> sure<00:12:30.730> they'll<00:12:30.910> be 00:12:31.170 --> 00:12:31.180 align:start position:0% your managers and I'm sure they'll be 00:12:31.180 --> 00:12:32.490 align:start position:0% your managers and I'm sure they'll be glad<00:12:31.329> to<00:12:31.660> fund<00:12:31.870> your<00:12:31.990> escape<00:12:32.199> hatch 00:12:32.490 --> 00:12:32.500 align:start position:0% glad to fund your escape hatch 00:12:32.500 --> 00:12:33.860 align:start position:0% glad to fund your escape hatch development 00:12:33.860 --> 00:12:33.870 align:start position:0% development 00:12:33.870 --> 00:12:36.509 align:start position:0% development all<00:12:34.870> right<00:12:35.079> so<00:12:35.470> we<00:12:35.589> got<00:12:35.709> some<00:12:35.920> cool<00:12:36.069> work<00:12:36.250> going 00:12:36.509 --> 00:12:36.519 align:start position:0% all right so we got some cool work going 00:12:36.519 --> 00:12:38.340 align:start position:0% all right so we got some cool work going on<00:12:36.579> in<00:12:36.639> this<00:12:36.850> space<00:12:37.000> some<00:12:37.720> of<00:12:37.810> my<00:12:37.930> favorite 00:12:38.340 --> 00:12:38.350 align:start position:0% on in this space some of my favorite 00:12:38.350 --> 00:12:39.480 align:start position:0% on in this space some of my favorite work<00:12:38.470> is<00:12:38.649> the<00:12:38.769> idea<00:12:39.040> of<00:12:39.100> using<00:12:39.279> these 00:12:39.480 --> 00:12:39.490 align:start position:0% work is the idea of using these 00:12:39.490 --> 00:12:40.949 align:start position:0% work is the idea of using these prediction<00:12:39.940> markets<00:12:40.329> that<00:12:40.569> we're<00:12:40.750> developing 00:12:40.949 --> 00:12:40.959 align:start position:0% prediction markets that we're developing 00:12:40.959 --> 00:12:43.680 align:start position:0% prediction markets that we're developing as<00:12:41.470> sort<00:12:42.130> of<00:12:42.160> Canaries<00:12:42.670> for<00:12:43.029> one<00:12:43.149> an<00:12:43.269> exploit 00:12:43.680 --> 00:12:43.690 align:start position:0% as sort of Canaries for one an exploit 00:12:43.690 --> 00:12:45.720 align:start position:0% as sort of Canaries for one an exploit is<00:12:43.839> about<00:12:44.019> to<00:12:44.170> happen<00:12:44.350> because<00:12:45.130> attackers 00:12:45.720 --> 00:12:45.730 align:start position:0% is about to happen because attackers 00:12:45.730 --> 00:12:47.730 align:start position:0% is about to happen because attackers will<00:12:45.880> naturally<00:12:46.029> be<00:12:46.389> incentivized<00:12:46.990> to<00:12:47.319> to 00:12:47.730 --> 00:12:47.740 align:start position:0% will naturally be incentivized to to 00:12:47.740 --> 00:12:49.769 align:start position:0% will naturally be incentivized to to reveal<00:12:48.069> this<00:12:48.279> by<00:12:48.550> taking<00:12:48.970> a<00:12:49.060> position<00:12:49.240> on<00:12:49.630> the 00:12:49.769 --> 00:12:49.779 align:start position:0% reveal this by taking a position on the 00:12:49.779 --> 00:12:52.889 align:start position:0% reveal this by taking a position on the prediction<00:12:50.170> markets<00:12:50.589> in<00:12:51.519> that<00:12:51.579> direction<00:12:51.940> so 00:12:52.889 --> 00:12:52.899 align:start position:0% prediction markets in that direction so 00:12:52.899 --> 00:12:54.240 align:start position:0% prediction markets in that direction so that's<00:12:53.110> sort<00:12:53.410> of<00:12:53.500> the<00:12:53.560> more<00:12:53.800> fringe<00:12:54.040> work 00:12:54.240 --> 00:12:54.250 align:start position:0% that's sort of the more fringe work 00:12:54.250 --> 00:12:55.680 align:start position:0% that's sort of the more fringe work that's<00:12:54.459> going<00:12:54.699> on<00:12:54.790> we<00:12:55.000> also<00:12:55.149> have<00:12:55.389> work<00:12:55.660> that 00:12:55.680 --> 00:12:55.690 align:start position:0% that's going on we also have work that 00:12:55.690 --> 00:12:57.840 align:start position:0% that's going on we also have work that directly<00:12:56.260> addresses<00:12:56.769> these<00:12:56.920> issues<00:12:56.980> in<00:12:57.639> a 00:12:57.840 --> 00:12:57.850 align:start position:0% directly addresses these issues in a 00:12:57.850 --> 00:12:59.850 align:start position:0% directly addresses these issues in a more<00:12:57.880> traditional<00:12:58.149> way<00:12:58.510> so<00:12:59.350> there's<00:12:59.529> a<00:12:59.620> blog 00:12:59.850 --> 00:12:59.860 align:start position:0% more traditional way so there's a blog 00:12:59.860 --> 00:13:02.040 align:start position:0% more traditional way so there's a blog post<00:13:00.160> by<00:13:00.399> Simone<00:13:00.940> de<00:13:01.089> la<00:13:01.209> riviere<00:13:01.600> again<00:13:02.019> I 00:13:02.040 --> 00:13:02.050 align:start position:0% post by Simone de la riviere again I 00:13:02.050 --> 00:13:04.199 align:start position:0% post by Simone de la riviere again I hope<00:13:02.260> I'm<00:13:02.410> pronouncing<00:13:02.440> that<00:13:02.889> right<00:13:03.209> on 00:13:04.199 --> 00:13:04.209 align:start position:0% hope I'm pronouncing that right on 00:13:04.209 --> 00:13:06.240 align:start position:0% hope I'm pronouncing that right on medium<00:13:04.660> called<00:13:04.899> asset<00:13:05.290> cards<00:13:05.620> which<00:13:05.889> I<00:13:05.980> highly 00:13:06.240 --> 00:13:06.250 align:start position:0% medium called asset cards which I highly 00:13:06.250 --> 00:13:08.160 align:start position:0% medium called asset cards which I highly suggest<00:13:06.370> you<00:13:06.610> take<00:13:06.760> a<00:13:06.819> look<00:13:07.029> at<00:13:07.209> that<00:13:07.660> details 00:13:08.160 --> 00:13:08.170 align:start position:0% suggest you take a look at that details 00:13:08.170 --> 00:13:10.230 align:start position:0% suggest you take a look at that details one<00:13:08.529> potential<00:13:09.040> approach<00:13:09.399> for<00:13:09.970> escape 00:13:10.230 --> 00:13:10.240 align:start position:0% one potential approach for escape 00:13:10.240 --> 00:13:12.000 align:start position:0% one potential approach for escape hatches<00:13:10.810> there's<00:13:11.260> also<00:13:11.529> escape<00:13:11.800> hatches 00:13:12.000 --> 00:13:12.010 align:start position:0% hatches there's also escape hatches 00:13:12.010 --> 00:13:14.009 align:start position:0% hatches there's also escape hatches mentioned<00:13:12.490> in<00:13:12.550> the<00:13:12.670> etherium<00:13:13.149> best<00:13:13.480> practices 00:13:14.009 --> 00:13:14.019 align:start position:0% mentioned in the etherium best practices 00:13:14.019 --> 00:13:15.990 align:start position:0% mentioned in the etherium best practices for<00:13:14.170> smart<00:13:14.410> contracts<00:13:14.860> documentation<00:13:15.699> and 00:13:15.990 --> 00:13:16.000 align:start position:0% for smart contracts documentation and 00:13:16.000 --> 00:13:18.329 align:start position:0% for smart contracts documentation and there's<00:13:16.779> a<00:13:16.870> user<00:13:17.050> called<00:13:17.470> doubt<00:13:17.680> challenge<00:13:18.190> on 00:13:18.329 --> 00:13:18.339 align:start position:0% there's a user called doubt challenge on 00:13:18.339 --> 00:13:20.280 align:start position:0% there's a user called doubt challenge on medium<00:13:18.670> who's<00:13:18.910> posted<00:13:19.329> a<00:13:19.420> series<00:13:19.990> of<00:13:20.019> really 00:13:20.280 --> 00:13:20.290 align:start position:0% medium who's posted a series of really 00:13:20.290 --> 00:13:22.350 align:start position:0% medium who's posted a series of really small<00:13:20.709> contracts<00:13:21.310> that<00:13:21.519> contain<00:13:21.910> common 00:13:22.350 --> 00:13:22.360 align:start position:0% small contracts that contain common 00:13:22.360 --> 00:13:24.629 align:start position:0% small contracts that contain common patterns<00:13:22.779> and<00:13:23.079> ask<00:13:23.740> the<00:13:23.920> community<00:13:24.040> to<00:13:24.430> try<00:13:24.550> to 00:13:24.629 --> 00:13:24.639 align:start position:0% patterns and ask the community to try to 00:13:24.639 --> 00:13:26.910 align:start position:0% patterns and ask the community to try to break<00:13:24.910> these<00:13:25.060> contracts<00:13:25.660> in<00:13:26.230> order<00:13:26.380> to<00:13:26.589> reveal 00:13:26.910 --> 00:13:26.920 align:start position:0% break these contracts in order to reveal 00:13:26.920 --> 00:13:29.490 align:start position:0% break these contracts in order to reveal underlying<00:13:27.490> language<00:13:27.730> flaws<00:13:28.240> or<00:13:28.899> issues<00:13:28.930> in 00:13:29.490 --> 00:13:29.500 align:start position:0% underlying language flaws or issues in 00:13:29.500 --> 00:13:31.199 align:start position:0% underlying language flaws or issues in our<00:13:29.589> coding<00:13:29.980> practices<00:13:30.459> that<00:13:30.640> we<00:13:30.790> haven't 00:13:31.199 --> 00:13:31.209 align:start position:0% our coding practices that we haven't 00:13:31.209 --> 00:13:32.580 align:start position:0% our coding practices that we haven't really<00:13:31.480> yet<00:13:31.600> thought<00:13:31.839> of 00:13:32.580 --> 00:13:32.590 align:start position:0% really yet thought of 00:13:32.590 --> 00:13:34.050 align:start position:0% really yet thought of there's<00:13:32.890> a<00:13:32.980> lot<00:13:33.130> more<00:13:33.160> work<00:13:33.460> going<00:13:33.760> on<00:13:33.850> in<00:13:33.970> this 00:13:34.050 --> 00:13:34.060 align:start position:0% there's a lot more work going on in this 00:13:34.060 --> 00:13:36.570 align:start position:0% there's a lot more work going on in this space<00:13:34.330> if<00:13:34.930> you<00:13:34.990> google<00:13:35.320> escape<00:13:35.740> sorry<00:13:36.340> bug 00:13:36.570 --> 00:13:36.580 align:start position:0% space if you google escape sorry bug 00:13:36.580 --> 00:13:38.490 align:start position:0% space if you google escape sorry bug bounties<00:13:36.940> if<00:13:37.390> you're<00:13:37.570> my<00:13:37.930> bounty<00:13:38.230> smart 00:13:38.490 --> 00:13:38.500 align:start position:0% bounties if you're my bounty smart 00:13:38.500 --> 00:13:40.410 align:start position:0% bounties if you're my bounty smart contracts<00:13:38.950> you'll<00:13:39.760> come<00:13:39.940> up<00:13:39.970> with<00:13:40.060> a<00:13:40.180> ton<00:13:40.390> of 00:13:40.410 --> 00:13:40.420 align:start position:0% contracts you'll come up with a ton of 00:13:40.420 --> 00:13:43.290 align:start position:0% contracts you'll come up with a ton of stuff<00:13:40.720> so<00:13:41.529> there's<00:13:41.710> a<00:13:41.800> common<00:13:42.100> problem<00:13:42.550> in<00:13:43.029> in 00:13:43.290 --> 00:13:43.300 align:start position:0% stuff so there's a common problem in in 00:13:43.300 --> 00:13:44.850 align:start position:0% stuff so there's a common problem in in academia<00:13:43.630> and<00:13:43.870> in<00:13:43.960> general<00:13:44.350> that<00:13:44.380> you<00:13:44.650> have 00:13:44.850 --> 00:13:44.860 align:start position:0% academia and in general that you have 00:13:44.860 --> 00:13:46.530 align:start position:0% academia and in general that you have all<00:13:45.160> of<00:13:45.279> these<00:13:45.400> great<00:13:45.700> solutions<00:13:46.300> to<00:13:46.450> the 00:13:46.530 --> 00:13:46.540 align:start position:0% all of these great solutions to the 00:13:46.540 --> 00:13:47.820 align:start position:0% all of these great solutions to the escape<00:13:46.779> hatch<00:13:46.960> problem<00:13:47.380> and<00:13:47.500> all<00:13:47.560> these<00:13:47.650> great 00:13:47.820 --> 00:13:47.830 align:start position:0% escape hatch problem and all these great 00:13:47.830 --> 00:13:49.350 align:start position:0% escape hatch problem and all these great proposals<00:13:48.340> and<00:13:48.430> you<00:13:48.520> consider<00:13:48.910> the<00:13:49.060> problem 00:13:49.350 --> 00:13:49.360 align:start position:0% proposals and you consider the problem 00:13:49.360 --> 00:13:51.630 align:start position:0% proposals and you consider the problem solved<00:13:50.080> and<00:13:50.170> I<00:13:50.980> would<00:13:51.130> urge<00:13:51.250> you<00:13:51.460> guys<00:13:51.490> to 00:13:51.630 --> 00:13:51.640 align:start position:0% solved and I would urge you guys to 00:13:51.640 --> 00:13:53.400 align:start position:0% solved and I would urge you guys to avoid<00:13:52.120> that<00:13:52.300> line<00:13:52.480> of<00:13:52.660> thinking<00:13:52.810> because 00:13:53.400 --> 00:13:53.410 align:start position:0% avoid that line of thinking because 00:13:53.410 --> 00:13:55.260 align:start position:0% avoid that line of thinking because there<00:13:53.589> are<00:13:53.710> still<00:13:53.920> gaps<00:13:54.190> in<00:13:54.580> this<00:13:54.700> in<00:13:54.910> this<00:13:55.029> bug 00:13:55.260 --> 00:13:55.270 align:start position:0% there are still gaps in this in this bug 00:13:55.270 --> 00:13:57.510 align:start position:0% there are still gaps in this in this bug bounty<00:13:55.660> approach<00:13:56.320> so<00:13:56.980> with<00:13:57.130> prediction 00:13:57.510 --> 00:13:57.520 align:start position:0% bounty approach so with prediction 00:13:57.520 --> 00:13:58.860 align:start position:0% bounty approach so with prediction markets<00:13:57.850> there's<00:13:58.029> always<00:13:58.240> the<00:13:58.480> question<00:13:58.600> of 00:13:58.860 --> 00:13:58.870 align:start position:0% markets there's always the question of 00:13:58.870 --> 00:14:00.570 align:start position:0% markets there's always the question of how<00:13:58.990> to<00:13:59.050> avoid<00:13:59.350> bad<00:13:59.620> incentives<00:14:00.190> and<00:14:00.370> how<00:14:00.430> to 00:14:00.570 --> 00:14:00.580 align:start position:0% how to avoid bad incentives and how to 00:14:00.580 --> 00:14:02.850 align:start position:0% how to avoid bad incentives and how to prevent<00:14:01.029> incentivizing<00:14:02.020> attackers<00:14:02.500> and<00:14:02.680> bad 00:14:02.850 --> 00:14:02.860 align:start position:0% prevent incentivizing attackers and bad 00:14:02.860 --> 00:14:05.070 align:start position:0% prevent incentivizing attackers and bad actors<00:14:03.250> from<00:14:04.060> actually<00:14:04.540> deploying<00:14:04.839> their 00:14:05.070 --> 00:14:05.080 align:start position:0% actors from actually deploying their 00:14:05.080 --> 00:14:06.450 align:start position:0% actors from actually deploying their attacks<00:14:05.350> on<00:14:05.470> the<00:14:05.560> main<00:14:05.710> end<00:14:05.890> and<00:14:06.010> profiting 00:14:06.450 --> 00:14:06.460 align:start position:0% attacks on the main end and profiting 00:14:06.460 --> 00:14:08.460 align:start position:0% attacks on the main end and profiting there's<00:14:07.120> also<00:14:07.270> the<00:14:07.480> hard<00:14:07.720> problem<00:14:08.170> of<00:14:08.260> how<00:14:08.410> to 00:14:08.460 --> 00:14:08.470 align:start position:0% there's also the hard problem of how to 00:14:08.470 --> 00:14:10.079 align:start position:0% there's also the hard problem of how to create<00:14:08.680> trustless<00:14:09.250> bounties<00:14:09.610> with<00:14:09.790> trustless 00:14:10.079 --> 00:14:10.089 align:start position:0% create trustless bounties with trustless 00:14:10.089 --> 00:14:11.850 align:start position:0% create trustless bounties with trustless payout<00:14:10.450> we<00:14:11.020> don't<00:14:11.230> want<00:14:11.410> to<00:14:11.500> leak<00:14:11.650> these 00:14:11.850 --> 00:14:11.860 align:start position:0% payout we don't want to leak these 00:14:11.860 --> 00:14:13.560 align:start position:0% payout we don't want to leak these exploits<00:14:12.279> to<00:14:12.370> the<00:14:12.460> test<00:14:12.670> net<00:14:12.880> because<00:14:13.390> once 00:14:13.560 --> 00:14:13.570 align:start position:0% exploits to the test net because once 00:14:13.570 --> 00:14:14.850 align:start position:0% exploits to the test net because once you<00:14:13.660> leak<00:14:13.870> the<00:14:13.990> exploit<00:14:14.260> to<00:14:14.350> the<00:14:14.440> test<00:14:14.650> net 00:14:14.850 --> 00:14:14.860 align:start position:0% you leak the exploit to the test net 00:14:14.860 --> 00:14:16.170 align:start position:0% you leak the exploit to the test net you've<00:14:15.040> removed<00:14:15.370> the<00:14:15.640> incentive<00:14:16.060> for 00:14:16.170 --> 00:14:16.180 align:start position:0% you've removed the incentive for 00:14:16.180 --> 00:14:18.120 align:start position:0% you've removed the incentive for defenders<00:14:16.600> and<00:14:16.870> attackers<00:14:17.230> can<00:14:17.740> take<00:14:17.950> that 00:14:18.120 --> 00:14:18.130 align:start position:0% defenders and attackers can take that 00:14:18.130 --> 00:14:20.190 align:start position:0% defenders and attackers can take that exploit<00:14:18.490> and<00:14:18.640> deploy<00:14:18.850> it<00:14:18.940> on<00:14:19.029> the<00:14:19.120> main<00:14:19.270> net<00:14:19.510> we 00:14:20.190 --> 00:14:20.200 align:start position:0% exploit and deploy it on the main net we 00:14:20.200 --> 00:14:21.600 align:start position:0% exploit and deploy it on the main net we also<00:14:20.350> don't<00:14:20.620> want<00:14:20.770> to<00:14:20.920> trust<00:14:21.130> contract 00:14:21.600 --> 00:14:21.610 align:start position:0% also don't want to trust contract 00:14:21.610 --> 00:14:22.950 align:start position:0% also don't want to trust contract authors<00:14:21.940> to<00:14:22.060> pay<00:14:22.240> out<00:14:22.390> because<00:14:22.810> that 00:14:22.950 --> 00:14:22.960 align:start position:0% authors to pay out because that 00:14:22.960 --> 00:14:25.380 align:start position:0% authors to pay out because that significantly<00:14:23.620> harms<00:14:24.040> the<00:14:24.390> attackers 00:14:25.380 --> 00:14:25.390 align:start position:0% significantly harms the attackers 00:14:25.390 --> 00:14:28.170 align:start position:0% significantly harms the attackers incentive<00:14:25.839> to<00:14:25.990> report<00:14:26.380> the<00:14:26.920> the<00:14:26.950> bug<00:14:27.790> if<00:14:28.060> they 00:14:28.170 --> 00:14:28.180 align:start position:0% incentive to report the the bug if they 00:14:28.180 --> 00:14:29.790 align:start position:0% incentive to report the the bug if they think<00:14:28.240> it's<00:14:28.480> a<00:14:28.570> really<00:14:28.810> profitable<00:14:29.260> bug<00:14:29.529> and 00:14:29.790 --> 00:14:29.800 align:start position:0% think it's a really profitable bug and 00:14:29.800 --> 00:14:31.740 align:start position:0% think it's a really profitable bug and the<00:14:30.040> contract<00:14:30.430> authors<00:14:30.730> may<00:14:30.910> just<00:14:31.180> invoke<00:14:31.690> a 00:14:31.740 --> 00:14:31.750 align:start position:0% the contract authors may just invoke a 00:14:31.750 --> 00:14:33.420 align:start position:0% the contract authors may just invoke a kill<00:14:32.020> switch<00:14:32.200> or<00:14:32.440> fix<00:14:32.650> it<00:14:32.860> before<00:14:33.010> they<00:14:33.310> have 00:14:33.420 --> 00:14:33.430 align:start position:0% kill switch or fix it before they have 00:14:33.430 --> 00:14:35.820 align:start position:0% kill switch or fix it before they have the<00:14:33.550> chance<00:14:33.760> to<00:14:33.850> get<00:14:34.000> paid<00:14:34.470> there's<00:14:35.470> also<00:14:35.620> the 00:14:35.820 --> 00:14:35.830 align:start position:0% the chance to get paid there's also the 00:14:35.830 --> 00:14:37.230 align:start position:0% the chance to get paid there's also the very<00:14:36.070> very<00:14:36.310> hard<00:14:36.550> problem<00:14:36.850> of<00:14:36.940> how<00:14:37.089> do<00:14:37.150> we 00:14:37.230 --> 00:14:37.240 align:start position:0% very very hard problem of how do we 00:14:37.240 --> 00:14:39.000 align:start position:0% very very hard problem of how do we define<00:14:37.570> conditions<00:14:38.170> for<00:14:38.350> bug<00:14:38.470> bounties<00:14:38.800> how 00:14:39.000 --> 00:14:39.010 align:start position:0% define conditions for bug bounties how 00:14:39.010 --> 00:14:41.010 align:start position:0% define conditions for bug bounties how do<00:14:39.070> we<00:14:39.220> know<00:14:39.400> when<00:14:39.700> an<00:14:39.820> exploit<00:14:40.240> is<00:14:40.480> a<00:14:40.510> valid 00:14:41.010 --> 00:14:41.020 align:start position:0% do we know when an exploit is a valid 00:14:41.020 --> 00:14:43.260 align:start position:0% do we know when an exploit is a valid claim<00:14:41.170> of<00:14:41.440> a<00:14:41.500> bounty<00:14:41.850> we<00:14:42.850> have<00:14:42.970> a<00:14:43.000> bunch<00:14:43.210> of 00:14:43.260 --> 00:14:43.270 align:start position:0% claim of a bounty we have a bunch of 00:14:43.270 --> 00:14:44.910 align:start position:0% claim of a bounty we have a bunch of academic<00:14:43.780> solutions<00:14:44.170> here<00:14:44.440> sealed<00:14:44.800> glass 00:14:44.910 --> 00:14:44.920 align:start position:0% academic solutions here sealed glass 00:14:44.920 --> 00:14:47.130 align:start position:0% academic solutions here sealed glass proofs<00:14:45.430> we<00:14:45.730> have<00:14:45.880> a<00:14:45.910> paper<00:14:46.150> about<00:14:46.420> that<00:14:46.480> on<00:14:46.900> our 00:14:47.130 --> 00:14:47.140 align:start position:0% proofs we have a paper about that on our 00:14:47.140 --> 00:14:49.230 align:start position:0% proofs we have a paper about that on our website<00:14:47.350> that<00:14:48.310> basically<00:14:48.670> involves<00:14:49.089> using 00:14:49.230 --> 00:14:49.240 align:start position:0% website that basically involves using 00:14:49.240 --> 00:14:51.180 align:start position:0% website that basically involves using trusted<00:14:49.780> hardware<00:14:50.140> to<00:14:50.290> deliver<00:14:50.560> a<00:14:50.650> proof<00:14:50.980> of 00:14:51.180 --> 00:14:51.190 align:start position:0% trusted hardware to deliver a proof of 00:14:51.190 --> 00:14:52.800 align:start position:0% trusted hardware to deliver a proof of an<00:14:51.310> exploit<00:14:51.700> without<00:14:52.030> revealing<00:14:52.270> the<00:14:52.450> exploit 00:14:52.800 --> 00:14:52.810 align:start position:0% an exploit without revealing the exploit 00:14:52.810 --> 00:14:53.930 align:start position:0% an exploit without revealing the exploit itself 00:14:53.930 --> 00:14:53.940 align:start position:0% itself 00:14:53.940 --> 00:14:56.520 align:start position:0% itself SGX<00:14:54.940> also<00:14:55.360> leverages<00:14:55.870> trusted<00:14:56.200> hardware 00:14:56.520 --> 00:14:56.530 align:start position:0% SGX also leverages trusted hardware 00:14:56.530 --> 00:14:58.260 align:start position:0% SGX also leverages trusted hardware maybe<00:14:57.130> zero<00:14:57.400> knowledge<00:14:57.580> proof<00:14:57.730> could<00:14:58.150> be 00:14:58.260 --> 00:14:58.270 align:start position:0% maybe zero knowledge proof could be 00:14:58.270 --> 00:15:01.500 align:start position:0% maybe zero knowledge proof could be useful<00:14:58.390> here<00:14:58.830> etc<00:14:59.880> bug<00:15:00.880> bounties<00:15:01.210> are<00:15:01.300> also 00:15:01.500 --> 00:15:01.510 align:start position:0% useful here etc bug bounties are also 00:15:01.510 --> 00:15:03.150 align:start position:0% useful here etc bug bounties are also hard<00:15:01.660> to<00:15:01.690> do<00:15:01.839> for<00:15:02.020> subtle<00:15:02.260> issues<00:15:02.589> things<00:15:02.980> that 00:15:03.150 --> 00:15:03.160 align:start position:0% hard to do for subtle issues things that 00:15:03.160 --> 00:15:04.860 align:start position:0% hard to do for subtle issues things that I<00:15:03.190> talked<00:15:03.460> about<00:15:03.550> before<00:15:03.790> gain<00:15:04.270> theoretical 00:15:04.860 --> 00:15:04.870 align:start position:0% I talked about before gain theoretical 00:15:04.870 --> 00:15:06.540 align:start position:0% I talked about before gain theoretical issues<00:15:05.260> or<00:15:05.470> fundamental<00:15:06.040> flaws<00:15:06.280> in<00:15:06.460> the 00:15:06.540 --> 00:15:06.550 align:start position:0% issues or fundamental flaws in the 00:15:06.550 --> 00:15:08.640 align:start position:0% issues or fundamental flaws in the architecture<00:15:07.060> of<00:15:07.150> your<00:15:07.210> contracts<00:15:07.810> so<00:15:08.470> like 00:15:08.640 --> 00:15:08.650 align:start position:0% architecture of your contracts so like 00:15:08.650 --> 00:15:09.840 align:start position:0% architecture of your contracts so like our<00:15:08.800> other<00:15:08.950> two<00:15:09.160> prongs<00:15:09.400> they're<00:15:09.700> not<00:15:09.820> a 00:15:09.840 --> 00:15:09.850 align:start position:0% our other two prongs they're not a 00:15:09.850 --> 00:15:10.940 align:start position:0% our other two prongs they're not a silver<00:15:10.150> bullet 00:15:10.940 --> 00:15:10.950 align:start position:0% silver bullet 00:15:10.950 --> 00:15:12.810 align:start position:0% silver bullet also<00:15:11.950> I<00:15:11.980> urge<00:15:12.310> you<00:15:12.460> not<00:15:12.490> to<00:15:12.700> forget 00:15:12.810 --> 00:15:12.820 align:start position:0% also I urge you not to forget 00:15:12.820 --> 00:15:14.370 align:start position:0% also I urge you not to forget traditional<00:15:13.360> software<00:15:13.690> engineering<00:15:14.020> test 00:15:14.370 --> 00:15:14.380 align:start position:0% traditional software engineering test 00:15:14.380 --> 00:15:16.230 align:start position:0% traditional software engineering test fuzzing<00:15:14.830> static<00:15:15.160> dynamic<00:15:15.310> analysis<00:15:16.030> phase 00:15:16.230 --> 00:15:16.240 align:start position:0% fuzzing static dynamic analysis phase 00:15:16.240 --> 00:15:18.329 align:start position:0% fuzzing static dynamic analysis phase deployment<00:15:16.839> upgrades<00:15:17.350> smaller<00:15:18.040> test 00:15:18.329 --> 00:15:18.339 align:start position:0% deployment upgrades smaller test 00:15:18.339 --> 00:15:19.800 align:start position:0% deployment upgrades smaller test contracts<00:15:18.820> these<00:15:19.030> are<00:15:19.150> all<00:15:19.300> very<00:15:19.570> valuable 00:15:19.800 --> 00:15:19.810 align:start position:0% contracts these are all very valuable 00:15:19.810 --> 00:15:21.270 align:start position:0% contracts these are all very valuable things<00:15:20.290> I<00:15:20.530> don't<00:15:20.680> think<00:15:20.830> I<00:15:20.890> need<00:15:21.040> to<00:15:21.070> talk 00:15:21.270 --> 00:15:21.280 align:start position:0% things I don't think I need to talk 00:15:21.280 --> 00:15:23.220 align:start position:0% things I don't think I need to talk about<00:15:21.430> them<00:15:21.730> pretty<00:15:22.480> obvious<00:15:22.839> how<00:15:22.959> to<00:15:22.990> use 00:15:23.220 --> 00:15:23.230 align:start position:0% about them pretty obvious how to use 00:15:23.230 --> 00:15:24.960 align:start position:0% about them pretty obvious how to use them<00:15:23.440> and<00:15:23.680> I<00:15:23.890> highly<00:15:24.250> suggest<00:15:24.400> you<00:15:24.640> cover<00:15:24.850> all 00:15:24.960 --> 00:15:24.970 align:start position:0% them and I highly suggest you cover all 00:15:24.970 --> 00:15:26.460 align:start position:0% them and I highly suggest you cover all of<00:15:25.120> these<00:15:25.360> bases<00:15:25.420> if<00:15:25.900> you're<00:15:26.020> writing<00:15:26.200> a<00:15:26.350> high 00:15:26.460 --> 00:15:26.470 align:start position:0% of these bases if you're writing a high 00:15:26.470 --> 00:15:29.100 align:start position:0% of these bases if you're writing a high value<00:15:26.800> contract<00:15:27.390> alright<00:15:28.540> so<00:15:28.690> takeaways 00:15:29.100 --> 00:15:29.110 align:start position:0% value contract alright so takeaways 00:15:29.110 --> 00:15:30.780 align:start position:0% value contract alright so takeaways we've<00:15:29.410> got<00:15:29.589> lots<00:15:29.800> of<00:15:29.920> work<00:15:30.040> still<00:15:30.310> to<00:15:30.370> do<00:15:30.550> here 00:15:30.780 --> 00:15:30.790 align:start position:0% we've got lots of work still to do here 00:15:30.790 --> 00:15:32.790 align:start position:0% we've got lots of work still to do here the<00:15:31.120> ecosystem<00:15:31.750> definitely<00:15:32.290> will<00:15:32.440> develop 00:15:32.790 --> 00:15:32.800 align:start position:0% the ecosystem definitely will develop 00:15:32.800 --> 00:15:34.620 align:start position:0% the ecosystem definitely will develop good<00:15:32.950> formal<00:15:33.339> tools<00:15:33.550> we<00:15:34.209> have<00:15:34.330> a<00:15:34.360> number<00:15:34.540> of 00:15:34.620 --> 00:15:34.630 align:start position:0% good formal tools we have a number of 00:15:34.630 --> 00:15:36.660 align:start position:0% good formal tools we have a number of talks<00:15:34.870> on<00:15:35.110> this<00:15:35.260> think<00:15:36.040> about<00:15:36.220> humans<00:15:36.520> in<00:15:36.610> the 00:15:36.660 --> 00:15:36.670 align:start position:0% talks on this think about humans in the 00:15:36.670 --> 00:15:37.980 align:start position:0% talks on this think about humans in the loops<00:15:36.850> when<00:15:37.029> you're<00:15:37.120> writing<00:15:37.300> your<00:15:37.690> smart 00:15:37.980 --> 00:15:37.990 align:start position:0% loops when you're writing your smart 00:15:37.990 --> 00:15:40.230 align:start position:0% loops when you're writing your smart contracts<00:15:38.470> and<00:15:38.770> use<00:15:39.250> bug<00:15:39.490> bounties<00:15:39.880> as<00:15:40.180> a 00:15:40.230 --> 00:15:40.240 align:start position:0% contracts and use bug bounties as a 00:15:40.240 --> 00:15:42.300 align:start position:0% contracts and use bug bounties as a stopgap<00:15:40.600> for<00:15:41.050> verification<00:15:41.709> and<00:15:41.860> incentive 00:15:42.300 --> 00:15:42.310 align:start position:0% stopgap for verification and incentive 00:15:42.310 --> 00:15:43.250 align:start position:0% stopgap for verification and incentive fixes 00:15:43.250 --> 00:15:43.260 align:start position:0% fixes 00:15:43.260 --> 00:15:45.449 align:start position:0% fixes thank<00:15:44.260> you<00:15:44.350> guys<00:15:44.500> for<00:15:44.770> listening<00:15:44.890> and<00:15:45.310> if<00:15:45.430> you 00:15:45.449 --> 00:15:45.459 align:start position:0% thank you guys for listening and if you 00:15:45.459 --> 00:15:46.949 align:start position:0% thank you guys for listening and if you want<00:15:45.670> to<00:15:45.760> interact<00:15:45.910> with<00:15:46.150> us<00:15:46.420> further<00:15:46.570> please 00:15:46.949 --> 00:15:46.959 align:start position:0% want to interact with us further please 00:15:46.959 --> 00:15:48.930 align:start position:0% want to interact with us further please check<00:15:47.200> out<00:15:47.350> our<00:15:47.380> website<00:15:47.829> at<00:15:47.980> India<00:15:48.220> c3<00:15:48.579> org 00:15:48.930 --> 00:15:48.940 align:start position:0% check out our website at India c3 org 00:15:48.940 --> 00:15:50.639 align:start position:0% check out our website at India c3 org check<00:15:49.329> out<00:15:49.450> our<00:15:49.600> publications<00:15:50.230> and<00:15:50.410> we<00:15:50.560> are 00:15:50.639 --> 00:15:50.649 align:start position:0% check out our publications and we are 00:15:50.649 --> 00:15:51.810 align:start position:0% check out our publications and we are always<00:15:50.860> looking<00:15:51.190> for<00:15:51.370> industry 00:15:51.810 --> 00:15:51.820 align:start position:0% always looking for industry 00:15:51.820 --> 00:15:53.879 align:start position:0% always looking for industry collaborations<00:15:52.420> and<00:15:52.570> partners<00:15:52.959> we'd<00:15:53.529> love<00:15:53.740> to 00:15:53.879 --> 00:15:53.889 align:start position:0% collaborations and partners we'd love to 00:15:53.889 --> 00:15:55.410 align:start position:0% collaborations and partners we'd love to work<00:15:54.040> with<00:15:54.070> you<00:15:54.220> to<00:15:54.490> solve<00:15:54.730> the<00:15:54.910> open<00:15:55.180> research 00:15:55.410 --> 00:15:55.420 align:start position:0% work with you to solve the open research 00:15:55.420 --> 00:15:57.990 align:start position:0% work with you to solve the open research problems<00:15:55.899> in<00:15:56.019> the<00:15:56.110> space<00:15:56.519> so<00:15:57.519> definitely 00:15:57.990 --> 00:15:58.000 align:start position:0% problems in the space so definitely 00:15:58.000 --> 00:15:59.759 align:start position:0% problems in the space so definitely contact<00:15:58.180> us<00:15:58.570> or<00:15:58.779> find<00:15:58.990> me<00:15:59.170> somewhere<00:15:59.500> if<00:15:59.649> you 00:15:59.759 --> 00:15:59.769 align:start position:0% contact us or find me somewhere if you 00:15:59.769 --> 00:16:01.290 align:start position:0% contact us or find me somewhere if you have<00:15:59.920> questions<00:16:00.399> about<00:16:00.490> anything<00:16:00.820> I've<00:16:01.060> said 00:16:01.290 --> 00:16:01.300 align:start position:0% have questions about anything I've said 00:16:01.300 --> 00:16:03.710 align:start position:0% have questions about anything I've said here<00:16:01.510> all<00:16:02.380> right<00:16:02.500> thank<00:16:02.769> you<00:16:02.860> very<00:16:02.980> much 00:16:03.710 --> 00:16:03.720 align:start position:0% here all right thank you very much 00:16:03.720 --> 00:16:07.640 align:start position:0% here all right thank you very much [Applause] 00:16:07.640 --> 00:16:07.650 align:start position:0% [Applause] 00:16:07.650 --> 00:16:12.789 align:start position:0% [Applause] [Music]