0 00:00:00,000 --> 00:00:30,000 Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/731 Thanks! 1 00:00:13,320 --> 00:00:15,719 All right, your speakers 2 00:00:15,720 --> 00:00:17,309 are Felix. 3 00:00:17,310 --> 00:00:19,379 He is a student at 4 00:00:19,380 --> 00:00:21,629 the Castro Institute for Technology, 5 00:00:23,310 --> 00:00:25,409 the baseline for a talk, basically 6 00:00:25,410 --> 00:00:28,289 both his bachelor's thesis, which was 7 00:00:28,290 --> 00:00:30,390 actually awarded the. 8 00:00:31,860 --> 00:00:33,499 International Student Award for 9 00:00:33,500 --> 00:00:35,959 Undergraduate Research at the 10 00:00:35,960 --> 00:00:36,960 University of Vienna, 11 00:00:38,150 --> 00:00:40,759 um, we been on stage is 12 00:00:40,760 --> 00:00:42,859 Vladimir Klibanoff, who 13 00:00:42,860 --> 00:00:45,739 supervises teachers and provided 14 00:00:45,740 --> 00:00:46,699 feedback and guidance. 15 00:00:46,700 --> 00:00:49,459 And to help, they also 16 00:00:49,460 --> 00:00:51,679 developed an automated tool 17 00:00:51,680 --> 00:00:53,389 using that framework. 18 00:00:53,390 --> 00:00:55,789 So please welcome them with a 19 00:00:55,790 --> 00:00:56,790 warm round of applause. 20 00:01:05,200 --> 00:01:06,819 Thank you very much. 21 00:01:06,820 --> 00:01:08,649 This work was supported by Karlsruhe 22 00:01:08,650 --> 00:01:10,749 Institute of Technology and also the 23 00:01:10,750 --> 00:01:12,759 German National Research Council. 24 00:01:12,760 --> 00:01:15,319 Under the priority program 25 00:01:15,320 --> 00:01:17,649 are a three research into reliable, 26 00:01:17,650 --> 00:01:19,959 secure software systems. 27 00:01:19,960 --> 00:01:22,149 And sometime ago, we started to ask 28 00:01:22,150 --> 00:01:24,339 ourselves the question, how do we know 29 00:01:24,340 --> 00:01:27,519 that our engines are working properly? 30 00:01:27,520 --> 00:01:29,829 And not soon after we started asking 31 00:01:29,830 --> 00:01:32,229 the question, we actually realized that 32 00:01:32,230 --> 00:01:35,499 the answer is spoiler alert. 33 00:01:35,500 --> 00:01:37,129 We hope they do. 34 00:01:37,130 --> 00:01:38,130 And. 35 00:01:39,520 --> 00:01:41,259 This is an important question. 36 00:01:41,260 --> 00:01:43,629 Does anyone have any idea what this list 37 00:01:43,630 --> 00:01:44,630 represents? 38 00:01:45,250 --> 00:01:47,379 Um, the well, the younger 39 00:01:47,380 --> 00:01:49,029 generation probably does not remember 40 00:01:49,030 --> 00:01:51,099 this event, but the older generation 41 00:01:51,100 --> 00:01:52,959 will know that this is the list of 42 00:01:52,960 --> 00:01:55,269 services that were affected when 43 00:01:55,270 --> 00:01:57,459 Debbie and Miss Page, the open as 44 00:01:57,460 --> 00:01:59,619 parent. And as you can see, this is 45 00:01:59,620 --> 00:02:00,609 almost everything. 46 00:02:00,610 --> 00:02:02,859 So, uh, wonderful example 47 00:02:02,860 --> 00:02:04,449 of a single point of failure here. 48 00:02:05,800 --> 00:02:06,890 And, um. 49 00:02:09,180 --> 00:02:11,369 Well, this was 50 00:02:11,370 --> 00:02:13,889 a really defining moment in 51 00:02:13,890 --> 00:02:16,019 the history of pseudo random 52 00:02:16,020 --> 00:02:17,009 number generation. 53 00:02:17,010 --> 00:02:19,439 This is really great example 54 00:02:19,440 --> 00:02:21,179 of a great story. 55 00:02:21,180 --> 00:02:22,889 We will go a little bit into technical 56 00:02:22,890 --> 00:02:25,109 detail later, but I would encourage 57 00:02:25,110 --> 00:02:27,209 you actually to talk to Google it and 58 00:02:27,210 --> 00:02:29,399 to read the full account of what 59 00:02:29,400 --> 00:02:31,879 happened. This is really thrilling story 60 00:02:31,880 --> 00:02:34,589 of fine Greek tragedy where 61 00:02:34,590 --> 00:02:36,809 technical, human 62 00:02:36,810 --> 00:02:39,839 and organizational factors aligned 63 00:02:39,840 --> 00:02:41,699 to create this perfect storm that 64 00:02:41,700 --> 00:02:44,579 actually caused, um, 65 00:02:44,580 --> 00:02:46,739 well, for two years a back door 66 00:02:46,740 --> 00:02:47,819 in all of these things. 67 00:02:49,460 --> 00:02:51,739 And well, at some point, 68 00:02:51,740 --> 00:02:53,869 it was discovered there was a talk 69 00:02:53,870 --> 00:02:56,029 at the 25th Congress about 70 00:02:56,030 --> 00:02:58,400 that, and then one could ask 71 00:02:59,870 --> 00:03:01,759 ourselves, well, what actually happened 72 00:03:01,760 --> 00:03:02,319 afterward? 73 00:03:02,320 --> 00:03:04,429 So what were the technical measures 74 00:03:04,430 --> 00:03:06,469 taken to prevent reoccurrence of such 75 00:03:06,470 --> 00:03:07,610 incidents in the future? 76 00:03:08,870 --> 00:03:11,389 Well, the 77 00:03:11,390 --> 00:03:13,759 technical consequence of the disaster was 78 00:03:13,760 --> 00:03:15,979 to add these two comments 79 00:03:15,980 --> 00:03:18,349 that you see here. 80 00:03:18,350 --> 00:03:20,539 Um, so what what what happened how 81 00:03:20,540 --> 00:03:22,639 the disaster came to be is that the Deben 82 00:03:22,640 --> 00:03:25,069 maintain due to some 83 00:03:25,070 --> 00:03:27,019 quite reasonable logic, to remove this 84 00:03:27,020 --> 00:03:29,209 particular line in 85 00:03:29,210 --> 00:03:31,879 the code. And essentially, one reinstated 86 00:03:31,880 --> 00:03:33,739 the line and then added the comment to do 87 00:03:33,740 --> 00:03:34,909 not remove this line. 88 00:03:36,800 --> 00:03:39,709 This is a very specific remediation 89 00:03:39,710 --> 00:03:42,579 and this was it. 90 00:03:42,580 --> 00:03:45,379 Um, so 91 00:03:45,380 --> 00:03:47,059 in the end, we will see that one can 92 00:03:47,060 --> 00:03:49,189 actually do better things 93 00:03:49,190 --> 00:03:50,929 to make sure that things are working 94 00:03:50,930 --> 00:03:52,579 correctly, but also that they're good 95 00:03:52,580 --> 00:03:53,479 technical reasons. 96 00:03:53,480 --> 00:03:56,269 High quality assurance is difficult. 97 00:03:56,270 --> 00:03:58,549 But nonetheless, and while we're here 98 00:03:58,550 --> 00:04:00,739 talking about comments, I would 99 00:04:00,740 --> 00:04:03,139 like to show you some more comments 100 00:04:03,140 --> 00:04:05,869 from other implementations 101 00:04:05,870 --> 00:04:07,729 of other hearings just to give you a 102 00:04:07,730 --> 00:04:09,529 feeling of what the state of 103 00:04:09,530 --> 00:04:12,049 implementation is in the wild 104 00:04:12,050 --> 00:04:13,050 and. 105 00:04:14,910 --> 00:04:17,129 These are not some obscure 106 00:04:17,130 --> 00:04:19,289 implementations, these are actually 107 00:04:19,290 --> 00:04:21,479 things that you have on your devices. 108 00:04:21,480 --> 00:04:23,549 This is what we use every day. 109 00:04:23,550 --> 00:04:25,859 And you might be saying, well, 110 00:04:25,860 --> 00:04:26,879 you're not being fair. 111 00:04:26,880 --> 00:04:28,679 You are taking things out of context. 112 00:04:28,680 --> 00:04:29,730 And indeed, 113 00:04:31,050 --> 00:04:32,309 this is in some sense, right. 114 00:04:32,310 --> 00:04:34,169 But I can also tell it's only mildly 115 00:04:34,170 --> 00:04:36,869 unfair and there is not a lot of context 116 00:04:36,870 --> 00:04:37,929 accompanying these things. 117 00:04:37,930 --> 00:04:39,959 And also, they really do transport the 118 00:04:39,960 --> 00:04:41,729 feeling that at least I get when I look 119 00:04:41,730 --> 00:04:42,730 at that code, 120 00:04:44,490 --> 00:04:45,149 for example. 121 00:04:45,150 --> 00:04:47,939 So in one implementation, we read 122 00:04:47,940 --> 00:04:50,189 Hashemites to use the number of binary 123 00:04:50,190 --> 00:04:52,439 taught by computers to use to form a wide 124 00:04:52,440 --> 00:04:54,389 area returning by the next pieds method. 125 00:04:54,390 --> 00:04:55,799 Note that this implementation uses 126 00:04:55,800 --> 00:04:57,209 Moabites and that is defined in the above 127 00:04:57,210 --> 00:04:58,210 specification. 128 00:04:59,820 --> 00:05:00,369 What? 129 00:05:00,370 --> 00:05:02,549 Uh, so 130 00:05:02,550 --> 00:05:04,259 it is it is really difficult to 131 00:05:04,260 --> 00:05:05,669 understand what is going on here. 132 00:05:05,670 --> 00:05:07,469 And to this day I am actually not quite 133 00:05:07,470 --> 00:05:07,709 sure. 134 00:05:07,710 --> 00:05:10,529 I think the author just wanted to say 135 00:05:10,530 --> 00:05:12,959 we define that the Schavan return 136 00:05:12,960 --> 00:05:15,089 to digest of 20 bytes, but 137 00:05:15,090 --> 00:05:16,090 in the end. 138 00:05:17,700 --> 00:05:19,799 The intent of this message 139 00:05:19,800 --> 00:05:20,959 is completely unclear. 140 00:05:22,150 --> 00:05:24,429 And if you more so, here is another 141 00:05:24,430 --> 00:05:26,589 one, put the data into the entropy 142 00:05:26,590 --> 00:05:28,299 at some data from the unknown state 143 00:05:28,300 --> 00:05:30,609 recede, we see 144 00:05:30,610 --> 00:05:32,949 terminology is really difficult 145 00:05:32,950 --> 00:05:34,899 and it is so. 146 00:05:34,900 --> 00:05:36,999 But you have to make 147 00:05:37,000 --> 00:05:39,219 an effort, take 148 00:05:39,220 --> 00:05:41,169 some random data and make more random 149 00:05:41,170 --> 00:05:42,170 looking data from it. 150 00:05:44,800 --> 00:05:46,399 I don't know what it means. 151 00:05:46,400 --> 00:05:47,400 Um. 152 00:05:48,840 --> 00:05:51,089 Yeah, the 153 00:05:51,090 --> 00:05:53,429 only comment at a particular 154 00:05:53,430 --> 00:05:54,430 place in the code. 155 00:05:58,980 --> 00:06:01,109 Yeah, this is this is 156 00:06:01,110 --> 00:06:03,299 the code that has the potential to put 157 00:06:03,300 --> 00:06:05,639 a backdoor into all your applications. 158 00:06:05,640 --> 00:06:07,769 Uh, yeah. 159 00:06:09,360 --> 00:06:11,849 Here is here is another nice 160 00:06:11,850 --> 00:06:12,309 statement. 161 00:06:12,310 --> 00:06:14,309 This is from the end user documentation 162 00:06:14,310 --> 00:06:16,499 of the period. And here one has really 163 00:06:16,500 --> 00:06:18,749 to say, hey, you have end 164 00:06:18,750 --> 00:06:19,739 user documentation. 165 00:06:19,740 --> 00:06:22,139 Great. Really, really fantastic 166 00:06:22,140 --> 00:06:23,279 do this. 167 00:06:23,280 --> 00:06:24,839 But of course, nobody is perfect. 168 00:06:24,840 --> 00:06:26,969 So at a particular function, 169 00:06:26,970 --> 00:06:28,529 it just says be very careful. 170 00:06:28,530 --> 00:06:30,209 Otherwise bad things happen and you have 171 00:06:30,210 --> 00:06:32,639 no idea why 172 00:06:32,640 --> 00:06:34,439 you're supposed to be careful, how you're 173 00:06:34,440 --> 00:06:36,719 supposed to be careful what's going 174 00:06:36,720 --> 00:06:37,509 on. 175 00:06:37,510 --> 00:06:38,510 Um. 176 00:06:40,000 --> 00:06:42,249 To to to make well, to 177 00:06:42,250 --> 00:06:43,449 to make the point a little bit more 178 00:06:43,450 --> 00:06:45,519 precise, so I'm showing this, of 179 00:06:45,520 --> 00:06:47,619 course, to entertain you, but the idea 180 00:06:47,620 --> 00:06:50,019 here is not to blame the developer 181 00:06:50,020 --> 00:06:51,969 and not to say, well, this was a bad 182 00:06:51,970 --> 00:06:52,459 developer. 183 00:06:52,460 --> 00:06:54,489 If it were a better developer, then this 184 00:06:54,490 --> 00:06:55,699 wouldn't be there. 185 00:06:55,700 --> 00:06:57,819 And I will not 186 00:06:57,820 --> 00:07:00,189 make these mistakes, of course. 187 00:07:00,190 --> 00:07:02,170 Now, if you think so, you have it coming. 188 00:07:03,490 --> 00:07:05,859 The point is that there is well, 189 00:07:05,860 --> 00:07:07,719 there is a process and they are actually 190 00:07:07,720 --> 00:07:10,959 natural forces that make 191 00:07:10,960 --> 00:07:12,309 things the way they are today. 192 00:07:12,310 --> 00:07:14,409 And typically things start with some kind 193 00:07:14,410 --> 00:07:16,509 of personal project or 194 00:07:16,510 --> 00:07:18,369 research project, or sometimes it's a 195 00:07:18,370 --> 00:07:20,559 clean room implementation 196 00:07:20,560 --> 00:07:22,629 and well, slowly, Fujiko 197 00:07:22,630 --> 00:07:24,369 down there and then people notice. 198 00:07:24,370 --> 00:07:26,769 And then maybe in the meantime, it ends 199 00:07:26,770 --> 00:07:28,839 up on a bigger project 200 00:07:28,840 --> 00:07:30,549 that is under the auspices of some 201 00:07:30,550 --> 00:07:32,619 respected entity like the Apache 202 00:07:32,620 --> 00:07:35,529 Foundation or Mozilla or something else. 203 00:07:35,530 --> 00:07:37,419 And then in the end of the supply chain, 204 00:07:37,420 --> 00:07:39,819 there is some kind of dealer and inventor 205 00:07:39,820 --> 00:07:41,919 who has a need 206 00:07:41,920 --> 00:07:42,819 for appearing period. 207 00:07:42,820 --> 00:07:44,259 And then they will go and say, oh, 208 00:07:44,260 --> 00:07:45,939 there's this code. 209 00:07:45,940 --> 00:07:48,339 Um, and, uh, it 210 00:07:48,340 --> 00:07:49,449 looks really great. We'll just 211 00:07:49,450 --> 00:07:51,549 incorporate that into our product and we 212 00:07:51,550 --> 00:07:54,639 will not do any further due diligence. 213 00:07:54,640 --> 00:07:55,799 We solve our problem. 214 00:07:55,800 --> 00:07:57,909 Schippert And I think 215 00:07:57,910 --> 00:07:59,799 these guys are actually responsible for 216 00:07:59,800 --> 00:08:02,109 most of the problems that we have. 217 00:08:02,110 --> 00:08:04,359 The vendors who take the open 218 00:08:04,360 --> 00:08:06,729 source code to not put in the effort 219 00:08:06,730 --> 00:08:08,829 and just include it into the product 220 00:08:08,830 --> 00:08:10,659 and ship it up. 221 00:08:10,660 --> 00:08:12,759 So we need to really take care of the 222 00:08:12,760 --> 00:08:14,889 process, which is 223 00:08:14,890 --> 00:08:17,059 putting software on our devices. 224 00:08:17,060 --> 00:08:18,369 I don't really have a better 225 00:08:18,370 --> 00:08:20,529 recommendation here, but let me show 226 00:08:20,530 --> 00:08:21,699 you one more example. 227 00:08:22,850 --> 00:08:25,749 So this is more or less the only comment 228 00:08:25,750 --> 00:08:27,939 attached to critical function of 229 00:08:27,940 --> 00:08:29,529 yet another hearing. 230 00:08:29,530 --> 00:08:31,539 And I can assure you, if you know what's 231 00:08:31,540 --> 00:08:33,908 going on, it makes total sense. 232 00:08:33,909 --> 00:08:36,399 But if you do not know what's going on, 233 00:08:36,400 --> 00:08:38,859 you have no chance to understand it. 234 00:08:38,860 --> 00:08:41,288 Um, so 235 00:08:41,289 --> 00:08:43,178 we need documentation, but we need 236 00:08:43,179 --> 00:08:45,069 actually to write documentation for 237 00:08:45,070 --> 00:08:47,169 people who do not understand what 238 00:08:47,170 --> 00:08:48,399 is going on because otherwise your 239 00:08:48,400 --> 00:08:49,989 documentation is useless. 240 00:08:51,670 --> 00:08:53,769 What we find 241 00:08:53,770 --> 00:08:55,959 works best is if you have something like 242 00:08:55,960 --> 00:08:58,059 a one page design document 243 00:08:58,060 --> 00:09:00,189 where you explain in abstract terms, in 244 00:09:00,190 --> 00:09:02,349 mathematical terms, the design 245 00:09:02,350 --> 00:09:04,389 of your Premji and then you can refine 246 00:09:04,390 --> 00:09:05,649 that into the implementation. 247 00:09:05,650 --> 00:09:08,229 So it's not just sufficient to add some 248 00:09:08,230 --> 00:09:09,879 comments to the functions that you have 249 00:09:09,880 --> 00:09:10,879 in the code. 250 00:09:10,880 --> 00:09:13,059 And but 251 00:09:13,060 --> 00:09:15,249 I should say it is really good that 252 00:09:15,250 --> 00:09:16,869 you have this kind of comment there. 253 00:09:16,870 --> 00:09:18,909 So it's abstracted away from the code. 254 00:09:18,910 --> 00:09:20,979 But you have to phrase it in 255 00:09:20,980 --> 00:09:23,349 a different way. You have to to 256 00:09:23,350 --> 00:09:24,859 target the different audience. 257 00:09:24,860 --> 00:09:27,009 And in this hearing, at least, there 258 00:09:27,010 --> 00:09:29,289 was a link to a scientific paper that 259 00:09:29,290 --> 00:09:31,449 describes kind 260 00:09:31,450 --> 00:09:32,929 of the inspiration for this kind of 261 00:09:32,930 --> 00:09:35,019 schema. And that was 262 00:09:35,020 --> 00:09:36,700 that was that part was really helpful. 263 00:09:39,300 --> 00:09:41,399 Anyway, you hopefully get an 264 00:09:41,400 --> 00:09:43,769 idea that there is a need actually to 265 00:09:43,770 --> 00:09:45,869 to to do something and there is a need to 266 00:09:45,870 --> 00:09:47,669 improve the state of things and there is 267 00:09:47,670 --> 00:09:50,579 a need for quality assurance and 268 00:09:50,580 --> 00:09:52,799 well, what are the options 269 00:09:52,800 --> 00:09:55,229 for quality assurance that we have today? 270 00:09:55,230 --> 00:09:57,479 So here is a top five of things you may 271 00:09:57,480 --> 00:09:58,480 or may not be doing. 272 00:09:59,550 --> 00:10:01,679 And the first one is what one does 273 00:10:01,680 --> 00:10:03,779 with whatever other 274 00:10:03,780 --> 00:10:05,039 software that you have. 275 00:10:05,040 --> 00:10:06,869 You typically have some kind of system 276 00:10:06,870 --> 00:10:08,969 test or maybe even apply 277 00:10:08,970 --> 00:10:11,219 some formal methods to verify that 278 00:10:11,220 --> 00:10:12,629 your software does what you think it 279 00:10:12,630 --> 00:10:13,709 should be doing. 280 00:10:13,710 --> 00:10:16,019 But in this particular case, this 281 00:10:16,020 --> 00:10:18,169 is very difficult almost. 282 00:10:18,170 --> 00:10:19,290 Well, I would say impossible. 283 00:10:21,140 --> 00:10:23,569 We have to say that the specification 284 00:10:23,570 --> 00:10:25,669 of appearing, it's it's a piece 285 00:10:25,670 --> 00:10:27,859 of software that takes a 286 00:10:27,860 --> 00:10:30,049 little piece of random data somewhere 287 00:10:30,050 --> 00:10:32,239 from outside of the system and then 288 00:10:32,240 --> 00:10:34,939 stretches it into a stream of 289 00:10:34,940 --> 00:10:37,729 other data that is indistinguishable 290 00:10:37,730 --> 00:10:40,339 from random to computationally bounded 291 00:10:40,340 --> 00:10:41,719 observer. 292 00:10:41,720 --> 00:10:43,789 So it is actually not a 293 00:10:43,790 --> 00:10:46,219 property of single 294 00:10:46,220 --> 00:10:47,689 output stream. 295 00:10:47,690 --> 00:10:49,939 So you cannot really check 296 00:10:49,940 --> 00:10:51,889 this property by looking at one output 297 00:10:51,890 --> 00:10:52,819 stream that you are having. 298 00:10:52,820 --> 00:10:55,159 You cannot try to test for the particular 299 00:10:55,160 --> 00:10:57,559 stream that actually tells 300 00:10:57,560 --> 00:10:58,729 if this is true or not. 301 00:10:58,730 --> 00:11:00,559 It is a property of all the output 302 00:11:00,560 --> 00:11:02,449 streams that appear and can produce. 303 00:11:02,450 --> 00:11:04,819 So this is really 304 00:11:04,820 --> 00:11:05,820 difficult here. 305 00:11:06,550 --> 00:11:08,659 Um, the thing that one could 306 00:11:08,660 --> 00:11:11,519 be doing is to have. 307 00:11:11,520 --> 00:11:13,889 Unit tests for individual units 308 00:11:13,890 --> 00:11:16,409 that have well-defined functional 309 00:11:16,410 --> 00:11:18,779 behavior, for example, 310 00:11:20,190 --> 00:11:22,109 we know is also from implementations in 311 00:11:22,110 --> 00:11:23,669 the wild, that it is difficult to 312 00:11:23,670 --> 00:11:25,589 implement a circular buffer. 313 00:11:25,590 --> 00:11:27,689 It is indeed surprisingly difficult to 314 00:11:27,690 --> 00:11:29,139 do so correctly. 315 00:11:29,140 --> 00:11:31,149 But of course, no self-respect and C 316 00:11:31,150 --> 00:11:32,519 programing goes and says, I will 317 00:11:32,520 --> 00:11:34,589 implement the data structure and I 318 00:11:34,590 --> 00:11:36,839 will write tests for this data structure 319 00:11:36,840 --> 00:11:39,119 and then I will use this data structure 320 00:11:39,120 --> 00:11:40,079 in my other code. 321 00:11:40,080 --> 00:11:42,299 No, everything is baked into one 322 00:11:42,300 --> 00:11:44,849 monolithic thing because 323 00:11:44,850 --> 00:11:46,829 that's what one doesn't see or because 324 00:11:46,830 --> 00:11:48,179 performance, I don't know. 325 00:11:48,180 --> 00:11:50,249 It doesn't really make 326 00:11:50,250 --> 00:11:52,479 sense. So the recommendation 327 00:11:52,480 --> 00:11:54,569 here is clearly try to make your code 328 00:11:54,570 --> 00:11:56,729 modular, let the compiler take 329 00:11:56,730 --> 00:11:58,649 care of the compiler will in line things. 330 00:11:58,650 --> 00:11:59,659 Don't worry about that. 331 00:11:59,660 --> 00:12:01,799 There will be, if any, 332 00:12:01,800 --> 00:12:03,779 very small performance overhead. 333 00:12:03,780 --> 00:12:06,179 But then you obtain units 334 00:12:06,180 --> 00:12:08,129 with clear functionality and you can test 335 00:12:08,130 --> 00:12:10,049 it and be safe. 336 00:12:10,050 --> 00:12:12,149 And they say don't risk 337 00:12:12,150 --> 00:12:14,129 things then. 338 00:12:15,490 --> 00:12:17,679 Another kind of testing that one sees 339 00:12:17,680 --> 00:12:19,419 from time to time, and also this is 340 00:12:19,420 --> 00:12:21,339 recommended from time to time, is 341 00:12:21,340 --> 00:12:22,809 statistical tests. 342 00:12:22,810 --> 00:12:24,339 There is a whole bunch of them here, a 343 00:12:24,340 --> 00:12:25,449 few examples. 344 00:12:25,450 --> 00:12:27,459 What these do, they look at the 345 00:12:27,460 --> 00:12:30,339 individual output stream 346 00:12:30,340 --> 00:12:32,589 and they try to find bad 347 00:12:32,590 --> 00:12:33,669 smells in the stream. 348 00:12:33,670 --> 00:12:36,069 So if your stream has way more 349 00:12:36,070 --> 00:12:38,019 zeros than once, then this test would 350 00:12:38,020 --> 00:12:39,369 say, oh, this is suspicious, 351 00:12:40,420 --> 00:12:42,609 OK, you can do 352 00:12:42,610 --> 00:12:43,029 that. 353 00:12:43,030 --> 00:12:44,949 But it is not helpful and it is not 354 00:12:44,950 --> 00:12:46,539 helpful for one reason because. 355 00:12:47,790 --> 00:12:50,109 Well, most of the things 356 00:12:50,110 --> 00:12:51,449 we are talking about here are 357 00:12:51,450 --> 00:12:53,819 cryptographically oranges, and that means 358 00:12:53,820 --> 00:12:56,009 on one side that they are intended 359 00:12:56,010 --> 00:12:57,299 to be used for cryptography. 360 00:12:57,300 --> 00:12:58,739 The output is intended to be used for 361 00:12:58,740 --> 00:12:59,669 cryptography. 362 00:12:59,670 --> 00:13:01,319 And on the other side, that they actually 363 00:13:01,320 --> 00:13:03,269 have cryptographic building blocks within 364 00:13:03,270 --> 00:13:05,549 them. And these cryptographic 365 00:13:05,550 --> 00:13:07,409 building blocks have the property that 366 00:13:07,410 --> 00:13:09,539 once you pipe whatever you 367 00:13:09,540 --> 00:13:11,789 have through them, the output 368 00:13:11,790 --> 00:13:14,159 will immediately satisfy 369 00:13:14,160 --> 00:13:15,389 this statistical test. 370 00:13:15,390 --> 00:13:17,879 So your appearance can be as almost 371 00:13:17,880 --> 00:13:19,859 as badly broken as you wish. 372 00:13:19,860 --> 00:13:21,989 It will still pass this test 373 00:13:21,990 --> 00:13:23,549 so it doesn't hurt to do them. 374 00:13:23,550 --> 00:13:25,829 Sometimes regulatory agencies require 375 00:13:25,830 --> 00:13:27,959 them. These are remnants from the days 376 00:13:27,960 --> 00:13:29,879 passed when the pure energy output was 377 00:13:29,880 --> 00:13:32,070 not meant for cryptography, but. 378 00:13:33,130 --> 00:13:34,599 Essentially, this is a waste of your 379 00:13:34,600 --> 00:13:35,860 time, you can skip this step. 380 00:13:37,430 --> 00:13:39,829 On the other hand, what is useful, but 381 00:13:39,830 --> 00:13:41,599 what is also not done enough is 382 00:13:41,600 --> 00:13:42,600 regression testing. 383 00:13:43,640 --> 00:13:45,769 Regression tests are 384 00:13:45,770 --> 00:13:47,929 collections of reference seeds 385 00:13:47,930 --> 00:13:50,119 and reference outputs 386 00:13:50,120 --> 00:13:51,120 and. 387 00:13:51,990 --> 00:13:54,089 By comparing the output of your 388 00:13:54,090 --> 00:13:55,889 implementation with this reference 389 00:13:55,890 --> 00:13:58,169 values, you can at least 390 00:13:58,170 --> 00:14:00,269 be as good or as bad as other 391 00:14:00,270 --> 00:14:02,279 people in particular if you are 392 00:14:02,280 --> 00:14:04,039 implementing. 393 00:14:04,040 --> 00:14:06,289 Uh, this particular appearing standard, 394 00:14:06,290 --> 00:14:08,329 which not many people do, but what some 395 00:14:08,330 --> 00:14:10,789 do you have this reference values 396 00:14:10,790 --> 00:14:12,799 in the standard and so you can be as good 397 00:14:12,800 --> 00:14:14,869 or as bad as the standard and 398 00:14:14,870 --> 00:14:16,699 you can hope that more people have looked 399 00:14:16,700 --> 00:14:18,319 at the standard. 400 00:14:18,320 --> 00:14:20,419 So also, if 401 00:14:20,420 --> 00:14:22,579 you change something, if 402 00:14:22,580 --> 00:14:25,099 you do maintenance and it is 403 00:14:25,100 --> 00:14:26,989 not supposed to change the outcome, then 404 00:14:26,990 --> 00:14:28,879 at least you can be sure that you didn't 405 00:14:28,880 --> 00:14:31,219 change something that you didn't want to. 406 00:14:31,220 --> 00:14:32,809 So do regression tests. 407 00:14:32,810 --> 00:14:34,219 This is really helpful. 408 00:14:34,220 --> 00:14:35,220 Not done enough. 409 00:14:36,230 --> 00:14:37,230 Well, almost. 410 00:14:39,850 --> 00:14:42,129 Almost the only thing that we see 411 00:14:42,130 --> 00:14:44,019 for many, many implementation, this is 412 00:14:44,020 --> 00:14:46,209 really the only thing that 413 00:14:46,210 --> 00:14:47,979 stands between you and the disaster. 414 00:14:47,980 --> 00:14:49,419 This is the manual code review. 415 00:14:49,420 --> 00:14:51,039 So people are just looking at the code 416 00:14:51,040 --> 00:14:53,109 and say, OK, it looks fine 417 00:14:53,110 --> 00:14:54,699 and think about it. 418 00:14:54,700 --> 00:14:57,099 Would you accept such a situation 419 00:14:57,100 --> 00:15:00,099 for any other piece of software? 420 00:15:00,100 --> 00:15:03,549 Doesn't matter. How unimportant 421 00:15:03,550 --> 00:15:04,659 would you feel? 422 00:15:04,660 --> 00:15:06,729 Fine. If I told you this piece of 423 00:15:06,730 --> 00:15:08,739 software was never tested. 424 00:15:08,740 --> 00:15:10,299 We looked at it. We think it's fine. 425 00:15:10,300 --> 00:15:11,459 But we never tested. 426 00:15:11,460 --> 00:15:13,699 We never did any quality assurance, 427 00:15:13,700 --> 00:15:15,279 any technical quality assurance. 428 00:15:15,280 --> 00:15:17,259 Would you accept that situation? 429 00:15:17,260 --> 00:15:18,729 This is what you have at the center of 430 00:15:18,730 --> 00:15:20,009 your security infrastructure. 431 00:15:21,390 --> 00:15:23,399 Um, so. 432 00:15:26,220 --> 00:15:28,349 We do not have bad news, but we also 433 00:15:28,350 --> 00:15:30,899 try to improve things a little bit, and 434 00:15:30,900 --> 00:15:32,699 here we did two things. 435 00:15:32,700 --> 00:15:34,769 First, we looked at many, 436 00:15:34,770 --> 00:15:37,199 many incidents with springs that 437 00:15:37,200 --> 00:15:39,329 occurred previously, and we 438 00:15:39,330 --> 00:15:41,459 identified a particular property that 439 00:15:41,460 --> 00:15:43,319 has been violated in many of these 440 00:15:43,320 --> 00:15:44,579 incidents. 441 00:15:44,580 --> 00:15:46,889 And on top of that, we also 442 00:15:46,890 --> 00:15:48,929 developed a tool, we developed a method, 443 00:15:48,930 --> 00:15:51,479 a particular specialized static analysis 444 00:15:52,800 --> 00:15:54,929 that will find violations of this 445 00:15:54,930 --> 00:15:57,239 property in your implementations, 446 00:15:57,240 --> 00:15:59,369 in real world implementations, 447 00:15:59,370 --> 00:16:01,439 open SSL and the like. 448 00:16:01,440 --> 00:16:03,719 And in this talk, we will try to 449 00:16:03,720 --> 00:16:06,029 explain what the property is, what 450 00:16:06,030 --> 00:16:07,829 the tool does, and what was the result of 451 00:16:07,830 --> 00:16:11,389 applying it actually to implementations. 452 00:16:11,390 --> 00:16:12,720 But first, I need to. 453 00:16:14,000 --> 00:16:16,459 Explain a little bit 454 00:16:16,460 --> 00:16:19,159 how a typical parent works, 455 00:16:19,160 --> 00:16:21,439 and this is a very simplified model 456 00:16:21,440 --> 00:16:23,539 in practice, of course, things 457 00:16:23,540 --> 00:16:25,909 are more complicated, but nonetheless, 458 00:16:25,910 --> 00:16:28,009 in the middle you have, 459 00:16:28,010 --> 00:16:30,199 um, some kind of state sometimes 460 00:16:30,200 --> 00:16:32,419 called entropy pool. But this 461 00:16:32,420 --> 00:16:34,219 is this just the state of entropy is 462 00:16:34,220 --> 00:16:35,149 collected. 463 00:16:35,150 --> 00:16:37,069 And then there is a seating function that 464 00:16:37,070 --> 00:16:39,409 takes this little piece of 465 00:16:39,410 --> 00:16:41,539 random seed that is. 466 00:16:42,800 --> 00:16:44,929 Has its origins somewhere outside of 467 00:16:44,930 --> 00:16:47,299 the system. Typically, you ask the 468 00:16:47,300 --> 00:16:49,069 operating system for it in the operating 469 00:16:49,070 --> 00:16:51,349 system, will also typically derive 470 00:16:51,350 --> 00:16:53,539 it from hardware, from 471 00:16:53,540 --> 00:16:55,879 disk latency, from timing 472 00:16:55,880 --> 00:16:57,919 of your keystrokes, from interrupt timing 473 00:16:57,920 --> 00:16:58,920 and so on. 474 00:16:59,480 --> 00:17:01,999 So then you obtain this 475 00:17:02,000 --> 00:17:04,039 kind of very short about 20 bytes, 476 00:17:04,040 --> 00:17:06,649 typical value of 477 00:17:06,650 --> 00:17:08,929 random speed and you transfer 478 00:17:08,930 --> 00:17:11,419 it into your state and the 479 00:17:11,420 --> 00:17:13,519 rest of operation goes in cycles. 480 00:17:13,520 --> 00:17:15,618 And in every cycle you somehow 481 00:17:15,619 --> 00:17:17,749 perturb this internal state 482 00:17:17,750 --> 00:17:19,818 and then you derive a little chunk of 483 00:17:19,819 --> 00:17:22,429 output from the state 484 00:17:22,430 --> 00:17:23,939 and then the next cycle begins. 485 00:17:23,940 --> 00:17:25,789 So you perturb the state again and derive 486 00:17:25,790 --> 00:17:27,318 the next chunk and so on and so forth. 487 00:17:27,319 --> 00:17:28,369 And then you obtain a stream 488 00:17:30,320 --> 00:17:31,320 in the model. 489 00:17:32,990 --> 00:17:35,449 All of these things that you see here 490 00:17:35,450 --> 00:17:36,450 deterministic. 491 00:17:37,680 --> 00:17:39,779 So all of this 492 00:17:39,780 --> 00:17:41,789 procedure is completely deterministic and 493 00:17:41,790 --> 00:17:43,949 the only source of randomness, 494 00:17:43,950 --> 00:17:46,199 the only source of natural determinism is 495 00:17:46,200 --> 00:17:48,389 actually the choice of the seed. 496 00:17:48,390 --> 00:17:50,489 So we will go ahead and we will 497 00:17:50,490 --> 00:17:52,559 actually treat this 498 00:17:52,560 --> 00:17:55,139 whole cascade as a function 499 00:17:55,140 --> 00:17:57,419 from an MBA seed to and 500 00:17:57,420 --> 00:17:59,459 end with prefix of the output stream 501 00:17:59,460 --> 00:18:00,479 genes for generator. 502 00:18:00,480 --> 00:18:02,159 And you will see the symbol from time to 503 00:18:02,160 --> 00:18:03,160 time during the talk. 504 00:18:04,200 --> 00:18:06,030 This is what we are concerned with. 505 00:18:07,100 --> 00:18:08,100 And 506 00:18:09,920 --> 00:18:10,920 before. 507 00:18:11,960 --> 00:18:13,999 I explained the problem that we actually 508 00:18:14,000 --> 00:18:16,459 solve. I would also like to 509 00:18:16,460 --> 00:18:18,199 make clear that there are a lot of 510 00:18:18,200 --> 00:18:20,419 problems that we do not solve and it is 511 00:18:20,420 --> 00:18:23,029 important to name some of them. 512 00:18:23,030 --> 00:18:25,339 So first problem that we do not take care 513 00:18:25,340 --> 00:18:28,129 of is the choice of the city. 514 00:18:28,130 --> 00:18:30,259 This is a difficult problem, but it 515 00:18:30,260 --> 00:18:32,239 is completely orthogonal to making sure 516 00:18:32,240 --> 00:18:34,909 that this procedure is working correctly. 517 00:18:34,910 --> 00:18:36,800 And there was a talk about 518 00:18:38,990 --> 00:18:40,309 seat selection yesterday. 519 00:18:41,390 --> 00:18:42,799 And, uh, well, 520 00:18:44,270 --> 00:18:45,979 there are also popular mistakes then you 521 00:18:45,980 --> 00:18:47,959 can have in the choice of the seat. 522 00:18:47,960 --> 00:18:50,209 For example, if you ever seat 523 00:18:50,210 --> 00:18:52,459 with something related to time, 524 00:18:52,460 --> 00:18:54,629 you will have a bad time. 525 00:18:54,630 --> 00:18:56,689 Um, yeah, 526 00:18:56,690 --> 00:18:59,659 for reasons first, because the 527 00:18:59,660 --> 00:19:01,699 typically the resolution of the time is 528 00:19:01,700 --> 00:19:03,559 not large enough. So your seat will have 529 00:19:03,560 --> 00:19:06,049 a small range and also because 530 00:19:06,050 --> 00:19:08,149 time is often a 531 00:19:08,150 --> 00:19:10,619 publicly known entity. 532 00:19:10,620 --> 00:19:12,830 So the attacker might actually know. 533 00:19:14,090 --> 00:19:16,459 And now know the seed and then 534 00:19:16,460 --> 00:19:18,589 all the construction collapses, and by 535 00:19:18,590 --> 00:19:20,269 the way, if you are doing this in the 536 00:19:20,270 --> 00:19:22,429 embedded world, then I'm really sorry. 537 00:19:22,430 --> 00:19:24,769 You have very few options to 538 00:19:24,770 --> 00:19:25,939 get good seats. 539 00:19:25,940 --> 00:19:28,039 But again, luckily 540 00:19:28,040 --> 00:19:29,569 not our problem. 541 00:19:29,570 --> 00:19:31,729 Um, the other thing 542 00:19:31,730 --> 00:19:32,899 we are not considering is. 543 00:19:34,860 --> 00:19:36,599 Typically, all of these functions that 544 00:19:36,600 --> 00:19:38,459 you have seen will contain cryptographic 545 00:19:38,460 --> 00:19:40,859 building blocks and here 546 00:19:40,860 --> 00:19:43,259 we assume that these blocks are there. 547 00:19:43,260 --> 00:19:45,089 We can actually check if they're there, 548 00:19:45,090 --> 00:19:47,159 but for the time 549 00:19:47,160 --> 00:19:48,689 being, we'll just assume that they are 550 00:19:48,690 --> 00:19:50,789 there. And also we will assume that 551 00:19:50,790 --> 00:19:53,219 they are really one way, in 552 00:19:53,220 --> 00:19:55,140 particular colloquial sense. 553 00:19:56,520 --> 00:19:59,069 There has been only one incident, the 554 00:19:59,070 --> 00:20:02,129 dual elliptic curve generator. 555 00:20:02,130 --> 00:20:04,289 Also quite thrilling story. 556 00:20:04,290 --> 00:20:06,209 You can you can Google that where it 557 00:20:06,210 --> 00:20:08,399 turned out that these 558 00:20:08,400 --> 00:20:10,199 functions were not one way for everybody, 559 00:20:10,200 --> 00:20:12,359 but they were not one way for 560 00:20:12,360 --> 00:20:13,409 the NSA. 561 00:20:13,410 --> 00:20:16,079 But, uh, yeah, 562 00:20:16,080 --> 00:20:17,609 but that's that's a completely different 563 00:20:17,610 --> 00:20:19,439 thing. And another thing we do to take 564 00:20:19,440 --> 00:20:21,779 care of, uh, is we don't take care 565 00:20:21,780 --> 00:20:23,579 of very powerful attackers. 566 00:20:23,580 --> 00:20:25,589 So here we assume that the attacker knows 567 00:20:25,590 --> 00:20:27,749 the code of appearance, but they do 568 00:20:27,750 --> 00:20:29,729 not know the seed and they do not know 569 00:20:29,730 --> 00:20:31,409 the internal state. 570 00:20:31,410 --> 00:20:33,719 If you have an attacker that knows 571 00:20:33,720 --> 00:20:35,789 some of these things, you're 572 00:20:35,790 --> 00:20:36,389 on your own. 573 00:20:36,390 --> 00:20:38,439 If a three letter agency is standing with 574 00:20:38,440 --> 00:20:39,839 the tempest when in front of your 575 00:20:39,840 --> 00:20:42,599 building, sorry, we cannot help you. 576 00:20:42,600 --> 00:20:45,569 Um, but we cannot 577 00:20:45,570 --> 00:20:47,669 we can help you detect entropy 578 00:20:47,670 --> 00:20:49,979 loss in your implementation and entropy 579 00:20:49,980 --> 00:20:52,679 loss. There are several different ways to 580 00:20:52,680 --> 00:20:54,839 define entropy loss. 581 00:20:54,840 --> 00:20:57,509 So all of the following are equivalent. 582 00:20:57,510 --> 00:20:59,729 For example, if you have 583 00:20:59,730 --> 00:21:01,889 two seeds that produce the same 584 00:21:01,890 --> 00:21:03,459 output stream, this is entropy loss. 585 00:21:03,460 --> 00:21:04,949 So there is a collision and European 586 00:21:04,950 --> 00:21:05,849 energy. 587 00:21:05,850 --> 00:21:08,069 And this is equivalent to the fact that 588 00:21:08,070 --> 00:21:09,569 part of your see, this is where the 589 00:21:09,570 --> 00:21:11,609 collision will be is not used for the 590 00:21:11,610 --> 00:21:13,799 output. It also means that there are 591 00:21:13,800 --> 00:21:15,659 fewer possible outputs than you have 592 00:21:15,660 --> 00:21:17,069 seeds. And here you already get the 593 00:21:17,070 --> 00:21:18,759 intuition why this is bad. 594 00:21:18,760 --> 00:21:21,479 So you are wasting some of the entropy 595 00:21:21,480 --> 00:21:24,239 you have collected in your seed and 596 00:21:24,240 --> 00:21:26,099 probably you are wasting quite a lot of 597 00:21:26,100 --> 00:21:26,279 it. 598 00:21:26,280 --> 00:21:28,349 And then your seed, your output will 599 00:21:28,350 --> 00:21:30,599 be much more predictable than 600 00:21:30,600 --> 00:21:32,079 the seed. And this is bad. 601 00:21:32,080 --> 00:21:34,049 We do not want this mathematically. 602 00:21:34,050 --> 00:21:36,119 It all boils boils down that you have 603 00:21:36,120 --> 00:21:38,279 a problem if the function G is not an 604 00:21:38,280 --> 00:21:40,349 objective, this is 605 00:21:40,350 --> 00:21:41,339 what we will be looking for. 606 00:21:41,340 --> 00:21:43,949 So we have a whole machinery 607 00:21:43,950 --> 00:21:46,079 to check if functions are in 608 00:21:46,080 --> 00:21:47,469 a.. 609 00:21:47,470 --> 00:21:48,789 Security, by the way, that's an 610 00:21:48,790 --> 00:21:50,469 interesting observation, is often about 611 00:21:50,470 --> 00:21:52,329 injectivity, it's it's either about 612 00:21:52,330 --> 00:21:54,279 injectivity or not injectivity, but many 613 00:21:54,280 --> 00:21:56,139 things like privacy and integrity and so 614 00:21:56,140 --> 00:21:58,149 on can be defined in these terms 615 00:21:58,150 --> 00:21:59,150 mathematically. 616 00:22:01,060 --> 00:22:03,339 Just quickly, this is just a mathematical 617 00:22:03,340 --> 00:22:05,499 formal definition of 618 00:22:05,500 --> 00:22:07,089 injectivity of the function. 619 00:22:07,090 --> 00:22:08,769 And this is indeed what our tool will be 620 00:22:08,770 --> 00:22:10,869 checking. But now 621 00:22:10,870 --> 00:22:13,239 we'll show you examples of entropy 622 00:22:13,240 --> 00:22:15,009 also that you get a better intuition. 623 00:22:19,660 --> 00:22:21,759 So that's first come back 624 00:22:21,760 --> 00:22:23,859 to what happened in 625 00:22:23,860 --> 00:22:26,709 the division of SSL disaster. 626 00:22:26,710 --> 00:22:29,709 So this is this is the model that 627 00:22:29,710 --> 00:22:32,969 we slightly adopted for the transparency. 628 00:22:32,970 --> 00:22:35,799 We adopted it the way that we have here 629 00:22:35,800 --> 00:22:38,169 in the mixed function edition 630 00:22:38,170 --> 00:22:39,099 to edit the PID. 631 00:22:39,100 --> 00:22:41,769 So the SSL PMG 632 00:22:41,770 --> 00:22:43,779 does not only take the seat as a random 633 00:22:43,780 --> 00:22:46,149 input, but it also takes 634 00:22:46,150 --> 00:22:48,519 the process idea of your process as 635 00:22:48,520 --> 00:22:50,769 random input used in 636 00:22:50,770 --> 00:22:53,199 the mix function to perturb 637 00:22:53,200 --> 00:22:55,329 the state and then derive 638 00:22:55,330 --> 00:22:56,330 output. 639 00:22:56,800 --> 00:22:58,389 So then what happened? 640 00:22:58,390 --> 00:23:00,640 That line was removed and yeah, 641 00:23:01,810 --> 00:23:02,939 the seed was cut off. 642 00:23:05,600 --> 00:23:07,959 Badly, they had the video 643 00:23:07,960 --> 00:23:10,539 here contained in the mixed function, so 644 00:23:10,540 --> 00:23:12,639 the stage, the output of the energy was 645 00:23:12,640 --> 00:23:14,309 still random. Looking out, if you have a 646 00:23:14,310 --> 00:23:16,959 punji and get all this the same key 647 00:23:16,960 --> 00:23:18,849 somewhere, someone would have noticed 648 00:23:18,850 --> 00:23:19,569 that. 649 00:23:19,570 --> 00:23:21,639 But this way it was 650 00:23:21,640 --> 00:23:24,309 not wonky, but thirty 651 00:23:24,310 --> 00:23:25,779 two thousand keys. 652 00:23:27,070 --> 00:23:29,259 So it was not easy to 653 00:23:29,260 --> 00:23:30,260 notice that. 654 00:23:31,750 --> 00:23:33,579 And as you can see, that's that's an easy 655 00:23:33,580 --> 00:23:34,609 instance of entropy. 656 00:23:34,610 --> 00:23:36,879 So you're not using part of the CJA, 657 00:23:36,880 --> 00:23:39,819 you're not using anything of the seed. 658 00:23:39,820 --> 00:23:42,129 And what we can learn from here is you 659 00:23:42,130 --> 00:23:44,439 should separate your energy out, take 660 00:23:44,440 --> 00:23:46,509 the random data at 661 00:23:46,510 --> 00:23:48,609 one place, use it in some 662 00:23:48,610 --> 00:23:50,919 way, but not at random data 663 00:23:50,920 --> 00:23:53,049 at different points in your code, 664 00:23:54,160 --> 00:23:56,409 but also help us later when we talk 665 00:23:56,410 --> 00:23:58,509 about how we verify that 666 00:23:58,510 --> 00:24:00,399 the code works correctly and does not 667 00:24:00,400 --> 00:24:02,049 lose any of your entropy. 668 00:24:03,900 --> 00:24:05,789 Another prominent example is what 669 00:24:05,790 --> 00:24:07,589 happened in the Android pseudo random 670 00:24:07,590 --> 00:24:09,809 number generator, so this 671 00:24:09,810 --> 00:24:12,959 is a large Java Intertrade 672 00:24:12,960 --> 00:24:14,520 that's used in that period. 673 00:24:15,600 --> 00:24:17,729 It's called seed, but the seed is 674 00:24:17,730 --> 00:24:18,730 only here. 675 00:24:20,660 --> 00:24:22,579 Generally, it's the whole internal state 676 00:24:22,580 --> 00:24:23,569 of the P.A. 677 00:24:23,570 --> 00:24:25,639 and the seat should be 678 00:24:25,640 --> 00:24:27,859 written from Java interests 679 00:24:27,860 --> 00:24:30,679 zero to drama and such as for yeah that 680 00:24:30,680 --> 00:24:33,079 would be five Java Indigenous feet. 681 00:24:33,080 --> 00:24:35,289 That's good for 682 00:24:35,290 --> 00:24:37,729 a good number of output streams to not 683 00:24:37,730 --> 00:24:38,730 be able to. 684 00:24:39,680 --> 00:24:41,899 Do attacks, but what accidentally 685 00:24:41,900 --> 00:24:43,999 happened? Yeah, they would want to 686 00:24:44,000 --> 00:24:46,249 try the counter and the padding here 687 00:24:46,250 --> 00:24:48,349 afterwards, but what they 688 00:24:48,350 --> 00:24:50,509 did is they did not update the 689 00:24:50,510 --> 00:24:52,219 pointer, so they wrote the counter and 690 00:24:52,220 --> 00:24:54,529 the padding here overriding more 691 00:24:54,530 --> 00:24:55,599 than half of the seats. 692 00:24:55,600 --> 00:24:58,219 So what was left were two Java integers. 693 00:24:58,220 --> 00:25:01,459 Sixty four. But that's not much 694 00:25:01,460 --> 00:25:04,009 that's more than what was left 695 00:25:04,010 --> 00:25:06,109 with Davian. Yeah, but it's 696 00:25:06,110 --> 00:25:07,699 you see more than the half is gone. 697 00:25:07,700 --> 00:25:09,949 So that's a clear example 698 00:25:09,950 --> 00:25:12,679 that you cannot detect such issues 699 00:25:12,680 --> 00:25:15,589 when looking at the output and looking at 700 00:25:15,590 --> 00:25:17,299 how the PMG works. 701 00:25:18,590 --> 00:25:20,689 And the nadelberg that's the one that 702 00:25:20,690 --> 00:25:23,299 we detected was like Decrypt. 703 00:25:23,300 --> 00:25:25,609 And we'll discuss that in greater 704 00:25:25,610 --> 00:25:26,610 detail later. 705 00:25:27,880 --> 00:25:29,259 So what do we do to analyze, 706 00:25:30,860 --> 00:25:33,009 first of all, the user has to take that 707 00:25:33,010 --> 00:25:34,779 the user of our tool use that wants to 708 00:25:34,780 --> 00:25:36,639 analyze has to take the pinchy and 709 00:25:36,640 --> 00:25:38,499 isolate the currently isolated, 710 00:25:38,500 --> 00:25:40,959 deterministic part, remove other 711 00:25:40,960 --> 00:25:43,329 all other entropy sources 712 00:25:43,330 --> 00:25:45,549 that are not directly the seed 713 00:25:45,550 --> 00:25:47,529 so that the tool can check that the whole 714 00:25:47,530 --> 00:25:49,629 random data from the seed is included in 715 00:25:49,630 --> 00:25:50,630 the output. 716 00:25:51,730 --> 00:25:53,829 Then it has to choose a scope 717 00:25:53,830 --> 00:25:54,969 which we want to analyze. 718 00:25:54,970 --> 00:25:57,759 So we have to define a fixed length 719 00:25:57,760 --> 00:25:59,709 of input and output length that we want 720 00:25:59,710 --> 00:26:00,720 to check injectivity. 721 00:26:01,810 --> 00:26:03,939 So, yeah, 722 00:26:03,940 --> 00:26:06,339 typically we we do that and just 723 00:26:06,340 --> 00:26:07,419 take one cycle. 724 00:26:09,470 --> 00:26:11,599 Then the user needs to 725 00:26:11,600 --> 00:26:13,579 find a way around the crypto functions 726 00:26:13,580 --> 00:26:15,679 because the crypto functions are 727 00:26:15,680 --> 00:26:17,359 essentially hard to be proven 728 00:26:17,360 --> 00:26:19,429 ineffective. That's the whole point 729 00:26:19,430 --> 00:26:21,139 of the crypto functions. 730 00:26:21,140 --> 00:26:23,359 So we need to circumvent 731 00:26:23,360 --> 00:26:25,519 that in a way that our Trouville can 732 00:26:25,520 --> 00:26:28,279 prove around those crypto functions that 733 00:26:28,280 --> 00:26:30,439 the rest of the code does its job 734 00:26:30,440 --> 00:26:31,440 correctly. 735 00:26:32,300 --> 00:26:34,339 And then our tool comes into play, 736 00:26:34,340 --> 00:26:36,619 generates the condition 737 00:26:36,620 --> 00:26:38,089 it generates the condition that we 738 00:26:38,090 --> 00:26:40,249 described earlier and verifies that this 739 00:26:40,250 --> 00:26:41,889 condition is true. 740 00:26:41,890 --> 00:26:44,139 And finally, the weekend 741 00:26:44,140 --> 00:26:46,299 results. Is there a yes 742 00:26:46,300 --> 00:26:47,619 or no? 743 00:26:47,620 --> 00:26:50,409 And I would like to show you that in 744 00:26:50,410 --> 00:26:52,599 short now so. 745 00:26:56,280 --> 00:26:58,379 What's here, that's the that's 746 00:26:58,380 --> 00:27:00,569 part of the open here, and 747 00:27:00,570 --> 00:27:02,909 that's the function that would add random 748 00:27:02,910 --> 00:27:05,409 data to the appearance's internal state. 749 00:27:05,410 --> 00:27:07,289 Now, that's the seed arrow. 750 00:27:09,150 --> 00:27:11,339 Pillow comes the part where where 751 00:27:11,340 --> 00:27:13,409 where something was moved and what 752 00:27:13,410 --> 00:27:15,509 you want to do now is we just want to 753 00:27:15,510 --> 00:27:17,609 introduce a simple problem that I 754 00:27:17,610 --> 00:27:18,569 have here. 755 00:27:18,570 --> 00:27:21,119 The problem kills one bit 756 00:27:21,120 --> 00:27:23,399 in the input, so we will not 757 00:27:23,400 --> 00:27:25,349 use one bit of the input. 758 00:27:29,300 --> 00:27:31,400 And now I will run the analysis. 759 00:27:39,250 --> 00:27:41,749 And the analysis will now translate to 760 00:27:41,750 --> 00:27:43,839 the program of 761 00:27:43,840 --> 00:27:45,969 energy into a logical formula, 762 00:27:45,970 --> 00:27:48,309 a formula describing what the 763 00:27:48,310 --> 00:27:49,329 G actually does. 764 00:27:51,170 --> 00:27:53,659 Then our tool comes into play, 765 00:27:53,660 --> 00:27:55,669 duplicates the formula and specifies the 766 00:27:55,670 --> 00:27:57,349 condition that we will to have two 767 00:27:57,350 --> 00:27:59,629 different inputs and when applying 768 00:27:59,630 --> 00:28:01,789 this function, this will result 769 00:28:01,790 --> 00:28:03,439 in the same output. 770 00:28:03,440 --> 00:28:05,869 And finally, we have here 771 00:28:05,870 --> 00:28:08,059 solver for such a formulas 772 00:28:08,060 --> 00:28:10,099 and the formula that the solve quickly 773 00:28:10,100 --> 00:28:12,169 said, yeah, we have a we have 774 00:28:12,170 --> 00:28:13,219 a solution here. 775 00:28:13,220 --> 00:28:15,229 And the solution is giving those two 776 00:28:15,230 --> 00:28:16,319 inputs. 777 00:28:16,320 --> 00:28:18,739 We receive these same outputs. 778 00:28:18,740 --> 00:28:20,959 So now you have to check 779 00:28:20,960 --> 00:28:21,919 what's wrong. 780 00:28:21,920 --> 00:28:24,139 Oh, oh. Here, here's exactly one 781 00:28:24,140 --> 00:28:25,339 bit wrong. 782 00:28:25,340 --> 00:28:27,169 Why is the Punji not using this bit? 783 00:28:28,530 --> 00:28:31,469 So in the end, you would probably 784 00:28:31,470 --> 00:28:34,019 want to debunk that and hopefully 785 00:28:34,020 --> 00:28:35,879 stumble across the instruction that we 786 00:28:35,880 --> 00:28:37,319 edit here. 787 00:28:37,320 --> 00:28:38,369 And remove that again, 788 00:28:39,480 --> 00:28:41,369 and then you can run the analysis again 789 00:28:41,370 --> 00:28:43,769 and again, the whole program 790 00:28:43,770 --> 00:28:45,659 gets now translated into a logical 791 00:28:45,660 --> 00:28:46,660 formula. 792 00:28:47,680 --> 00:28:49,889 That that takes its time, so that's 793 00:28:49,890 --> 00:28:52,389 a 30 megabyte of logical formula, 794 00:28:52,390 --> 00:28:54,640 then we double that size 795 00:28:56,110 --> 00:28:57,909 because we want to have two invocations 796 00:28:57,910 --> 00:28:59,859 of the program, which have different 797 00:28:59,860 --> 00:29:02,399 inputs resulting in the same outputs. 798 00:29:02,400 --> 00:29:03,849 And finally. 799 00:29:05,380 --> 00:29:08,049 Yeah, the the solar cell 800 00:29:08,050 --> 00:29:10,829 shows, yeah, we have we have no example. 801 00:29:10,830 --> 00:29:13,439 There's no example where this function 802 00:29:13,440 --> 00:29:14,569 loses random data. 803 00:29:16,710 --> 00:29:18,959 So how can we deal 804 00:29:18,960 --> 00:29:20,849 with this cryptographic functions, that's 805 00:29:20,850 --> 00:29:23,009 the part that I skipped and Vladimir will 806 00:29:23,010 --> 00:29:25,199 now take over to 807 00:29:25,200 --> 00:29:26,849 explain to you how we do that. 808 00:29:29,560 --> 00:29:31,739 Um, yeah, so this is the bit that we 809 00:29:31,740 --> 00:29:33,689 have conveniently swept under the rug so 810 00:29:33,690 --> 00:29:34,690 far. 811 00:29:35,910 --> 00:29:37,529 I will show you an example. 812 00:29:37,530 --> 00:29:39,539 So the thing that you see at the top, 813 00:29:39,540 --> 00:29:41,939 this is one invocation 814 00:29:41,940 --> 00:29:44,189 of the shower, one that 815 00:29:44,190 --> 00:29:46,409 is part of the seed. 816 00:29:46,410 --> 00:29:48,299 Um, the function of the openness is 817 00:29:48,300 --> 00:29:50,369 healthier and that takes the 818 00:29:50,370 --> 00:29:52,739 seed somewhere from outside and transfers 819 00:29:52,740 --> 00:29:54,079 it into the internal state. 820 00:29:55,080 --> 00:29:57,209 And what you see here is a concatenation 821 00:29:57,210 --> 00:29:59,009 of one, two, three, four different 822 00:29:59,010 --> 00:30:00,010 things. 823 00:30:00,720 --> 00:30:01,720 And. 824 00:30:02,440 --> 00:30:04,389 I can tell you that on the first 825 00:30:04,390 --> 00:30:06,849 invocation, only the 826 00:30:06,850 --> 00:30:09,519 third parameter here, only the buff, 827 00:30:09,520 --> 00:30:11,289 this is the actually the parameter to the 828 00:30:11,290 --> 00:30:13,509 function will contain entropy 829 00:30:13,510 --> 00:30:15,759 and all the other 830 00:30:15,760 --> 00:30:18,489 parameters have fixed values. 831 00:30:18,490 --> 00:30:21,159 And altogether, this is 832 00:30:21,160 --> 00:30:23,439 sixty eight, I think, bytes 833 00:30:23,440 --> 00:30:25,629 long. And the short on cash 834 00:30:25,630 --> 00:30:28,109 will derive a 20 byte, 835 00:30:28,110 --> 00:30:29,559 uh, digest from that. 836 00:30:29,560 --> 00:30:31,629 And the cryptographers promise 837 00:30:31,630 --> 00:30:33,759 us that, well 838 00:30:33,760 --> 00:30:35,859 if the 839 00:30:35,860 --> 00:30:38,139 input has more than 840 00:30:38,140 --> 00:30:40,719 well at least two to the power of 160 841 00:30:40,720 --> 00:30:43,059 different values, then we will see 842 00:30:43,060 --> 00:30:45,159 at least two to the power of 106, the 843 00:30:45,160 --> 00:30:46,929 different outputs. 844 00:30:46,930 --> 00:30:47,930 This is what we hope for. 845 00:30:49,060 --> 00:30:51,879 But again, as I said, we cannot 846 00:30:51,880 --> 00:30:54,009 really check for injectivity of 847 00:30:54,010 --> 00:30:56,439 this call of this function 848 00:30:56,440 --> 00:30:57,639 because this function has been 849 00:30:57,640 --> 00:30:59,799 specifically designed to 850 00:30:59,800 --> 00:31:01,869 make this very expensive. 851 00:31:01,870 --> 00:31:03,969 So if we could check that, if we 852 00:31:03,970 --> 00:31:06,069 could check the injectivity here, that we 853 00:31:06,070 --> 00:31:08,289 would basically have an attack 854 00:31:08,290 --> 00:31:10,629 on SHABAAN or we could prove 855 00:31:10,630 --> 00:31:12,969 that it's that there is no attack. 856 00:31:12,970 --> 00:31:14,049 So we cannot do that. 857 00:31:14,050 --> 00:31:16,239 We have to simplify the problem 858 00:31:16,240 --> 00:31:19,359 and we simplify it by offloading, 859 00:31:19,360 --> 00:31:22,239 um, the reasoning about 860 00:31:22,240 --> 00:31:24,429 one onto, again, onto somebody 861 00:31:24,430 --> 00:31:26,919 else. So we say the cryptographers 862 00:31:26,920 --> 00:31:29,019 take care of the behavior of 863 00:31:29,020 --> 00:31:31,599 one and we only check the code 864 00:31:31,600 --> 00:31:33,669 that is outside of Chavan 865 00:31:33,670 --> 00:31:35,109 because this is the code that is 866 00:31:35,110 --> 00:31:37,179 nonstandard and this is the code that is 867 00:31:37,180 --> 00:31:39,249 error prone, the SHABAAN 868 00:31:39,250 --> 00:31:40,989 itself. This is a standard primitive, 869 00:31:40,990 --> 00:31:42,469 their standard implementations. 870 00:31:42,470 --> 00:31:44,229 You have standard tests used. 871 00:31:44,230 --> 00:31:46,419 Um, it is difficult to break 872 00:31:46,420 --> 00:31:47,919 that, but it is very easy to break the 873 00:31:47,920 --> 00:31:48,889 code outside of it. 874 00:31:48,890 --> 00:31:51,069 So we will look only at the code 875 00:31:51,070 --> 00:31:53,829 outside and we do this 876 00:31:53,830 --> 00:31:54,769 in the following manner. 877 00:31:54,770 --> 00:31:56,829 So here is a 878 00:31:56,830 --> 00:31:59,199 little visualization of the same 879 00:31:59,200 --> 00:32:01,059 call that is shown on top. 880 00:32:02,710 --> 00:32:03,710 Uh, and. 881 00:32:04,780 --> 00:32:06,819 Now, there are two steps, actually, to 882 00:32:06,820 --> 00:32:08,919 replace this call with something 883 00:32:08,920 --> 00:32:10,959 that is easier to reason about, but at 884 00:32:10,960 --> 00:32:13,149 the same time, that still 885 00:32:13,150 --> 00:32:15,309 gives you useful information about all 886 00:32:15,310 --> 00:32:16,239 the cold outside. 887 00:32:16,240 --> 00:32:18,429 So we want to replace that call 888 00:32:18,430 --> 00:32:19,809 by something in a.. 889 00:32:19,810 --> 00:32:20,949 Any particular sense. 890 00:32:20,950 --> 00:32:22,419 And there are two steps to that. 891 00:32:22,420 --> 00:32:25,389 The first step is to identify 892 00:32:25,390 --> 00:32:27,789 the part of the input that will 893 00:32:27,790 --> 00:32:28,840 contain the entropy 894 00:32:29,950 --> 00:32:30,950 and. 895 00:32:32,570 --> 00:32:33,909 You could say, well, but this is 896 00:32:33,910 --> 00:32:36,039 difficult, but in fact, it is not as 897 00:32:36,040 --> 00:32:38,169 difficult as one thinks so 898 00:32:38,170 --> 00:32:39,719 first. 899 00:32:39,720 --> 00:32:41,459 We let the user do this, we could also 900 00:32:41,460 --> 00:32:43,289 automate that, but for the time being, we 901 00:32:43,290 --> 00:32:44,219 didn't bother. 902 00:32:44,220 --> 00:32:46,139 So we let the user do this first with the 903 00:32:46,140 --> 00:32:48,419 contextual clues, with the names 904 00:32:48,420 --> 00:32:50,759 of the variables and so on and so forth. 905 00:32:50,760 --> 00:32:53,369 Then with the information 906 00:32:53,370 --> 00:32:55,919 that we provide 907 00:32:55,920 --> 00:32:56,969 on counterexamples. 908 00:32:56,970 --> 00:32:59,129 And I will talk a little bit 909 00:32:59,130 --> 00:33:00,629 about that later. 910 00:33:00,630 --> 00:33:03,029 And also, you could just try 911 00:33:03,030 --> 00:33:04,229 different things. 912 00:33:04,230 --> 00:33:06,389 So here you have a choice 913 00:33:06,390 --> 00:33:08,399 actually between three different things. 914 00:33:08,400 --> 00:33:11,359 So the fourth is not big enough for 915 00:33:11,360 --> 00:33:13,049 for the 20 byte output. 916 00:33:14,730 --> 00:33:16,079 You can choose between these three 917 00:33:16,080 --> 00:33:18,299 things. You can just brute force it if 918 00:33:18,300 --> 00:33:20,039 you choose wrong that you will get a 919 00:33:20,040 --> 00:33:21,459 false alarm in the end. 920 00:33:21,460 --> 00:33:23,159 So the whole construction will not be 921 00:33:23,160 --> 00:33:25,319 objective and you can fix the 922 00:33:25,320 --> 00:33:26,969 problem and try again. 923 00:33:26,970 --> 00:33:27,970 So. 924 00:33:28,580 --> 00:33:30,079 First, we find. 925 00:33:31,390 --> 00:33:33,579 And input parameter with the length 926 00:33:33,580 --> 00:33:35,710 of 20 by it, because the output is 25. 927 00:33:37,030 --> 00:33:39,309 And then we have to replace that 928 00:33:39,310 --> 00:33:40,449 function by something else. 929 00:33:40,450 --> 00:33:42,579 And here we have two possibilities with 930 00:33:42,580 --> 00:33:44,079 what to replace it. 931 00:33:44,080 --> 00:33:46,359 And the first one is 932 00:33:46,360 --> 00:33:48,699 very simple. We can just replace 933 00:33:48,700 --> 00:33:50,479 this Chavan function by identity. 934 00:33:50,480 --> 00:33:52,899 We can just copy the content 935 00:33:52,900 --> 00:33:55,089 of the seed to the output. 936 00:33:55,090 --> 00:33:57,339 This is very simple and it also 937 00:33:57,340 --> 00:33:59,499 has many advantages because 938 00:33:59,500 --> 00:34:02,019 if you do this, um, 939 00:34:02,020 --> 00:34:03,819 well, with a little bit of luck, actually 940 00:34:03,820 --> 00:34:05,919 a holperin construction will become 941 00:34:05,920 --> 00:34:07,449 an identity function. 942 00:34:07,450 --> 00:34:09,549 So the output that 943 00:34:09,550 --> 00:34:11,439 the parent produces after you do this 944 00:34:11,440 --> 00:34:13,089 replacement will look very much like the 945 00:34:13,090 --> 00:34:15,339 seed, maybe the seed repeated 946 00:34:15,340 --> 00:34:16,448 and you can test for that. 947 00:34:16,449 --> 00:34:18,549 So you can immediately check 948 00:34:18,550 --> 00:34:20,649 that all the other code is 949 00:34:20,650 --> 00:34:21,549 fine. 950 00:34:21,550 --> 00:34:23,138 This construction is not sound because 951 00:34:23,139 --> 00:34:24,729 you have replaced one function with an 952 00:34:24,730 --> 00:34:27,428 unrelated function, but 953 00:34:27,429 --> 00:34:29,738 often or most of the time it will work 954 00:34:29,739 --> 00:34:31,839 and it will work and it will be OK. 955 00:34:31,840 --> 00:34:33,549 So the results will be trustworthy 956 00:34:33,550 --> 00:34:35,948 because you can imagine a 957 00:34:35,949 --> 00:34:38,079 typical parent is actually 958 00:34:38,080 --> 00:34:40,269 agnostic of the concrete data that 959 00:34:40,270 --> 00:34:42,428 you have in your seed. 960 00:34:42,429 --> 00:34:44,769 So it would be it 961 00:34:44,770 --> 00:34:46,509 would be strange if the parent would do 962 00:34:46,510 --> 00:34:48,638 different things, depending on what 963 00:34:48,639 --> 00:34:49,639 exactly 964 00:34:50,830 --> 00:34:52,609 the data is that it is operating on. 965 00:34:52,610 --> 00:34:54,819 So you can actually substitute 966 00:34:54,820 --> 00:34:55,928 this data for something else. 967 00:34:55,929 --> 00:34:57,999 You can substitute the one hash by the 968 00:34:58,000 --> 00:34:59,800 just copy of the seed. 969 00:35:01,610 --> 00:35:03,469 So this is this is very useful. 970 00:35:03,470 --> 00:35:04,789 This is great for debugging. 971 00:35:04,790 --> 00:35:06,619 Uh, you can already test many things for 972 00:35:06,620 --> 00:35:07,939 this replacement, but it is still 973 00:35:07,940 --> 00:35:09,139 unsound. 974 00:35:09,140 --> 00:35:11,419 And what we can do because 975 00:35:11,420 --> 00:35:13,279 we are not just testing things, but we 976 00:35:13,280 --> 00:35:15,649 are applying a formal reasoning 977 00:35:15,650 --> 00:35:16,940 tool, is that we can. 978 00:35:18,360 --> 00:35:20,669 Here, instead of this 979 00:35:20,670 --> 00:35:22,889 identity function, use something else 980 00:35:22,890 --> 00:35:24,659 we can use a mathematical construct, we 981 00:35:24,660 --> 00:35:27,469 can say we replace 982 00:35:27,470 --> 00:35:28,749 at this particular. 983 00:35:30,090 --> 00:35:32,369 Um, this particular function is an 984 00:35:32,370 --> 00:35:34,109 abstraction, we replace it with an 985 00:35:34,110 --> 00:35:36,209 underspecified injector 986 00:35:36,210 --> 00:35:37,709 function, so we do not say what it is, 987 00:35:37,710 --> 00:35:39,839 but it is something that is injected. 988 00:35:39,840 --> 00:35:41,669 And this is an approximation of the 989 00:35:41,670 --> 00:35:43,589 behavior of the hash function here. 990 00:35:43,590 --> 00:35:45,689 And the results that you get will 991 00:35:45,690 --> 00:35:48,179 also transform to the original 992 00:35:48,180 --> 00:35:49,180 code that you have. 993 00:35:50,640 --> 00:35:53,040 So we would typically do the first thing. 994 00:35:54,760 --> 00:35:57,339 And that will help us to find bugs, 995 00:35:57,340 --> 00:35:59,499 um, it will show us collisions, if 996 00:35:59,500 --> 00:36:01,239 the any we can actually look at the 997 00:36:01,240 --> 00:36:03,379 trace, we can we can see how the 998 00:36:03,380 --> 00:36:05,889 speech pattern of the seed propagates 999 00:36:05,890 --> 00:36:07,359 along the implementation. 1000 00:36:07,360 --> 00:36:09,609 We can just print 1001 00:36:09,610 --> 00:36:11,889 at print statements along the way and 1002 00:36:11,890 --> 00:36:14,469 we see where these, um, 1003 00:36:14,470 --> 00:36:16,299 how this flow is working. 1004 00:36:16,300 --> 00:36:18,280 We will not show that today, but 1005 00:36:19,300 --> 00:36:21,699 we do have a nice visualization there. 1006 00:36:21,700 --> 00:36:23,709 And then in the end we switch over to the 1007 00:36:23,710 --> 00:36:25,479 sound of idealization and then we prove 1008 00:36:25,480 --> 00:36:27,309 that the positive result that we get and 1009 00:36:27,310 --> 00:36:29,089 then the good result is indeed. 1010 00:36:29,090 --> 00:36:31,139 All right. 1011 00:36:32,290 --> 00:36:34,149 A few words about the implementation. 1012 00:36:34,150 --> 00:36:36,299 So little commercial break here. 1013 00:36:36,300 --> 00:36:38,439 We could get 1014 00:36:38,440 --> 00:36:40,269 that far because we were standing on the 1015 00:36:40,270 --> 00:36:42,609 shoulders of giants and the two giants. 1016 00:36:42,610 --> 00:36:44,829 Here is the CBC 1017 00:36:44,830 --> 00:36:46,389 Endemol check. 1018 00:36:46,390 --> 00:36:48,789 It means it is a static analysis tool 1019 00:36:48,790 --> 00:36:50,949 that you can, uh, 1020 00:36:50,950 --> 00:36:53,109 feed your implementation in here 1021 00:36:53,110 --> 00:36:55,329 in Java and it will 1022 00:36:55,330 --> 00:36:57,309 happily take it, even if it's something 1023 00:36:57,310 --> 00:36:59,679 complex, like open SSL or Linux kernel 1024 00:36:59,680 --> 00:37:00,099 or something. 1025 00:37:00,100 --> 00:37:01,959 So this is this is really the advantage 1026 00:37:01,960 --> 00:37:02,439 with this tool. 1027 00:37:02,440 --> 00:37:05,229 It's a really robust and fantastic tool. 1028 00:37:05,230 --> 00:37:07,509 It will explore the behavior of 1029 00:37:07,510 --> 00:37:09,819 your program to a particular depth 1030 00:37:09,820 --> 00:37:11,020 and it will detect. 1031 00:37:12,660 --> 00:37:14,729 Uh, well, certain things that can 1032 00:37:14,730 --> 00:37:16,649 detect predefine things like Buffa or 1033 00:37:16,650 --> 00:37:18,509 flaws and so on, but it can also check 1034 00:37:18,510 --> 00:37:20,519 user specified assertions. 1035 00:37:20,520 --> 00:37:22,619 So even if you have 1036 00:37:22,620 --> 00:37:23,969 nothing to do with cryptographically 1037 00:37:23,970 --> 00:37:25,829 ranges formally recommended to use that 1038 00:37:25,830 --> 00:37:27,959 tool to gain to gain 1039 00:37:27,960 --> 00:37:29,849 confidence in your implementation. 1040 00:37:29,850 --> 00:37:31,949 And on the other hand, we are using 1041 00:37:31,950 --> 00:37:34,379 many such Sasolburg, 1042 00:37:34,380 --> 00:37:36,509 which is also quite an amazing piece 1043 00:37:36,510 --> 00:37:37,589 of technology. 1044 00:37:37,590 --> 00:37:38,609 I mean, there are, of course, other 1045 00:37:38,610 --> 00:37:41,309 tools. The other verification 1046 00:37:41,310 --> 00:37:43,289 tools and other such told us this is just 1047 00:37:43,290 --> 00:37:45,389 what we are familiar with and you 1048 00:37:45,390 --> 00:37:47,099 know, that satyrs and then complete 1049 00:37:47,100 --> 00:37:49,259 problem. But it doesn't really matter for 1050 00:37:49,260 --> 00:37:51,289 us in practice. We can feed formulas that 1051 00:37:51,290 --> 00:37:53,579 the gigabytes and size to the solver. 1052 00:37:53,580 --> 00:37:55,679 And within seconds it will tell us if 1053 00:37:55,680 --> 00:37:58,049 this formula says that is viable, if 1054 00:37:58,050 --> 00:37:59,939 there is a problem in the appearing or 1055 00:37:59,940 --> 00:38:02,009 not, and we use 1056 00:38:02,010 --> 00:38:04,289 these tools to combine 1057 00:38:04,290 --> 00:38:06,479 these tools with our 1058 00:38:06,480 --> 00:38:07,109 own code. 1059 00:38:07,110 --> 00:38:09,479 So we use BMC to 1060 00:38:09,480 --> 00:38:11,869 generate a description. 1061 00:38:11,870 --> 00:38:14,659 Of what the parent does as a formula, 1062 00:38:14,660 --> 00:38:17,119 and then we combine this description 1063 00:38:17,120 --> 00:38:19,129 into this definition of injectivity that 1064 00:38:19,130 --> 00:38:20,689 I have shown you previously, and we feed 1065 00:38:20,690 --> 00:38:22,459 the result in two minutes, 10 minutes, 1066 00:38:22,460 --> 00:38:24,979 and we'll see if it is possible to find 1067 00:38:24,980 --> 00:38:26,869 a violation of injectivity in this 1068 00:38:26,870 --> 00:38:27,349 formula. 1069 00:38:27,350 --> 00:38:30,679 And if it does, then we show 1070 00:38:30,680 --> 00:38:32,839 the resulting traces for 1071 00:38:32,840 --> 00:38:34,969 the two seats and the same 1072 00:38:34,970 --> 00:38:36,529 output to the user. 1073 00:38:36,530 --> 00:38:38,329 And they call procedures you have seen 1074 00:38:38,330 --> 00:38:40,579 takes some seconds so you can use 1075 00:38:40,580 --> 00:38:42,070 you can use the tool interactively. 1076 00:38:44,000 --> 00:38:46,309 What are the results from applying 1077 00:38:46,310 --> 00:38:47,310 this? 1078 00:38:49,490 --> 00:38:52,079 So that rule was applied on various 1079 00:38:52,080 --> 00:38:55,099 pages and first the good parts. 1080 00:38:55,100 --> 00:38:57,199 So we check those. 1081 00:38:57,200 --> 00:38:59,269 We did not found anything suspicious 1082 00:38:59,270 --> 00:39:01,429 there that we could verify 1083 00:39:01,430 --> 00:39:03,349 that the punji code around the 1084 00:39:03,350 --> 00:39:05,449 cryptographic primitives is objective 1085 00:39:05,450 --> 00:39:06,739 and does not loose entropy. 1086 00:39:08,610 --> 00:39:10,759 Now, we, as I said 1087 00:39:10,760 --> 00:39:13,309 previously, had this known problem, 1088 00:39:13,310 --> 00:39:14,899 when we reinstate the problem, we would 1089 00:39:14,900 --> 00:39:16,099 have detected that. 1090 00:39:16,100 --> 00:39:18,319 And when we removed the problem, we 1091 00:39:18,320 --> 00:39:19,730 detect no further problem. 1092 00:39:21,620 --> 00:39:22,620 You know, Vanessa's l 1093 00:39:23,690 --> 00:39:24,859 that's quite similar. 1094 00:39:24,860 --> 00:39:26,299 Yeah, we would have detected if you 1095 00:39:26,300 --> 00:39:27,300 remove the code. 1096 00:39:28,610 --> 00:39:31,819 We also detected other problems 1097 00:39:31,820 --> 00:39:34,129 in code that is 1098 00:39:34,130 --> 00:39:36,469 may or may not be used in practice, 1099 00:39:36,470 --> 00:39:38,569 and that has 1100 00:39:38,570 --> 00:39:40,819 problem managing the circular buffer 1101 00:39:40,820 --> 00:39:43,279 with the array going off by one 1102 00:39:43,280 --> 00:39:45,320 writing one byte outside the buffer 1103 00:39:46,580 --> 00:39:48,079 doing doing strange stuff. 1104 00:39:48,080 --> 00:39:50,540 But all that was not very fatal. 1105 00:39:52,160 --> 00:39:54,469 Yeah. And then finally, we 1106 00:39:54,470 --> 00:39:57,499 found the critical back in 1107 00:39:57,500 --> 00:39:59,569 Viji that 1108 00:39:59,570 --> 00:40:01,729 we then cost to be fixed. 1109 00:40:01,730 --> 00:40:03,859 And I will show you how 1110 00:40:03,860 --> 00:40:06,019 that works, how the other back 1111 00:40:06,020 --> 00:40:08,149 works, whether that's the problem and how 1112 00:40:08,150 --> 00:40:10,639 the bug could be gone undetected 1113 00:40:10,640 --> 00:40:12,049 for so long. 1114 00:40:12,050 --> 00:40:13,050 So. 1115 00:40:20,270 --> 00:40:22,369 So first of all, there was there 1116 00:40:22,370 --> 00:40:24,619 was a paper that proposed 1117 00:40:24,620 --> 00:40:26,959 how we could operate, apparently, and 1118 00:40:26,960 --> 00:40:29,119 first I would like to show you how it was 1119 00:40:29,120 --> 00:40:31,879 designed to be implemented. 1120 00:40:31,880 --> 00:40:33,979 So we have the Buffa with with 1121 00:40:33,980 --> 00:40:35,009 random data here. 1122 00:40:35,010 --> 00:40:37,099 And what we're looking at here 1123 00:40:37,100 --> 00:40:39,349 is the perturbing function that 1124 00:40:39,350 --> 00:40:41,689 mixes the buffer internally 1125 00:40:41,690 --> 00:40:44,179 in some strange way using cryptographic 1126 00:40:44,180 --> 00:40:46,249 primitives. And what was suggested here 1127 00:40:46,250 --> 00:40:48,349 is that we would take 1128 00:40:48,350 --> 00:40:50,539 84 bytes of the 1129 00:40:50,540 --> 00:40:51,540 of the buffer. 1130 00:40:53,010 --> 00:40:55,169 Hash them using hash function and 1131 00:40:55,170 --> 00:40:57,239 override the middle 1132 00:40:57,240 --> 00:40:59,339 20 bytes that we 1133 00:40:59,340 --> 00:41:01,409 have above here and then 1134 00:41:01,410 --> 00:41:03,539 this this buffer would go 1135 00:41:03,540 --> 00:41:06,089 up there again, you would ask 1136 00:41:06,090 --> 00:41:08,939 after hashing, we would move to the next 1137 00:41:08,940 --> 00:41:11,129 to the next block and hash 1138 00:41:11,130 --> 00:41:13,379 that again moved to the next 1139 00:41:13,380 --> 00:41:15,479 block and so on and so on until 1140 00:41:15,480 --> 00:41:17,579 the end where there that 1141 00:41:17,580 --> 00:41:19,919 happens and wrap around. 1142 00:41:19,920 --> 00:41:21,899 And finally, the last block would be 1143 00:41:21,900 --> 00:41:24,269 calculated by hashing this 1144 00:41:24,270 --> 00:41:26,939 blocks and the block here at front. 1145 00:41:26,940 --> 00:41:28,799 Then we would get the last block. 1146 00:41:28,800 --> 00:41:30,809 And then finally, this this buffer would 1147 00:41:30,810 --> 00:41:32,789 be handed out to the user as this is your 1148 00:41:32,790 --> 00:41:33,790 random data. 1149 00:41:35,880 --> 00:41:38,129 We had an hash function that was 1150 00:41:38,130 --> 00:41:40,769 that that took smaller input sizes, not 1151 00:41:40,770 --> 00:41:43,739 eighty four, but sixty four bytes, 1152 00:41:43,740 --> 00:41:46,349 and for reasons that are not 1153 00:41:46,350 --> 00:41:49,319 that clear, they decided 1154 00:41:49,320 --> 00:41:51,599 to just have a 60 bytes 1155 00:41:51,600 --> 00:41:53,069 hash function that just left the middle 1156 00:41:53,070 --> 00:41:54,319 bit out here. 1157 00:41:54,320 --> 00:41:56,339 Yeah, we are overriding that anyway so we 1158 00:41:56,340 --> 00:41:58,409 can do that. I don't know really what 1159 00:41:58,410 --> 00:42:00,690 was the intention, but what happens 1160 00:42:01,860 --> 00:42:03,929 with the dog is we would have them 1161 00:42:03,930 --> 00:42:06,119 write that down and so on and 1162 00:42:06,120 --> 00:42:08,459 so on and so on 1163 00:42:08,460 --> 00:42:10,109 until the end. 1164 00:42:10,110 --> 00:42:12,389 Where would take this one, 1165 00:42:12,390 --> 00:42:14,399 this one, hash them and write them here. 1166 00:42:15,850 --> 00:42:17,649 And this buffer is now should not be 1167 00:42:17,650 --> 00:42:18,650 random. 1168 00:42:19,250 --> 00:42:21,139 It's that buffer really random. 1169 00:42:22,600 --> 00:42:24,759 When we take this block and this 1170 00:42:24,760 --> 00:42:26,859 block, they are here 1171 00:42:26,860 --> 00:42:28,989 and here again and 1172 00:42:28,990 --> 00:42:31,179 hash them we to get this last 1173 00:42:31,180 --> 00:42:32,180 block. 1174 00:42:33,320 --> 00:42:34,429 The buffer cannot be run. 1175 00:42:34,430 --> 00:42:36,529 We can calculate the last 20 1176 00:42:36,530 --> 00:42:38,689 bytes when we use these 1177 00:42:38,690 --> 00:42:40,879 44 and these 20 bytes, 1178 00:42:40,880 --> 00:42:43,379 hashing them would get exactly 1179 00:42:43,380 --> 00:42:44,380 this block. 1180 00:42:45,790 --> 00:42:47,979 Yeah, so so that's that's 1181 00:42:47,980 --> 00:42:50,409 what happened, though, that's 1182 00:42:50,410 --> 00:42:51,819 that's a thinking problem. 1183 00:42:51,820 --> 00:42:53,769 Yeah, that's not really off by one 1184 00:42:53,770 --> 00:42:55,050 implementation problem. 1185 00:42:57,270 --> 00:42:59,429 But that's yeah, that's yeah, that's 1186 00:42:59,430 --> 00:43:00,430 essentially. 1187 00:43:01,080 --> 00:43:02,080 What happened there? 1188 00:43:04,750 --> 00:43:06,340 So the. 1189 00:43:10,530 --> 00:43:12,150 You know what the consequences are? 1190 00:43:13,860 --> 00:43:16,489 Yeah, I'm 1191 00:43:16,490 --> 00:43:18,719 on keys, they were hopefully 1192 00:43:18,720 --> 00:43:20,129 not that bad, but 1193 00:43:21,390 --> 00:43:23,519 yeah, hopefully we spotted that problem, 1194 00:43:23,520 --> 00:43:25,679 that problem lay dormant there 1195 00:43:25,680 --> 00:43:28,049 for a long period of time, 1196 00:43:28,050 --> 00:43:30,419 had several security audits. 1197 00:43:30,420 --> 00:43:31,509 Nobody spotted that. 1198 00:43:31,510 --> 00:43:32,429 Yeah, we looked at the code. 1199 00:43:32,430 --> 00:43:33,899 It said initial import. 1200 00:43:33,900 --> 00:43:36,149 So for several 1201 00:43:36,150 --> 00:43:38,309 years, years old and or we 1202 00:43:38,310 --> 00:43:41,099 can take away from that is that 1203 00:43:41,100 --> 00:43:42,809 audits are necessary. 1204 00:43:42,810 --> 00:43:44,369 Looking at the code is necessary, 1205 00:43:45,630 --> 00:43:48,419 that the code has grown too complex 1206 00:43:48,420 --> 00:43:51,029 to to fully understand 1207 00:43:51,030 --> 00:43:51,779 it manually. 1208 00:43:51,780 --> 00:43:54,360 So we have to take technical assurance 1209 00:43:55,500 --> 00:43:57,899 to verify that 1210 00:43:57,900 --> 00:43:59,199 the code is correct. 1211 00:43:59,200 --> 00:44:01,619 So thank you for your attention 1212 00:44:01,620 --> 00:44:02,620 and the. 1213 00:44:15,830 --> 00:44:17,269 Thank you. 1214 00:44:17,270 --> 00:44:19,069 If you have questions, please line up at 1215 00:44:19,070 --> 00:44:20,989 the microphones on stage and it's all 1216 00:44:20,990 --> 00:44:21,999 there are four of them, 1217 00:44:23,120 --> 00:44:24,709 and if you would like to leave now, 1218 00:44:24,710 --> 00:44:26,329 please do that quietly so that other 1219 00:44:26,330 --> 00:44:28,039 people can still listen to the Q&A 1220 00:44:30,950 --> 00:44:31,969 on the right hand side. 1221 00:44:31,970 --> 00:44:32,970 The. 1222 00:44:33,950 --> 00:44:35,569 Yes, hello. 1223 00:44:35,570 --> 00:44:36,589 Thank you for the presentation. 1224 00:44:36,590 --> 00:44:38,359 Very interesting. 1225 00:44:38,360 --> 00:44:40,669 Is there some kind of implementation 1226 00:44:40,670 --> 00:44:42,919 for mere mortals like us that 1227 00:44:42,920 --> 00:44:45,289 can take their 1228 00:44:45,290 --> 00:44:46,969 current stack of whatever they have? 1229 00:44:46,970 --> 00:44:50,179 For example, generate 1230 00:44:50,180 --> 00:44:52,789 a.. 20 RSX, 1231 00:44:52,790 --> 00:44:55,069 upload them to you and you tell 1232 00:44:55,070 --> 00:44:57,379 us whether those look and 1233 00:44:57,380 --> 00:44:59,839 or random enough from each other 1234 00:44:59,840 --> 00:45:02,359 and thus my system actually generate 1235 00:45:02,360 --> 00:45:04,759 correctly, you know? 1236 00:45:04,760 --> 00:45:07,039 Yeah. As we as we try to explain 1237 00:45:07,040 --> 00:45:09,379 the problems that we are looking here at 1238 00:45:09,380 --> 00:45:11,629 cannot be detected when just 1239 00:45:11,630 --> 00:45:13,309 looking at the output of the PMG. 1240 00:45:13,310 --> 00:45:15,199 So when you have one output stream of 1241 00:45:15,200 --> 00:45:17,359 your fiancée, that would still 1242 00:45:17,360 --> 00:45:19,519 look random. So statistical test 1243 00:45:19,520 --> 00:45:21,799 suites, one, detect anything. 1244 00:45:21,800 --> 00:45:23,839 So the only thing that you could do is 1245 00:45:23,840 --> 00:45:25,999 check for known issues and have 1246 00:45:26,000 --> 00:45:27,889 known all all streams that the known 1247 00:45:27,890 --> 00:45:28,919 issues produce. 1248 00:45:28,920 --> 00:45:31,009 So with the with 1249 00:45:31,010 --> 00:45:33,109 the open SSL disaster that we luckily 1250 00:45:33,110 --> 00:45:35,239 only only a few 1251 00:45:35,240 --> 00:45:37,339 so that you can have all those thirty 1252 00:45:37,340 --> 00:45:39,049 thousand keys and check against them. 1253 00:45:39,050 --> 00:45:41,239 But just looking at the keys and 1254 00:45:41,240 --> 00:45:43,639 not knowing what to look for, 1255 00:45:43,640 --> 00:45:44,719 I think that's not possible. 1256 00:45:47,270 --> 00:45:48,739 Apparent on the right. 1257 00:45:48,740 --> 00:45:49,339 Yeah. 1258 00:45:49,340 --> 00:45:51,949 So could your techniques beneficially 1259 00:45:51,950 --> 00:45:53,599 be applied to other cryptographic 1260 00:45:53,600 --> 00:45:55,729 primitives like block ciphers or the 1261 00:45:55,730 --> 00:45:57,109 building blocks that go into block 1262 00:45:57,110 --> 00:45:58,110 ciphers? 1263 00:45:58,820 --> 00:46:01,099 Um, that's a good question. 1264 00:46:01,100 --> 00:46:03,229 So you could I think 1265 00:46:03,230 --> 00:46:06,349 you could apply them to particular 1266 00:46:06,350 --> 00:46:08,509 auxiliary code 1267 00:46:08,510 --> 00:46:11,209 that accompanies the, 1268 00:46:11,210 --> 00:46:13,039 um, the primitives. 1269 00:46:13,040 --> 00:46:14,599 So the techniques that we've shown you 1270 00:46:14,600 --> 00:46:16,279 are purely information theoretical. 1271 00:46:16,280 --> 00:46:18,499 So they are not concerned with 1272 00:46:18,500 --> 00:46:20,599 cryptography as such, 1273 00:46:20,600 --> 00:46:22,969 but also in cryptographic code 1274 00:46:22,970 --> 00:46:24,169 you need these things. 1275 00:46:24,170 --> 00:46:26,569 So for key expansion, for example, 1276 00:46:26,570 --> 00:46:28,489 Qiqi expansion is supposed to have the 1277 00:46:28,490 --> 00:46:30,529 same injectivity properties you could you 1278 00:46:30,530 --> 00:46:31,879 could apply there. 1279 00:46:31,880 --> 00:46:34,339 So there are some applications, but 1280 00:46:34,340 --> 00:46:36,979 they are also very clear limitations. 1281 00:46:42,130 --> 00:46:43,839 All right, let's it's that question from 1282 00:46:43,840 --> 00:46:44,840 the IOC. 1283 00:46:47,410 --> 00:46:49,719 No, it's not OK to let that 1284 00:46:49,720 --> 00:46:50,829 one in the back. 1285 00:46:50,830 --> 00:46:51,969 Hello. 1286 00:46:51,970 --> 00:46:53,799 If I understood your definition of 1287 00:46:53,800 --> 00:46:55,839 entropy correctly, you mean if you have 1288 00:46:55,840 --> 00:46:57,939 two seats that go to the same 1289 00:46:57,940 --> 00:47:00,609 output that you would consider a problem? 1290 00:47:00,610 --> 00:47:02,679 Um, and you had several 1291 00:47:02,680 --> 00:47:05,109 examples with one, I think for myself. 1292 00:47:05,110 --> 00:47:06,819 And I think the Linux kind is also using 1293 00:47:06,820 --> 00:47:08,889 Shravan. And that would mean, as far 1294 00:47:08,890 --> 00:47:11,109 as I understand, that if you have 1295 00:47:11,110 --> 00:47:13,029 a hash function with, uh, with a 1296 00:47:13,030 --> 00:47:15,579 collision, then this would 1297 00:47:15,580 --> 00:47:17,949 generate a situation of entropy loss. 1298 00:47:17,950 --> 00:47:20,049 So what that mean that and 1299 00:47:20,050 --> 00:47:22,299 we assume that one will have collision 1300 00:47:22,300 --> 00:47:24,699 problems within the next couple of years. 1301 00:47:24,700 --> 00:47:27,249 So is there any practical problem 1302 00:47:27,250 --> 00:47:29,589 if you use a non existent 1303 00:47:29,590 --> 00:47:31,009 hash function here? 1304 00:47:31,010 --> 00:47:33,899 OK, so this is a little subtle. 1305 00:47:33,900 --> 00:47:36,519 Um, there are two answers to this. 1306 00:47:36,520 --> 00:47:39,489 So first, um, 1307 00:47:39,490 --> 00:47:41,889 well, first, we are 1308 00:47:41,890 --> 00:47:43,989 trying actually to look at the code that 1309 00:47:43,990 --> 00:47:46,449 is outside of Schavan 1310 00:47:46,450 --> 00:47:48,609 because this is where the 1311 00:47:48,610 --> 00:47:50,259 mistakes often are. 1312 00:47:50,260 --> 00:47:52,359 So we try actually not to say 1313 00:47:52,360 --> 00:47:54,459 Siobhan is someone else's problem, 1314 00:47:54,460 --> 00:47:56,739 but also to be more exact, the 1315 00:47:56,740 --> 00:47:58,059 collisions. 1316 00:47:58,060 --> 00:48:00,759 So we are looking at injectivity from a 1317 00:48:00,760 --> 00:48:02,919 20 byte input to a 20 1318 00:48:02,920 --> 00:48:03,879 byte output. 1319 00:48:03,880 --> 00:48:05,499 And of course, if you find a collision 1320 00:48:05,500 --> 00:48:08,349 there, then, well, this will 1321 00:48:08,350 --> 00:48:10,899 weaken your power and give a little bit. 1322 00:48:10,900 --> 00:48:13,089 But, uh, hopefully they are not too many 1323 00:48:13,090 --> 00:48:14,829 of these collisions because if there were 1324 00:48:14,830 --> 00:48:17,379 too many, they would be easy to find. 1325 00:48:17,380 --> 00:48:18,849 But at some point, of course, you also 1326 00:48:18,850 --> 00:48:20,349 probably have to upgrade the hash 1327 00:48:20,350 --> 00:48:21,489 function and you up your energy. 1328 00:48:21,490 --> 00:48:22,490 So 1329 00:48:23,560 --> 00:48:25,629 it's very we can discuss that later in 1330 00:48:25,630 --> 00:48:26,630 detail. 1331 00:48:27,640 --> 00:48:28,839 OK, on the left up front 1332 00:48:30,280 --> 00:48:33,009 in the theory of, uh, deterministic 1333 00:48:33,010 --> 00:48:35,469 on the notions of forward 1334 00:48:35,470 --> 00:48:37,779 and Peckford and enhance 1335 00:48:37,780 --> 00:48:40,239 that secrecy, um, 1336 00:48:40,240 --> 00:48:42,579 as I understood, your 1337 00:48:42,580 --> 00:48:44,529 theory is going forward. 1338 00:48:44,530 --> 00:48:46,959 So detecting entropy 1339 00:48:46,960 --> 00:48:49,059 loss, would it be possible in 1340 00:48:49,060 --> 00:48:51,399 principle to detect, 1341 00:48:51,400 --> 00:48:54,129 uh, not fulfillment 1342 00:48:54,130 --> 00:48:56,289 of enhanced Peckford 1343 00:48:56,290 --> 00:48:58,750 secrecy? So if you know 1344 00:48:59,830 --> 00:49:02,199 or so the output 1345 00:49:02,200 --> 00:49:04,599 and in the state to go 1346 00:49:04,600 --> 00:49:06,699 backward to 1347 00:49:06,700 --> 00:49:08,739 guess form outputs? 1348 00:49:10,030 --> 00:49:11,030 Um, 1349 00:49:12,850 --> 00:49:14,559 that's a good question. I will have to 1350 00:49:14,560 --> 00:49:15,989 think about that, OK. 1351 00:49:17,500 --> 00:49:19,559 Yeah. I think we 1352 00:49:19,560 --> 00:49:21,819 are not looking at, uh, secrecy 1353 00:49:21,820 --> 00:49:23,919 in forward secrecy 1354 00:49:23,920 --> 00:49:24,879 or backward secrecy. 1355 00:49:24,880 --> 00:49:27,129 We are just focusing on two 1356 00:49:27,130 --> 00:49:29,379 different seeds derive different outputs 1357 00:49:29,380 --> 00:49:31,449 so that that does not have 1358 00:49:31,450 --> 00:49:33,759 any implications on whether we 1359 00:49:33,760 --> 00:49:36,249 have knowing some random output 1360 00:49:36,250 --> 00:49:38,649 means that you can calculate the next 1361 00:49:38,650 --> 00:49:40,929 random output or the other way round. 1362 00:49:40,930 --> 00:49:43,009 Yeah, but in the sense it's looking at 1363 00:49:43,010 --> 00:49:45,489 the injectivity 1364 00:49:45,490 --> 00:49:47,829 of two of the three functions and 1365 00:49:47,830 --> 00:49:50,589 what we need for backward secrecy 1366 00:49:50,590 --> 00:49:52,779 would be the inverse function, not 1367 00:49:52,780 --> 00:49:54,969 not only so the inverse function would be 1368 00:49:54,970 --> 00:49:57,069 having the output stream and being 1369 00:49:57,070 --> 00:49:58,329 able to derive the seed. 1370 00:49:59,410 --> 00:50:01,689 But what factor secrecy would mean 1371 00:50:01,690 --> 00:50:03,879 is that you would have a part 1372 00:50:03,880 --> 00:50:05,949 of the output function that is behind 1373 00:50:05,950 --> 00:50:06,609 other states. 1374 00:50:06,610 --> 00:50:08,979 So I don't need to 1375 00:50:08,980 --> 00:50:10,989 see it. But, uh, in the state. 1376 00:50:12,610 --> 00:50:14,439 And that the G function is from the seat 1377 00:50:14,440 --> 00:50:15,679 to the outlook. 1378 00:50:15,680 --> 00:50:18,009 So, yeah, OK, but 1379 00:50:18,010 --> 00:50:20,019 just to clarify, the attack model here is 1380 00:50:20,020 --> 00:50:21,909 that the attackers observed the output 1381 00:50:21,910 --> 00:50:24,069 and tries to brute force the seed. 1382 00:50:24,070 --> 00:50:25,059 This is the attacker model. 1383 00:50:25,060 --> 00:50:26,589 If you want more things, you need to the 1384 00:50:26,590 --> 00:50:27,590 model. 1385 00:50:29,780 --> 00:50:31,789 OK, we do have a question from the 1386 00:50:31,790 --> 00:50:33,139 Internet. 1387 00:50:33,140 --> 00:50:35,479 Yeah, basically we have two questions. 1388 00:50:35,480 --> 00:50:37,759 First of all, Agonistic is asking 1389 00:50:37,760 --> 00:50:40,219 our physical implementations of R&D 1390 00:50:40,220 --> 00:50:42,319 better or do we need them to test the 1391 00:50:42,320 --> 00:50:43,320 same way? 1392 00:50:44,640 --> 00:50:47,759 I think we need to test them the same way 1393 00:50:47,760 --> 00:50:50,099 and yeah, 1394 00:50:50,100 --> 00:50:52,559 because they typically also have some 1395 00:50:52,560 --> 00:50:55,799 kind of hardware source of randomness. 1396 00:50:55,800 --> 00:50:58,109 And then there is this deterministic 1397 00:50:58,110 --> 00:51:00,179 expansion also on top of 1398 00:51:00,180 --> 00:51:01,980 that. So you need to check that. 1399 00:51:03,030 --> 00:51:05,549 Yeah, the answer is you do and 1400 00:51:05,550 --> 00:51:06,839 you can. 1401 00:51:06,840 --> 00:51:09,059 Thank you. And second, 1402 00:51:09,060 --> 00:51:11,249 the IOC or 1403 00:51:11,250 --> 00:51:12,539 some people on the street were not able 1404 00:51:12,540 --> 00:51:14,639 to see your explanation of the 1405 00:51:14,640 --> 00:51:15,869 new piggyback. 1406 00:51:15,870 --> 00:51:18,179 So could you please repeat that 1407 00:51:18,180 --> 00:51:19,530 without using the laser pointer? 1408 00:51:20,790 --> 00:51:22,889 OK, so the whole 1409 00:51:22,890 --> 00:51:25,559 problem finally boils down to that. 1410 00:51:25,560 --> 00:51:27,719 If you take blocks that 1411 00:51:27,720 --> 00:51:29,789 are not overwritten, so 1412 00:51:29,790 --> 00:51:32,219 they are visible in the output stream and 1413 00:51:32,220 --> 00:51:34,439 have them together using the hash 1414 00:51:34,440 --> 00:51:36,839 function that you hopefully know, 1415 00:51:36,840 --> 00:51:39,089 having the code, 1416 00:51:39,090 --> 00:51:41,489 then you can derive from that the last 1417 00:51:41,490 --> 00:51:42,209 20 bytes. 1418 00:51:42,210 --> 00:51:43,210 So. 1419 00:51:43,970 --> 00:51:47,119 First 44 and 1420 00:51:47,120 --> 00:51:49,999 not the last, but the before last 20 1421 00:51:50,000 --> 00:51:52,999 heads together, we'll 1422 00:51:53,000 --> 00:51:54,799 give you the last 20 bites. 1423 00:51:54,800 --> 00:51:56,939 And that's a problem because that's not 1424 00:51:56,940 --> 00:51:57,940 when. 1425 00:51:59,040 --> 00:52:01,229 Maybe not the way to formulate this 1426 00:52:01,230 --> 00:52:03,389 is when you have this dream and 1427 00:52:03,390 --> 00:52:05,039 you are looking at the last chunk in the 1428 00:52:05,040 --> 00:52:08,519 stream, then everything 1429 00:52:08,520 --> 00:52:11,279 that this chunk depends on 1430 00:52:11,280 --> 00:52:13,919 comes earlier in the stream. 1431 00:52:13,920 --> 00:52:14,969 And this is the problem. 1432 00:52:14,970 --> 00:52:17,569 So when you output the stream to 1433 00:52:17,570 --> 00:52:19,739 to the observer, the observer can 1434 00:52:19,740 --> 00:52:21,869 observe everything that 1435 00:52:21,870 --> 00:52:24,359 is needed to calculate the last chunk 1436 00:52:24,360 --> 00:52:26,939 in the stream. So there is no 1437 00:52:26,940 --> 00:52:29,399 more data that the observer 1438 00:52:29,400 --> 00:52:31,739 doesn't see going into the calculation 1439 00:52:31,740 --> 00:52:32,740 of the last chunk. 1440 00:52:33,940 --> 00:52:36,309 And yeah, OK, that's 1441 00:52:36,310 --> 00:52:39,309 your first microphone on the right. 1442 00:52:39,310 --> 00:52:41,119 One comment about hardware 1443 00:52:41,120 --> 00:52:43,179 implementations, because 1444 00:52:43,180 --> 00:52:45,729 usually you take two and 1445 00:52:45,730 --> 00:52:48,059 it's entropy and compress 1446 00:52:48,060 --> 00:52:49,659 them first to one. 1447 00:52:49,660 --> 00:52:51,969 And that's because 1448 00:52:51,970 --> 00:52:54,489 you ask this question or comment 1449 00:52:54,490 --> 00:52:56,739 is a problem for the detection 1450 00:52:56,740 --> 00:52:58,999 of entropy loss, because you're too sad, 1451 00:52:59,000 --> 00:53:01,719 because your heart will have a bias. 1452 00:53:01,720 --> 00:53:03,999 And you said, OK, 1453 00:53:04,000 --> 00:53:06,189 that is just an offset of 1454 00:53:06,190 --> 00:53:08,319 the comparators, something like that. 1455 00:53:08,320 --> 00:53:10,449 The bias is OK, you 1456 00:53:10,450 --> 00:53:12,549 solve the problem is bias by 1457 00:53:12,550 --> 00:53:14,829 compressing two and bit 1458 00:53:14,830 --> 00:53:16,359 to one and bits. 1459 00:53:16,360 --> 00:53:18,549 And I think you're checkerboard 1460 00:53:18,550 --> 00:53:20,929 detect that as entropy loss because 1461 00:53:20,930 --> 00:53:23,079 you really take two 1462 00:53:23,080 --> 00:53:25,179 end bits, compress it to one 1463 00:53:25,180 --> 00:53:27,459 and bits. And so obviously and bits 1464 00:53:27,460 --> 00:53:28,460 are lost. 1465 00:53:29,860 --> 00:53:32,289 Yeah. We assume that the seed 1466 00:53:32,290 --> 00:53:34,629 indeed is uniformly distributed 1467 00:53:34,630 --> 00:53:37,869 in um well in whatever 1468 00:53:37,870 --> 00:53:40,089 a lengthy test so that there's 1469 00:53:40,090 --> 00:53:41,529 a hardware entropy source. 1470 00:53:41,530 --> 00:53:43,989 It doesn't have this uniform distribution 1471 00:53:43,990 --> 00:53:45,909 and by compressing it with a hash 1472 00:53:45,910 --> 00:53:48,519 function, you get a uniform 1473 00:53:48,520 --> 00:53:49,659 distribution. 1474 00:53:49,660 --> 00:53:51,999 And that's the first step to 1475 00:53:52,000 --> 00:53:54,639 send you expand from the uniform, 1476 00:53:54,640 --> 00:53:56,289 from the compressed version. 1477 00:53:56,290 --> 00:53:58,779 And then so you have to 1478 00:53:58,780 --> 00:54:00,849 be careful of them using your check 1479 00:54:00,850 --> 00:54:03,099 because the input is 1480 00:54:03,100 --> 00:54:05,829 not completely uniformly distributed 1481 00:54:05,830 --> 00:54:08,439 mostly, but not perfectly 1482 00:54:08,440 --> 00:54:10,509 ancestors', because hardwares, 1483 00:54:10,510 --> 00:54:12,579 analog design and you have offsets 1484 00:54:12,580 --> 00:54:13,509 and things like that. 1485 00:54:13,510 --> 00:54:16,179 The other thing I did of 1486 00:54:16,180 --> 00:54:18,339 checking excuse me, 1487 00:54:18,340 --> 00:54:21,429 please come to the question is 1488 00:54:21,430 --> 00:54:23,559 when you have something like this 1489 00:54:23,560 --> 00:54:25,239 is a problem. 1490 00:54:25,240 --> 00:54:27,609 I write the first 1491 00:54:27,610 --> 00:54:30,249 round of the first 32 1492 00:54:30,250 --> 00:54:32,499 bytes into a file and I check 1493 00:54:32,500 --> 00:54:35,199 each time I initialize my 1494 00:54:35,200 --> 00:54:37,269 fiancee and I check if 1495 00:54:37,270 --> 00:54:40,089 that pattern has been set before 1496 00:54:40,090 --> 00:54:42,199 and due to the birthday paradoxal, 1497 00:54:42,200 --> 00:54:44,469 if I reduce my 1498 00:54:44,470 --> 00:54:46,779 initial seed, I 1499 00:54:46,780 --> 00:54:48,339 get to the square root. 1500 00:54:48,340 --> 00:54:50,619 So then I have this 1501 00:54:50,620 --> 00:54:53,199 problem. I would have after, 1502 00:54:53,200 --> 00:54:55,569 uh, two hundred fifty 1503 00:54:55,570 --> 00:54:57,639 six iterations, I would 1504 00:54:57,640 --> 00:55:00,209 have a 50 percent chance to see 1505 00:55:00,210 --> 00:55:01,449 that I have a problem. 1506 00:55:03,520 --> 00:55:05,499 Yeah, yeah. But we showed, for example, 1507 00:55:05,500 --> 00:55:07,069 the harmony problem. 1508 00:55:07,070 --> 00:55:09,279 Yeah. And the margins are much bigger. 1509 00:55:09,280 --> 00:55:11,619 So they are 70 after 1510 00:55:11,620 --> 00:55:12,729 to kick up. 1511 00:55:12,730 --> 00:55:13,719 Yeah. 1512 00:55:13,720 --> 00:55:16,149 But if every user does this, check 1513 00:55:16,150 --> 00:55:18,219 every user a chance to 1514 00:55:18,220 --> 00:55:20,559 see it is pretty 1515 00:55:20,560 --> 00:55:21,560 good. 1516 00:55:23,470 --> 00:55:25,019 OK, the other one on the right please. 1517 00:55:28,260 --> 00:55:30,599 I am so at some point you talk 1518 00:55:30,600 --> 00:55:32,759 about, uh, checking the, um, 1519 00:55:32,760 --> 00:55:35,129 the generation by simplifying 1520 00:55:35,130 --> 00:55:36,129 the hash function. 1521 00:55:36,130 --> 00:55:37,949 So, for example, you talked about 1522 00:55:37,950 --> 00:55:40,769 replacing one with 1523 00:55:40,770 --> 00:55:41,819 Mohapi. 1524 00:55:41,820 --> 00:55:44,039 So I was wondering, you said 1525 00:55:44,040 --> 00:55:46,259 that some implementations, 1526 00:55:46,260 --> 00:55:49,109 um, could, um, 1527 00:55:49,110 --> 00:55:51,619 outputs, um, like 1528 00:55:51,620 --> 00:55:53,699 the C material in the 1529 00:55:53,700 --> 00:55:55,909 output when you use Mkapa. 1530 00:55:55,910 --> 00:55:57,929 Do you have any examples of that, like in 1531 00:55:57,930 --> 00:56:00,299 real punji implementations 1532 00:56:00,300 --> 00:56:01,739 of, for example, openness as well? 1533 00:56:01,740 --> 00:56:02,740 We'll do that. 1534 00:56:03,750 --> 00:56:05,489 OK. And then to make it clear, this is 1535 00:56:05,490 --> 00:56:07,679 just for for analysis purposes here, this 1536 00:56:07,680 --> 00:56:08,559 is, uh. 1537 00:56:08,560 --> 00:56:09,560 Yeah. 1538 00:56:10,620 --> 00:56:12,689 Uh, both on the left. 1539 00:56:12,690 --> 00:56:14,919 Um, I'm very happy to see more 1540 00:56:14,920 --> 00:56:17,069 formal methods, informal verification 1541 00:56:17,070 --> 00:56:18,959 popping up and making this useable. 1542 00:56:18,960 --> 00:56:20,369 So thank you for that. 1543 00:56:20,370 --> 00:56:22,499 And my question is, you said 1544 00:56:22,500 --> 00:56:24,629 that you can trace the Entropia, you 1545 00:56:24,630 --> 00:56:27,389 can trace the changes in state or 1546 00:56:27,390 --> 00:56:29,819 in the production function. 1547 00:56:29,820 --> 00:56:31,649 Um, how does this actually work? 1548 00:56:31,650 --> 00:56:34,139 Is this a feature of the C proof 1549 00:56:34,140 --> 00:56:36,269 stuff you used or did you implement 1550 00:56:36,270 --> 00:56:38,399 it? And how can you actually. 1551 00:56:38,400 --> 00:56:40,529 Well, go ahead and trace 1552 00:56:40,530 --> 00:56:42,599 where my entropy gets lost. 1553 00:56:42,600 --> 00:56:43,859 How does this work? 1554 00:56:43,860 --> 00:56:46,139 You show the other 1555 00:56:46,140 --> 00:56:48,809 the seapower and models 1556 00:56:48,810 --> 00:56:50,939 the whole state of your program. 1557 00:56:50,940 --> 00:56:53,489 And so every every position 1558 00:56:53,490 --> 00:56:55,709 where the the seed is used 1559 00:56:55,710 --> 00:56:57,809 are variables in the logic of formula 1560 00:56:57,810 --> 00:57:00,689 that C approver outputs. 1561 00:57:00,690 --> 00:57:02,999 And that way, uh, 1562 00:57:03,000 --> 00:57:04,229 that that tracks the data. 1563 00:57:04,230 --> 00:57:06,359 OK, but is this part of the of the 1564 00:57:06,360 --> 00:57:08,579 C approver or did you add this 1565 00:57:08,580 --> 00:57:09,389 to. 1566 00:57:09,390 --> 00:57:12,509 I think this is a slightly different 1567 00:57:12,510 --> 00:57:14,639 point. Uh, this is not part 1568 00:57:14,640 --> 00:57:16,199 of this approver. This is actually 1569 00:57:16,200 --> 00:57:18,269 something that we do 1570 00:57:18,270 --> 00:57:20,639 after the supernova analysis 1571 00:57:20,640 --> 00:57:23,939 has, uh, terminated 1572 00:57:23,940 --> 00:57:26,489 because. Well, what we do get is we get 1573 00:57:26,490 --> 00:57:28,559 the model of the formula and we extract 1574 00:57:28,560 --> 00:57:30,359 the actual seeds that exhibit the 1575 00:57:30,360 --> 00:57:32,669 problem. And then we run 1576 00:57:32,670 --> 00:57:34,439 the pairing with these two seeds. 1577 00:57:34,440 --> 00:57:37,199 And, uh, we output 1578 00:57:37,200 --> 00:57:38,339 the intermediate states. 1579 00:57:38,340 --> 00:57:40,469 Just we we write them on the console and 1580 00:57:40,470 --> 00:57:42,119 we show you side by side. 1581 00:57:42,120 --> 00:57:44,609 And you can so you use the the 1582 00:57:44,610 --> 00:57:46,919 the variables that satisfy 1583 00:57:46,920 --> 00:57:47,920 your 1584 00:57:49,830 --> 00:57:51,989 injectivity. And then by having the 1585 00:57:51,990 --> 00:57:54,299 two two sides to break injectivity, 1586 00:57:54,300 --> 00:57:55,269 you can trace. 1587 00:57:55,270 --> 00:57:56,270 OK, yeah. 1588 00:57:58,290 --> 00:58:01,139 All right. Thanks a lot to me in Phenix. 1589 00:58:01,140 --> 00:58:02,549 Please give them some applause for this 1590 00:58:02,550 --> 00:58:03,550 one.