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/535 Thanks! 1 00:00:09,210 --> 00:00:11,459 Has any of you ever been using, like, 2 00:00:11,460 --> 00:00:14,009 formal methods or automated proof 3 00:00:14,010 --> 00:00:15,119 softwares? 4 00:00:15,120 --> 00:00:16,919 Oh, many of you. 5 00:00:16,920 --> 00:00:18,719 I find this topic super interesting 6 00:00:18,720 --> 00:00:20,849 because when I first read it, I was like, 7 00:00:20,850 --> 00:00:22,589 oh, my God, no, I'm going to prove the 8 00:00:22,590 --> 00:00:24,389 security of everything I've written so 9 00:00:24,390 --> 00:00:26,549 far. Then I realize it takes a lot of 10 00:00:26,550 --> 00:00:28,709 time and it's very difficult. 11 00:00:28,710 --> 00:00:30,569 And most of this stuff doesn't have 12 00:00:30,570 --> 00:00:33,089 Othell any kind of documentation. 13 00:00:33,090 --> 00:00:35,609 So but I mean, 14 00:00:35,610 --> 00:00:38,499 Kornelius. Or some formal method as, um, 15 00:00:38,500 --> 00:00:40,239 for for security network management. 16 00:00:40,240 --> 00:00:41,969 So I believe he will be able to tell me 17 00:00:41,970 --> 00:00:43,169 more about this. 18 00:00:43,170 --> 00:00:45,269 And in particular for this talk 19 00:00:45,270 --> 00:00:47,969 of today, he will be telling us about 20 00:00:47,970 --> 00:00:50,279 verifying properties of a portable 21 00:00:50,280 --> 00:00:51,239 firewall rules. 22 00:00:51,240 --> 00:00:53,099 So please give him a big round of 23 00:00:53,100 --> 00:00:54,100 applause. 24 00:01:00,760 --> 00:01:02,499 OK, thank you very much. 25 00:01:02,500 --> 00:01:04,238 Thank you all for getting up early and 26 00:01:04,239 --> 00:01:05,289 joining my talk. 27 00:01:05,290 --> 00:01:07,419 This talk is called Verified Firewall 28 00:01:07,420 --> 00:01:09,039 Rules and verification. 29 00:01:09,040 --> 00:01:11,139 So I think it's best to first refresh 30 00:01:11,140 --> 00:01:13,149 our knowledge about firewalls in the 31 00:01:13,150 --> 00:01:14,589 first few seconds. 32 00:01:14,590 --> 00:01:16,629 So he has a firewall rules that I found 33 00:01:16,630 --> 00:01:18,249 on a network attached storage. 34 00:01:18,250 --> 00:01:20,249 It's a Linux IP tables firewall. 35 00:01:20,250 --> 00:01:22,269 Let's just walk through that router to 36 00:01:22,270 --> 00:01:23,349 see what it does. 37 00:01:23,350 --> 00:01:25,059 So let's say we have a packet for this 38 00:01:25,060 --> 00:01:27,159 box. The packet is given to the input 39 00:01:27,160 --> 00:01:29,049 chain and the box will now walk through 40 00:01:29,050 --> 00:01:30,909 all these firewall sequentially until it 41 00:01:30,910 --> 00:01:32,799 finds a material to know what to do with 42 00:01:32,800 --> 00:01:34,479 this packet. Let's just do that for the 43 00:01:34,480 --> 00:01:36,759 sake of example so we all know 44 00:01:36,760 --> 00:01:38,529 what firewalls do. 45 00:01:38,530 --> 00:01:40,029 So this is the first rule. 46 00:01:40,030 --> 00:01:41,949 The box will look at what you see there 47 00:01:41,950 --> 00:01:43,509 on your right hand side is what we call 48 00:01:43,510 --> 00:01:45,609 the match condition. It tells you if 49 00:01:45,610 --> 00:01:47,679 this rule matches for a packet, this one 50 00:01:47,680 --> 00:01:49,779 matches for all protocols or types, 51 00:01:49,780 --> 00:01:50,799 all destination IP. 52 00:01:50,800 --> 00:01:52,029 So essentially this rule matches 53 00:01:52,030 --> 00:01:54,519 everything and then it will execute 54 00:01:54,520 --> 00:01:56,649 this action, which is called us protect, 55 00:01:56,650 --> 00:01:58,479 which means we jump to the user defined 56 00:01:58,480 --> 00:02:00,999 chain does protect, which is down there. 57 00:02:01,000 --> 00:02:03,359 And we will continue our evaluation down 58 00:02:03,360 --> 00:02:05,319 the first rule as we damage condition. 59 00:02:05,320 --> 00:02:07,449 First looks at 60 00:02:07,450 --> 00:02:09,038 ICMP protocol. 61 00:02:09,039 --> 00:02:11,169 Any source, any destination IP, ISP 62 00:02:11,170 --> 00:02:12,939 Type eight, which is an echo request, as 63 00:02:12,940 --> 00:02:15,219 we all know, and check if a certain limit 64 00:02:15,220 --> 00:02:16,539 is not exceeded. 65 00:02:16,540 --> 00:02:18,669 If this is the case, we are we will 66 00:02:18,670 --> 00:02:21,279 return. We return to where we came from. 67 00:02:21,280 --> 00:02:22,899 Otherwise we will go to the next rule. 68 00:02:22,900 --> 00:02:25,239 It looks at ICMP request again 69 00:02:25,240 --> 00:02:26,319 and drops them. 70 00:02:26,320 --> 00:02:28,209 So we see a pattern here. 71 00:02:28,210 --> 00:02:30,309 Those two rule essentially implement rate 72 00:02:30,310 --> 00:02:31,929 limiting for us. If the limit is not 73 00:02:31,930 --> 00:02:34,209 exceeded, we can go out of the 74 00:02:34,210 --> 00:02:36,429 tech giant. Otherwise things are top 75 00:02:36,430 --> 00:02:38,529 here. The same pattern we see 76 00:02:38,530 --> 00:02:40,899 here for TCP Pickett's TCP Flex. 77 00:02:40,900 --> 00:02:43,029 Obviously with that flex 78 00:02:43,030 --> 00:02:44,889 that there if a certain limit is 79 00:02:44,890 --> 00:02:46,449 exceeded, they will be dropped. 80 00:02:46,450 --> 00:02:47,889 Otherwise we can return. 81 00:02:47,890 --> 00:02:49,489 So let's say we get through the dust 82 00:02:49,490 --> 00:02:51,399 protection without being dropped. 83 00:02:51,400 --> 00:02:52,959 We end up where it came from. 84 00:02:52,960 --> 00:02:55,209 The next rule accepts 85 00:02:55,210 --> 00:02:56,709 all tickets which belong to an 86 00:02:56,710 --> 00:02:58,989 established or related connection. 87 00:02:58,990 --> 00:03:00,819 Accepting everything that belongs to an 88 00:03:00,820 --> 00:03:02,079 established connection is usually 89 00:03:02,080 --> 00:03:04,419 considered best practice opinions differ 90 00:03:04,420 --> 00:03:07,119 on the related match. 91 00:03:07,120 --> 00:03:08,799 Well, the interesting question is how do 92 00:03:08,800 --> 00:03:10,719 we get a connection in an established 93 00:03:10,720 --> 00:03:12,849 state? Well, this is what most of the 94 00:03:12,850 --> 00:03:15,099 rules of a firewall are about. 95 00:03:15,100 --> 00:03:17,109 So how do we get in and establish state 96 00:03:17,110 --> 00:03:18,099 for this firewall? 97 00:03:18,100 --> 00:03:19,899 Well, not for us as packets. 98 00:03:19,900 --> 00:03:22,059 They are blocked. Also, a lot more TCP 99 00:03:22,060 --> 00:03:23,649 ports are blocked. 100 00:03:23,650 --> 00:03:25,599 Also a lot more. UDP ports are blocked. 101 00:03:25,600 --> 00:03:27,399 Finally, the firewall is accepting 102 00:03:27,400 --> 00:03:29,649 something. It's accepting all packets 103 00:03:29,650 --> 00:03:31,809 with a source IP address in the local 192 104 00:03:31,810 --> 00:03:34,149 one sixty eight zero range and 105 00:03:34,150 --> 00:03:35,769 it's dropping everything else. 106 00:03:35,770 --> 00:03:37,779 OK, I hope by now we have refreshed our 107 00:03:37,780 --> 00:03:39,759 knowledge about firewalls. 108 00:03:39,760 --> 00:03:42,759 So what's the problem with firewalls? 109 00:03:42,760 --> 00:03:44,979 Well, I guess everyone in this room loves 110 00:03:44,980 --> 00:03:47,019 open source solutions, so we don't have 111 00:03:47,020 --> 00:03:48,819 to care about pectus and proprietary 112 00:03:48,820 --> 00:03:50,589 software. We also don't have to care 113 00:03:50,590 --> 00:03:52,539 about global infrastructure security made 114 00:03:52,540 --> 00:03:53,469 in Germany. 115 00:03:53,470 --> 00:03:55,449 We love our open source firewalls to 116 00:03:55,450 --> 00:03:57,069 Linux, our firewalls. 117 00:03:57,070 --> 00:03:58,239 They are quite good. 118 00:03:58,240 --> 00:03:59,469 So what's the main problem? 119 00:03:59,470 --> 00:04:01,869 Well, there was a study that looked at 120 00:04:01,870 --> 00:04:03,999 real world enterprise firewall out 121 00:04:04,000 --> 00:04:05,739 there in the wild and the study found, 122 00:04:05,740 --> 00:04:08,349 well, there are no good high complexity 123 00:04:08,350 --> 00:04:10,239 rule sets. So the main problem of 124 00:04:10,240 --> 00:04:12,309 firewalls is administrating 125 00:04:12,310 --> 00:04:14,109 them, setting them up, which all comes 126 00:04:14,110 --> 00:04:16,268 down to configuring the ruleset 127 00:04:16,269 --> 00:04:17,169 for the firewalls. 128 00:04:17,170 --> 00:04:19,239 And, well, a few if you were laughing 129 00:04:19,240 --> 00:04:20,799 that was that we saw on the slide before 130 00:04:20,800 --> 00:04:21,849 was actually quite simple. 131 00:04:21,850 --> 00:04:24,789 Just imagine those sets get larger. 132 00:04:24,790 --> 00:04:26,919 Study repeated this 133 00:04:26,920 --> 00:04:29,079 finding a few 134 00:04:29,080 --> 00:04:30,729 years later and it still finds real 135 00:04:30,730 --> 00:04:32,379 firewalls are still poorly configured. 136 00:04:32,380 --> 00:04:34,519 So it's all about the firewall rules, 137 00:04:34,520 --> 00:04:36,489 sets that well, if the rules get 138 00:04:36,490 --> 00:04:37,989 complicated, we make errors. 139 00:04:37,990 --> 00:04:39,999 And by no means do I mean that 140 00:04:40,000 --> 00:04:42,069 administrators are incompetent. 141 00:04:42,070 --> 00:04:43,899 No, thank you very much to all those 142 00:04:43,900 --> 00:04:46,269 masters of complexity who get our network 143 00:04:46,270 --> 00:04:47,919 running. Thank you to the NOC for 144 00:04:47,920 --> 00:04:48,699 everything. 145 00:04:48,700 --> 00:04:50,559 Thank you for not filing us here so we 146 00:04:50,560 --> 00:04:51,560 can have more fun. 147 00:04:52,720 --> 00:04:55,419 So it's all the configuration 148 00:04:55,420 --> 00:04:57,159 of the firewall. So people had idea, 149 00:04:57,160 --> 00:04:59,109 well, let's just write a few tools that 150 00:04:59,110 --> 00:05:01,149 check our firewall rules and tell if the 151 00:05:01,150 --> 00:05:02,589 rules and is good. 152 00:05:02,590 --> 00:05:04,569 People had that idea and we looked at the 153 00:05:04,570 --> 00:05:06,039 tools that were out there. 154 00:05:06,040 --> 00:05:08,319 So we fed those tools, some 155 00:05:08,320 --> 00:05:10,269 real world firewall routers and we found, 156 00:05:10,270 --> 00:05:12,459 well, there's essentially no tool 157 00:05:12,460 --> 00:05:14,679 out there that understands our real world 158 00:05:14,680 --> 00:05:16,839 firewalls, because if you ever open men 159 00:05:16,840 --> 00:05:18,609 IP davits extension's, well, then you 160 00:05:18,610 --> 00:05:20,199 understand why things can get very 161 00:05:20,200 --> 00:05:21,250 complicated there. 162 00:05:22,450 --> 00:05:24,189 So and even if we had a tool that would 163 00:05:24,190 --> 00:05:26,389 check our firewall, said, would we trust 164 00:05:26,390 --> 00:05:29,589 the tool? Well, probably not. 165 00:05:29,590 --> 00:05:31,689 So let's do where others 166 00:05:31,690 --> 00:05:32,769 fail. Let's try again. 167 00:05:32,770 --> 00:05:34,719 Let's try to write a tool to check 168 00:05:34,720 --> 00:05:36,129 firewall ruleset. 169 00:05:36,130 --> 00:05:38,259 But because we found our tools, 170 00:05:38,260 --> 00:05:39,849 we have so far do not understand our 171 00:05:39,850 --> 00:05:41,679 ruleset. Let's start from the very 172 00:05:41,680 --> 00:05:43,329 beginning. Let's first talk about 173 00:05:43,330 --> 00:05:45,249 specification and implementation. 174 00:05:45,250 --> 00:05:46,779 When we mean implementation, we are 175 00:05:46,780 --> 00:05:48,969 usually talking about the code, about 176 00:05:48,970 --> 00:05:49,959 our tool. 177 00:05:49,960 --> 00:05:51,939 We talk about low level hacks to increase 178 00:05:51,940 --> 00:05:53,769 the performance of our tool all the on 179 00:05:53,770 --> 00:05:55,719 the right hand side. And this is usually 180 00:05:55,720 --> 00:05:57,789 the stuff you don't show to your users, 181 00:05:57,790 --> 00:05:58,869 to your users. 182 00:05:58,870 --> 00:06:00,499 You show them the specif. 183 00:06:00,500 --> 00:06:02,329 Or the documentation or just a question, 184 00:06:02,330 --> 00:06:03,740 what does your tool do? 185 00:06:04,940 --> 00:06:06,799 So here we are to right at what we have 186 00:06:06,800 --> 00:06:08,389 to answer the question, what is the 187 00:06:08,390 --> 00:06:10,549 correct rule said and for the 188 00:06:10,550 --> 00:06:12,649 sake of example, for this talk, we 189 00:06:12,650 --> 00:06:14,539 will stick to spoofing protection. 190 00:06:14,540 --> 00:06:16,669 So our ultimate goal will be 191 00:06:16,670 --> 00:06:18,589 a tool that checks if our firewall rules, 192 00:06:18,590 --> 00:06:20,149 that has proven protection. 193 00:06:20,150 --> 00:06:21,409 We only have 30 minutes. 194 00:06:21,410 --> 00:06:23,170 So let's stick to spoofing protection. 195 00:06:24,350 --> 00:06:26,569 But before we can specify what spoofing 196 00:06:26,570 --> 00:06:28,429 protection actually means, well, we need 197 00:06:28,430 --> 00:06:30,679 to specify what is a firewall 198 00:06:30,680 --> 00:06:32,779 and therefore we need a model of the 199 00:06:32,780 --> 00:06:34,669 packet filtering of IP tables. 200 00:06:34,670 --> 00:06:36,409 And that model is the firewall in the 201 00:06:36,410 --> 00:06:37,849 beginning should really, really be 202 00:06:37,850 --> 00:06:40,069 expressive so that we can really say, 203 00:06:40,070 --> 00:06:42,049 well, if this model mirrors reality and 204 00:06:42,050 --> 00:06:44,119 we can get all our complex firewalls 205 00:06:44,120 --> 00:06:46,279 with all the fancy IP tables matching 206 00:06:46,280 --> 00:06:48,529 extensions into that model 207 00:06:48,530 --> 00:06:50,779 so we can in the end run our tool that 208 00:06:50,780 --> 00:06:53,239 checks. If we are spoofing protection, 209 00:06:53,240 --> 00:06:54,949 we will implement everything in the eyes 210 00:06:54,950 --> 00:06:56,359 of a theorem improver. 211 00:06:56,360 --> 00:06:57,919 Why are we using a tier improver? 212 00:06:57,920 --> 00:07:00,439 Well, you know, the good old problem, 213 00:07:00,440 --> 00:07:02,479 you look up the documentation of some 214 00:07:02,480 --> 00:07:04,489 library you are using, then you look to 215 00:07:04,490 --> 00:07:05,809 the implementation and you found, well, 216 00:07:05,810 --> 00:07:08,209 the documentation was just plain lying 217 00:07:08,210 --> 00:07:09,889 to you because documentation are usually 218 00:07:09,890 --> 00:07:11,659 horribly out of date. 219 00:07:11,660 --> 00:07:13,549 So in this talk, we want to write an 220 00:07:13,550 --> 00:07:15,289 implementation and improve that 221 00:07:15,290 --> 00:07:16,969 implementation corresponds to the 222 00:07:16,970 --> 00:07:18,209 specification. 223 00:07:18,210 --> 00:07:20,479 That's why we are using a theorem proven 224 00:07:20,480 --> 00:07:22,729 to have a proof in the very end that our 225 00:07:22,730 --> 00:07:24,919 code really does what it is specified 226 00:07:24,920 --> 00:07:25,849 to do. 227 00:07:25,850 --> 00:07:27,679 So the most important thing here is to 228 00:07:27,680 --> 00:07:30,109 specify what it should do. 229 00:07:30,110 --> 00:07:32,509 So to summarize what we're talking 230 00:07:32,510 --> 00:07:34,789 about, we are verifier for ruleset 231 00:07:34,790 --> 00:07:37,849 and we will verify the verifier itself. 232 00:07:37,850 --> 00:07:39,889 So let's get started with step one. 233 00:07:39,890 --> 00:07:42,049 We need a model for IP tables 234 00:07:42,050 --> 00:07:44,380 before we can specify anything. 235 00:07:45,830 --> 00:07:48,439 OK, we so we need to match expression's. 236 00:07:48,440 --> 00:07:49,399 Let's start simple. 237 00:07:49,400 --> 00:07:51,169 Let's write down the syntax of match 238 00:07:51,170 --> 00:07:52,159 expressions. 239 00:07:52,160 --> 00:07:54,319 The syntax is all about how do I write 240 00:07:54,320 --> 00:07:56,329 things down there. 241 00:07:56,330 --> 00:07:59,359 Let's define a data type LECG expression 242 00:07:59,360 --> 00:08:01,819 and this data type should be polymorphic 243 00:08:01,820 --> 00:08:04,099 over the type apostrophe A, which 244 00:08:04,100 --> 00:08:06,289 means this apostrophe A can be 245 00:08:06,290 --> 00:08:07,849 any type who will call this the 246 00:08:07,850 --> 00:08:10,039 primitive, which will be the features 247 00:08:10,040 --> 00:08:11,679 IP tables can match on. 248 00:08:11,680 --> 00:08:14,599 Let's keep that generic for a moment. 249 00:08:14,600 --> 00:08:17,029 So how can I match expression 250 00:08:17,030 --> 00:08:19,159 then be constructed where we can match 251 00:08:19,160 --> 00:08:21,289 on such a primitive we can have a match 252 00:08:21,290 --> 00:08:22,969 expression that just matches playing 253 00:08:22,970 --> 00:08:25,159 anything, we can negate 254 00:08:25,160 --> 00:08:27,529 a match expression or we can combine 255 00:08:27,530 --> 00:08:29,569 to match expression to one larger match 256 00:08:29,570 --> 00:08:30,859 expression. 257 00:08:30,860 --> 00:08:33,168 As an example, we are combining to match 258 00:08:33,169 --> 00:08:34,879 expression with this match and 259 00:08:35,919 --> 00:08:37,979 and there we see in the thing. 260 00:08:37,980 --> 00:08:39,499 These are the primitives. 261 00:08:39,500 --> 00:08:41,479 So those things we keep completely 262 00:08:41,480 --> 00:08:42,529 arbitrary. 263 00:08:42,530 --> 00:08:44,419 Here we are meeting on destination IP and 264 00:08:44,420 --> 00:08:46,639 protocol. Tsipi And again, 265 00:08:46,640 --> 00:08:48,049 we will keep all these primitives. 266 00:08:48,050 --> 00:08:49,189 The features we can match aren't 267 00:08:49,190 --> 00:08:50,809 completely generic. 268 00:08:50,810 --> 00:08:52,789 This was the syntax how we can write 269 00:08:52,790 --> 00:08:55,429 things down. But what does this mean? 270 00:08:55,430 --> 00:08:57,369 So we have to specify the semantic 271 00:08:57,370 --> 00:08:58,939 semantics is all about what to match. 272 00:08:58,940 --> 00:09:00,079 Expressions mean. 273 00:09:00,080 --> 00:09:01,879 Well, match expressions are matching on 274 00:09:01,880 --> 00:09:03,619 packets, so we can't specify the 275 00:09:03,620 --> 00:09:05,419 semantics without a picket. 276 00:09:05,420 --> 00:09:07,129 Let's look at the type signature of the 277 00:09:07,130 --> 00:09:08,989 matching semantics first. 278 00:09:08,990 --> 00:09:10,909 There it is. Looks a bit intimidating for 279 00:09:10,910 --> 00:09:13,009 us. Let's look at what we have to. 280 00:09:13,010 --> 00:09:14,959 The first parameter of this Metrowest 281 00:09:14,960 --> 00:09:17,299 function is a function itself. 282 00:09:17,300 --> 00:09:19,399 We call it Gummo and we 283 00:09:19,400 --> 00:09:21,649 also call it a primitive measure 284 00:09:21,650 --> 00:09:22,790 because look at the type 285 00:09:23,840 --> 00:09:24,979 of the function. 286 00:09:24,980 --> 00:09:27,319 The first parameter is the primitive, 287 00:09:27,320 --> 00:09:29,089 some primitive match thing. 288 00:09:29,090 --> 00:09:30,709 We can mention, for example, two types of 289 00:09:30,710 --> 00:09:31,699 protocol. 290 00:09:31,700 --> 00:09:34,009 The second apostrophe P is A 291 00:09:34,010 --> 00:09:36,229 is the packet it should match on by 292 00:09:36,230 --> 00:09:37,909 the apostrophe. You see, we also have a 293 00:09:37,910 --> 00:09:39,349 generic packet model. 294 00:09:39,350 --> 00:09:41,539 You can plug in anything and it returns 295 00:09:41,540 --> 00:09:43,699 a boolean, true or false and well, 296 00:09:43,700 --> 00:09:46,099 dysfunction. Gamma should return true 297 00:09:46,100 --> 00:09:48,289 if and only if this primitive match 298 00:09:48,290 --> 00:09:50,569 condition matches for our packet. 299 00:09:50,570 --> 00:09:52,909 The second parameter for our semantics 300 00:09:52,910 --> 00:09:55,039 is a match expression as we defined it 301 00:09:55,040 --> 00:09:56,119 before. 302 00:09:56,120 --> 00:09:57,739 Then we give it the packet. 303 00:09:57,740 --> 00:10:00,049 We want to know if it matches and returns 304 00:10:00,050 --> 00:10:02,359 true if and only if the packet matches 305 00:10:02,360 --> 00:10:03,769 for the match expression. 306 00:10:03,770 --> 00:10:05,749 So let's look at the individual words 307 00:10:05,750 --> 00:10:06,649 here. 308 00:10:06,650 --> 00:10:08,969 First rule and 309 00:10:08,970 --> 00:10:10,879 straightforward. If we match on the 310 00:10:10,880 --> 00:10:13,189 primitive A for a packet P 311 00:10:13,190 --> 00:10:15,799 well we just ask our primitive Metcher 312 00:10:15,800 --> 00:10:18,229 if there's a match for packet P, 313 00:10:19,490 --> 00:10:22,189 then the next very straightforward 314 00:10:22,190 --> 00:10:24,019 match. Any major expression matches 315 00:10:24,020 --> 00:10:26,209 everything if we have this 316 00:10:26,210 --> 00:10:28,129 match not, which means we negate our 317 00:10:28,130 --> 00:10:29,899 image, expression and image. 318 00:10:29,900 --> 00:10:31,909 And you might already have guessed it as 319 00:10:31,910 --> 00:10:33,499 just a conjunction of the two match 320 00:10:33,500 --> 00:10:34,669 expressions. 321 00:10:34,670 --> 00:10:36,529 So now we have defined syntax and 322 00:10:36,530 --> 00:10:38,779 semantics of match expressions so we can 323 00:10:38,780 --> 00:10:39,799 match on packets. 324 00:10:39,800 --> 00:10:42,019 No, we only need to specify the filtering 325 00:10:42,020 --> 00:10:44,329 behavior of IP tables 326 00:10:44,330 --> 00:10:44,599 there. 327 00:10:44,600 --> 00:10:46,979 It is quite simple, 328 00:10:46,980 --> 00:10:47,980 first of all. 329 00:10:52,260 --> 00:10:54,119 First of all, what the fuck? 330 00:10:54,120 --> 00:10:56,639 So the good news about this is, 331 00:10:56,640 --> 00:10:58,799 well, this is really everything we need 332 00:10:58,800 --> 00:11:00,839 to know about IP tables, packet 333 00:11:00,840 --> 00:11:02,889 filtering. It's on one slide. 334 00:11:02,890 --> 00:11:04,469 If we have enough time, we could really 335 00:11:04,470 --> 00:11:06,369 read it. It's much more concise than the 336 00:11:06,370 --> 00:11:07,589 main pages. 337 00:11:07,590 --> 00:11:09,599 Well, it just has a few funny symbols on 338 00:11:09,600 --> 00:11:11,179 it. Let's try to read it. 339 00:11:12,180 --> 00:11:13,679 Everything we have to look at the 340 00:11:13,680 --> 00:11:15,149 following. 341 00:11:15,150 --> 00:11:16,619 Maybe we can recognize something. 342 00:11:16,620 --> 00:11:18,719 P should be the packet the firewall 343 00:11:18,720 --> 00:11:19,769 is examining there. 344 00:11:19,770 --> 00:11:21,329 We have to gamma again or a primitive 345 00:11:21,330 --> 00:11:23,099 measure which has encoded all the 346 00:11:23,100 --> 00:11:24,839 features IP tables can match on. 347 00:11:26,190 --> 00:11:28,439 Then at this position we have to 348 00:11:28,440 --> 00:11:30,809 set the rules. It is just a list of rules 349 00:11:30,810 --> 00:11:33,689 the firewall is currently examining. 350 00:11:33,690 --> 00:11:35,369 As should be the start state. 351 00:11:35,370 --> 00:11:37,409 The firewall starts looking at the 352 00:11:37,410 --> 00:11:39,029 packet. Usually the firewall in the 353 00:11:39,030 --> 00:11:41,039 beginning is undecided about what to do 354 00:11:41,040 --> 00:11:43,169 with the packet and at 355 00:11:43,170 --> 00:11:44,789 the end we have the final stage. 356 00:11:44,790 --> 00:11:46,649 So in the end, the firewall usually makes 357 00:11:46,650 --> 00:11:48,839 a decision either to accept or to drop 358 00:11:48,840 --> 00:11:49,919 a packet. 359 00:11:49,920 --> 00:11:52,229 So let's read the rules. 360 00:11:52,230 --> 00:11:54,029 Let's read a simple rule, skip rule, they 361 00:11:54,030 --> 00:11:55,979 are all written with this line, which 362 00:11:55,980 --> 00:11:57,959 means everything above the line is to 363 00:11:57,960 --> 00:11:59,879 preconditioning everything below the line 364 00:11:59,880 --> 00:12:02,039 is the conclusion here we don't 365 00:12:02,040 --> 00:12:04,229 have any preconditions or this rule holds 366 00:12:04,230 --> 00:12:06,089 unconditionally. 367 00:12:06,090 --> 00:12:09,089 So let's read what this means. 368 00:12:09,090 --> 00:12:10,349 There we have it. 369 00:12:10,350 --> 00:12:12,599 First of all, this rule looks 370 00:12:12,600 --> 00:12:15,029 at the empty rules that the empty list. 371 00:12:15,030 --> 00:12:16,859 So what does a firewall of the empty 372 00:12:16,860 --> 00:12:19,079 rules that to the rule says 373 00:12:19,080 --> 00:12:21,119 the start date and the final state are 374 00:12:21,120 --> 00:12:23,069 the same. So essentially, this rule says 375 00:12:23,070 --> 00:12:25,349 for the empty rules that a firewall does 376 00:12:25,350 --> 00:12:27,449 nothing, not really that 377 00:12:27,450 --> 00:12:29,609 hard, but we need to state we 378 00:12:29,610 --> 00:12:31,469 need to start at some point. 379 00:12:31,470 --> 00:12:33,419 Let's look at a quite more complicated 380 00:12:33,420 --> 00:12:34,799 rule here. 381 00:12:34,800 --> 00:12:37,119 We also have a precondition. 382 00:12:37,120 --> 00:12:39,369 And what we are looking at is a ruleset 383 00:12:39,370 --> 00:12:41,949 which only consists of one single rule, 384 00:12:41,950 --> 00:12:43,629 which has some match condition and 385 00:12:43,630 --> 00:12:46,419 direction is except our precondition 386 00:12:46,420 --> 00:12:48,639 is that we assume that the match 387 00:12:48,640 --> 00:12:51,399 condition matches for the packet. 388 00:12:51,400 --> 00:12:53,829 Well, what would then happen to Actionis 389 00:12:53,830 --> 00:12:55,719 except for two to five, will do well if 390 00:12:55,720 --> 00:12:57,459 we don't have a decision for the packet 391 00:12:57,460 --> 00:12:59,649 yet. The action was accept, then 392 00:12:59,650 --> 00:13:01,579 we are going to accept it. 393 00:13:01,580 --> 00:13:03,639 OK, also not that 394 00:13:03,640 --> 00:13:05,239 hard. 395 00:13:05,240 --> 00:13:07,129 And I guess we all agree that this is the 396 00:13:07,130 --> 00:13:09,569 behavior of our common firewalled. 397 00:13:09,570 --> 00:13:11,459 So all the other routes they actually 398 00:13:11,460 --> 00:13:13,649 read pretty similar, and we only have 11 399 00:13:13,650 --> 00:13:15,479 of them, so if we have enough time, it's 400 00:13:15,480 --> 00:13:17,819 not that hard to read like 401 00:13:17,820 --> 00:13:18,899 you were first laughing at. 402 00:13:18,900 --> 00:13:20,879 So let's directly jump to the most 403 00:13:20,880 --> 00:13:22,179 complicated route we have to. 404 00:13:22,180 --> 00:13:24,139 And our view is that it's critical 405 00:13:24,140 --> 00:13:25,140 return. 406 00:13:26,400 --> 00:13:28,349 Well, looks a bit complicated. 407 00:13:28,350 --> 00:13:29,350 It is. 408 00:13:29,880 --> 00:13:31,949 So first again, we have a route 409 00:13:31,950 --> 00:13:34,139 with a single rule, with some 410 00:13:34,140 --> 00:13:35,039 policy there. 411 00:13:35,040 --> 00:13:37,169 And our first precondition is this 412 00:13:37,170 --> 00:13:38,849 one rule matches otherwise to five. 413 00:13:38,850 --> 00:13:40,350 I would not do anything at all. 414 00:13:41,730 --> 00:13:43,419 Then there is the complicated part. 415 00:13:43,420 --> 00:13:45,059 The action of the rule recorded are 416 00:13:45,060 --> 00:13:47,159 called SI, which means we want 417 00:13:47,160 --> 00:13:49,739 to call or jump minus Jakobson 418 00:13:49,740 --> 00:13:51,959 and IP tables to some user defined 419 00:13:51,960 --> 00:13:54,119 chain. The name of the chain 420 00:13:54,120 --> 00:13:56,189 here is generically expressed 421 00:13:56,190 --> 00:13:58,679 as C in the example from the beginning, 422 00:13:58,680 --> 00:14:00,749 for example, the C was the 423 00:14:00,750 --> 00:14:02,039 name does protect. 424 00:14:03,450 --> 00:14:05,699 And we also have as a precondition 425 00:14:05,700 --> 00:14:06,700 that 426 00:14:07,950 --> 00:14:09,869 chain and the background rules, it looks 427 00:14:09,870 --> 00:14:12,029 as follows. So we have the capital gang 428 00:14:12,030 --> 00:14:14,249 out there of C, which basically means 429 00:14:14,250 --> 00:14:16,379 look up in the background of 430 00:14:16,380 --> 00:14:19,109 all the user defined chain and 431 00:14:19,110 --> 00:14:21,989 how the chain of this rule, 432 00:14:21,990 --> 00:14:24,329 how the chain food 433 00:14:24,330 --> 00:14:26,969 chain with the name C looks like. 434 00:14:26,970 --> 00:14:29,069 But so essentially we get what 435 00:14:29,070 --> 00:14:30,779 is in the dust protect chain for the 436 00:14:31,890 --> 00:14:34,499 sorry for the example from the beginning. 437 00:14:34,500 --> 00:14:36,299 And here we say, well it looks the 438 00:14:36,300 --> 00:14:38,639 following first years Rs1 then there's 439 00:14:38,640 --> 00:14:40,589 no return and then there is ours too, 440 00:14:40,590 --> 00:14:42,719 which means well this user 441 00:14:42,720 --> 00:14:44,099 defined chain can look as follows. 442 00:14:44,100 --> 00:14:46,439 First, there is an arbitrary part called 443 00:14:46,440 --> 00:14:48,689 Rs1. An arbitrary amount of goods could, 444 00:14:48,690 --> 00:14:50,849 for example, be the first ICMP 445 00:14:50,850 --> 00:14:53,339 rules we saw in the chain. 446 00:14:53,340 --> 00:14:55,499 Then there is a rule 447 00:14:55,500 --> 00:14:57,179 which has an action of return and then 448 00:14:57,180 --> 00:14:59,489 there can be more arbitrary rules called 449 00:14:59,490 --> 00:15:01,499 RS2 can be an arbitrary long list of 450 00:15:01,500 --> 00:15:02,500 other rules. 451 00:15:03,170 --> 00:15:05,239 OK, then we have the 452 00:15:05,240 --> 00:15:07,579 next precondition, it says we 453 00:15:07,580 --> 00:15:10,049 can process this first part, ours 454 00:15:10,050 --> 00:15:12,199 one without getting 455 00:15:12,200 --> 00:15:13,099 a decision. 456 00:15:13,100 --> 00:15:15,199 So so far we have called to a user 457 00:15:15,200 --> 00:15:17,599 defined chain, have processed our first 458 00:15:17,600 --> 00:15:19,849 part of this chain without getting 459 00:15:19,850 --> 00:15:22,309 any decision yet. 460 00:15:22,310 --> 00:15:24,349 Then there's the next assumption. 461 00:15:24,350 --> 00:15:26,719 We have a matching return. 462 00:15:26,720 --> 00:15:29,509 So what does happen there in IP tables? 463 00:15:29,510 --> 00:15:31,609 So we are called to a user defined chain. 464 00:15:31,610 --> 00:15:33,319 We have processed something, didn't get a 465 00:15:33,320 --> 00:15:35,609 result. Then we got a matching return 466 00:15:35,610 --> 00:15:37,579 route. So we came back to where we 467 00:15:37,580 --> 00:15:40,099 started from without any result. 468 00:15:40,100 --> 00:15:42,439 And this is what the rule tells us. 469 00:15:42,440 --> 00:15:44,149 Well, I know I'm going over those 470 00:15:44,150 --> 00:15:45,859 formalism a bit very fast. 471 00:15:45,860 --> 00:15:47,779 I hope a few can follow. 472 00:15:47,780 --> 00:15:49,669 First of all, the cool thing about this, 473 00:15:49,670 --> 00:15:51,139 this is really a mathematical 474 00:15:51,140 --> 00:15:52,429 specification. It's not an 475 00:15:52,430 --> 00:15:53,569 implementation. 476 00:15:53,570 --> 00:15:54,619 And we can see that. 477 00:15:54,620 --> 00:15:56,719 We can specify the behavior, for example, 478 00:15:56,720 --> 00:15:58,399 of crawling toward returning from user 479 00:15:58,400 --> 00:16:00,499 defined chain without a college stick. 480 00:16:00,500 --> 00:16:02,929 So this is really just a specification, 481 00:16:02,930 --> 00:16:03,889 not an implementation. 482 00:16:03,890 --> 00:16:05,959 It's not executable, but hopefully 483 00:16:05,960 --> 00:16:08,359 it tells quite clear what the firewall 484 00:16:08,360 --> 00:16:09,360 does. 485 00:16:09,850 --> 00:16:12,189 Well, anyway, if I already lost 486 00:16:12,190 --> 00:16:14,499 you, I hope you can join now, because 487 00:16:14,500 --> 00:16:16,479 there's the question, why are we doing 488 00:16:16,480 --> 00:16:18,219 all this formalism? 489 00:16:18,220 --> 00:16:20,859 Well, let's get a bit more applied 490 00:16:20,860 --> 00:16:22,789 now with every and every slide we have, 491 00:16:22,790 --> 00:16:24,729 we will get more applied and we will now 492 00:16:24,730 --> 00:16:26,619 use this formalism to actually do 493 00:16:26,620 --> 00:16:28,599 something useful with it. 494 00:16:28,600 --> 00:16:30,579 Now we just have specified the filtering 495 00:16:30,580 --> 00:16:31,779 behavior of a firewall. 496 00:16:33,400 --> 00:16:35,139 OK, let's specify more, let let's read 497 00:16:35,140 --> 00:16:37,239 this formula down your left hand side 498 00:16:37,240 --> 00:16:39,399 here of behavior of a firewall, then 499 00:16:39,400 --> 00:16:40,509 we have if and only if. 500 00:16:40,510 --> 00:16:41,949 And on the right hand side, again, 501 00:16:41,950 --> 00:16:43,119 behavior for five. 502 00:16:43,120 --> 00:16:45,279 So the left hand side and right hand 503 00:16:45,280 --> 00:16:46,919 side are equal. 504 00:16:46,920 --> 00:16:48,219 OK, where's the difference? 505 00:16:48,220 --> 00:16:50,289 The difference here is this f f is a 506 00:16:50,290 --> 00:16:52,299 function which takes a router and 507 00:16:52,300 --> 00:16:54,129 transforms it to another ruleset. 508 00:16:54,130 --> 00:16:56,439 So what could this function f possibly 509 00:16:56,440 --> 00:16:58,689 do? Well, we said the behavior 510 00:16:58,690 --> 00:17:00,879 of those fireboats are equal, so 511 00:17:00,880 --> 00:17:02,829 it means that this function F takes a 512 00:17:02,830 --> 00:17:04,779 ruleset, transforms it to a different 513 00:17:04,780 --> 00:17:06,909 ruleset. But it didn't change the 514 00:17:06,910 --> 00:17:08,588 behavior of the firewall. 515 00:17:08,589 --> 00:17:10,509 So for example, F could be a function 516 00:17:10,510 --> 00:17:12,279 that improves the performance of your 517 00:17:12,280 --> 00:17:14,559 roots. It and you could safely run this 518 00:17:14,560 --> 00:17:16,299 function on your ruleset because. 519 00:17:16,300 --> 00:17:18,639 Well, they are the formula says F doesn't 520 00:17:18,640 --> 00:17:20,039 change the behavior of your firewall. 521 00:17:20,040 --> 00:17:22,929 You can safely deploy to production. 522 00:17:22,930 --> 00:17:25,149 And we have implemented several such F 523 00:17:25,150 --> 00:17:26,078 functions. 524 00:17:26,079 --> 00:17:27,459 A very simple example. 525 00:17:27,460 --> 00:17:29,619 We can remove all the logging rules 526 00:17:29,620 --> 00:17:31,419 or semantics only cares about packet 527 00:17:31,420 --> 00:17:33,579 filtering. Logging doesn't influence that 528 00:17:33,580 --> 00:17:34,719 in IP tables. 529 00:17:34,720 --> 00:17:36,309 So if we remove all the logging rules, 530 00:17:36,310 --> 00:17:38,409 the behavior of the firewall stays 531 00:17:38,410 --> 00:17:40,809 the same. OK, simple example. 532 00:17:40,810 --> 00:17:42,069 You also can do more. 533 00:17:42,070 --> 00:17:44,199 We can unfold all calls 534 00:17:44,200 --> 00:17:46,719 to and returns from user defined chains. 535 00:17:46,720 --> 00:17:48,729 So when after we have run this function 536 00:17:48,730 --> 00:17:50,829 well, the firewall will be a long 537 00:17:50,830 --> 00:17:53,239 list of rules which will already process 538 00:17:53,240 --> 00:17:55,209 sequentially. There's no more jumping 539 00:17:55,210 --> 00:17:57,189 around, which is a cruel thing. 540 00:17:57,190 --> 00:17:59,109 Unfortunately, the match conditions will 541 00:17:59,110 --> 00:18:01,449 get quite complicated for the toolset. 542 00:18:01,450 --> 00:18:03,159 But again, we can normalize these match 543 00:18:03,160 --> 00:18:05,019 conditions to simpler ones. 544 00:18:05,020 --> 00:18:06,999 So in the end we will have a firewall, 545 00:18:07,000 --> 00:18:09,279 which is just a long list of simple 546 00:18:09,280 --> 00:18:11,439 rules. There is no jumping around and 547 00:18:11,440 --> 00:18:13,809 the actions are either accept or drop 548 00:18:13,810 --> 00:18:14,949 in the end. 549 00:18:14,950 --> 00:18:16,989 So we can essentially simplify our 550 00:18:16,990 --> 00:18:18,639 firewall and to formulas as this 551 00:18:18,640 --> 00:18:20,889 simplification doesn't change the packet 552 00:18:20,890 --> 00:18:22,209 filtering behavior at all. 553 00:18:22,210 --> 00:18:23,529 So we can safely run this. 554 00:18:24,880 --> 00:18:27,009 OK, let's look at more things 555 00:18:27,010 --> 00:18:29,139 we implemented on semantics in ternary 556 00:18:29,140 --> 00:18:31,329 logic, in Boolean logic, we either have 557 00:18:31,330 --> 00:18:33,339 true or false internal logic. 558 00:18:33,340 --> 00:18:36,159 We have true, false and unknown. 559 00:18:36,160 --> 00:18:37,909 Well, what can we do with it? 560 00:18:37,910 --> 00:18:38,829 Well, cool stuff. 561 00:18:38,830 --> 00:18:40,809 Let's first read this from the let's see 562 00:18:40,810 --> 00:18:42,699 what we have there in the middle. 563 00:18:42,700 --> 00:18:43,809 In the middle. 564 00:18:43,810 --> 00:18:46,059 We have a set we have a set of 565 00:18:46,060 --> 00:18:48,009 pickets and the conditions for this 566 00:18:48,010 --> 00:18:50,079 picket as they are accepted 567 00:18:50,080 --> 00:18:51,939 by the fire where you start an undecided 568 00:18:51,940 --> 00:18:53,819 state and in the end, you accepting it. 569 00:18:53,820 --> 00:18:54,969 It's all there in the middle. 570 00:18:54,970 --> 00:18:57,279 It says we have to set off all pickets 571 00:18:57,280 --> 00:18:59,859 accepted by the firewall. 572 00:18:59,860 --> 00:19:02,049 Well, we can specify that a 573 00:19:02,050 --> 00:19:03,699 theoretical computer scientist, we 574 00:19:03,700 --> 00:19:05,109 believe in specification. 575 00:19:05,110 --> 00:19:07,179 We have specified a set of all pickets 576 00:19:07,180 --> 00:19:08,949 accepted by the firewall. 577 00:19:08,950 --> 00:19:10,239 Quite cool. 578 00:19:10,240 --> 00:19:11,699 Well. 579 00:19:11,700 --> 00:19:13,799 I guess as Hecker's, we don't believe 580 00:19:13,800 --> 00:19:15,869 in just such a set specification, which 581 00:19:15,870 --> 00:19:17,939 is standing just out there in the void, 582 00:19:17,940 --> 00:19:19,799 having no connection to reality, you 583 00:19:19,800 --> 00:19:20,919 can't even execute. 584 00:19:20,920 --> 00:19:22,679 That's it. No, that's take us. 585 00:19:22,680 --> 00:19:24,509 We also believe in running code. 586 00:19:24,510 --> 00:19:26,639 And this is what we have there in 587 00:19:26,640 --> 00:19:27,809 the states above and below. 588 00:19:27,810 --> 00:19:29,879 Above, we have an approximation, 589 00:19:29,880 --> 00:19:32,309 which is essentially a stricter version 590 00:19:32,310 --> 00:19:33,869 of the firewall. And that's important 591 00:19:33,870 --> 00:19:35,009 that we embedded the whole thing in 592 00:19:35,010 --> 00:19:36,899 ternary logic because it's quite 593 00:19:36,900 --> 00:19:39,209 impossible to implement all the matching 594 00:19:39,210 --> 00:19:41,429 features you have in IP tables in 595 00:19:41,430 --> 00:19:42,839 an analysis tool. 596 00:19:42,840 --> 00:19:45,059 And I'm not aware of any tool that 597 00:19:45,060 --> 00:19:47,339 implements to full set because 598 00:19:47,340 --> 00:19:49,049 the net filter team also adds new 599 00:19:49,050 --> 00:19:51,239 features with many releases. 600 00:19:51,240 --> 00:19:53,729 So here we have an approximation embedded 601 00:19:53,730 --> 00:19:55,979 in ternary logic and 602 00:19:55,980 --> 00:19:57,539 well, we have proven that this is a solid 603 00:19:57,540 --> 00:19:59,249 approximation, which makes the firewall 604 00:19:59,250 --> 00:20:00,539 stricter. 605 00:20:00,540 --> 00:20:02,939 So basically this firewall may accept 606 00:20:02,940 --> 00:20:04,829 less packets than the original firewall. 607 00:20:04,830 --> 00:20:07,019 And on the set, on the bottom, we get an 608 00:20:07,020 --> 00:20:08,579 approximation, which essentially makes 609 00:20:08,580 --> 00:20:10,319 the firewall more permissive. 610 00:20:10,320 --> 00:20:12,479 This firewall may accept more 611 00:20:12,480 --> 00:20:14,429 packets than original firewall. 612 00:20:14,430 --> 00:20:16,409 And the important thing here is, well, 613 00:20:16,410 --> 00:20:18,819 those are executable and 614 00:20:18,820 --> 00:20:19,820 well. 615 00:20:20,100 --> 00:20:22,409 The reality or the specification, 616 00:20:22,410 --> 00:20:24,149 what we want is in the middle and we have 617 00:20:24,150 --> 00:20:26,819 executable code around 618 00:20:26,820 --> 00:20:29,189 the reality, so to say, 619 00:20:29,190 --> 00:20:31,379 and while we will use these things 620 00:20:31,380 --> 00:20:33,689 all in the background now, because now 621 00:20:33,690 --> 00:20:35,879 we can execute the whole thing 622 00:20:35,880 --> 00:20:38,129 and we can safely approximate something 623 00:20:38,130 --> 00:20:39,899 if we run into some features we don't 624 00:20:39,900 --> 00:20:41,669 understand because we have embedded 625 00:20:41,670 --> 00:20:42,749 internal logic. 626 00:20:42,750 --> 00:20:45,029 So essentially we have no sound 627 00:20:45,030 --> 00:20:46,949 approximation where we can say, well, 628 00:20:46,950 --> 00:20:48,749 there's a match expression in somewhere 629 00:20:48,750 --> 00:20:50,309 in the firewall. We do not understand the 630 00:20:50,310 --> 00:20:52,439 result. There is unknown and 631 00:20:52,440 --> 00:20:54,479 the whole thing will be safely 632 00:20:54,480 --> 00:20:56,269 approximated according to what you want 633 00:20:56,270 --> 00:20:57,749 to. You want to be stricter or more 634 00:20:57,750 --> 00:20:59,249 permissive. 635 00:20:59,250 --> 00:21:01,649 So I said, I will explain 636 00:21:01,650 --> 00:21:03,239 how we get spoofing protection in the 637 00:21:03,240 --> 00:21:05,339 end. Let's look at spoofing protection. 638 00:21:05,340 --> 00:21:06,989 Let's first specify what spoofing 639 00:21:06,990 --> 00:21:08,039 protection is. 640 00:21:08,040 --> 00:21:10,709 Let's say we have an IP assignment. 641 00:21:10,710 --> 00:21:12,899 Zero belongs to the IP range, 190 642 00:21:12,900 --> 00:21:15,209 to 168 zero 643 00:21:15,210 --> 00:21:17,609 slash twenty four. 644 00:21:17,610 --> 00:21:19,169 So what does spoofing protection mean? 645 00:21:19,170 --> 00:21:22,199 It means for any IP packet that enters 646 00:21:22,200 --> 00:21:24,629 zero, the source IP must be in this 190 647 00:21:24,630 --> 00:21:26,789 to 160 age IP 648 00:21:26,790 --> 00:21:27,779 range. 649 00:21:27,780 --> 00:21:29,219 So let's specify that 650 00:21:30,390 --> 00:21:32,549 again, we are looking at a set and we 651 00:21:32,550 --> 00:21:33,899 have seen that before. 652 00:21:33,900 --> 00:21:36,929 We require that in the set. 653 00:21:36,930 --> 00:21:38,699 These are the packets accepted by the 654 00:21:38,700 --> 00:21:40,139 firewall. There's an additional 655 00:21:40,140 --> 00:21:41,579 constraint about the packet. 656 00:21:41,580 --> 00:21:44,069 The packet should come from the interface 657 00:21:44,070 --> 00:21:45,059 zero. 658 00:21:45,060 --> 00:21:46,949 And just like before, we are looking at 659 00:21:46,950 --> 00:21:49,079 the packet but not the complete package, 660 00:21:49,080 --> 00:21:50,939 we only look at the source IP. 661 00:21:50,940 --> 00:21:53,309 So this big set expression on your left 662 00:21:53,310 --> 00:21:55,919 is essentially the set of all packets 663 00:21:55,920 --> 00:21:58,379 accepted by the firewall coming from 664 00:21:58,380 --> 00:22:00,539 zero, but only the source IP. 665 00:22:00,540 --> 00:22:02,639 Well, and what should the set fulfill 666 00:22:02,640 --> 00:22:04,199 that the whole firewall implement 667 00:22:04,200 --> 00:22:05,549 spoofing protection. 668 00:22:05,550 --> 00:22:08,069 Well all this IP should be in the 669 00:22:08,070 --> 00:22:09,389 range of that interface. 670 00:22:09,390 --> 00:22:11,639 I guess we can all agree that 671 00:22:11,640 --> 00:22:13,769 they specify spoofing protection for that 672 00:22:13,770 --> 00:22:15,449 particular example. 673 00:22:15,450 --> 00:22:16,679 Let's generalize that. 674 00:22:16,680 --> 00:22:18,659 Let's say we require this for all the 675 00:22:18,660 --> 00:22:20,879 interfaces we have in our system and 676 00:22:20,880 --> 00:22:23,129 now we have specified spoofing 677 00:22:23,130 --> 00:22:24,209 protection. 678 00:22:24,210 --> 00:22:26,189 OK, again, we have specified it. 679 00:22:26,190 --> 00:22:27,749 I guess we all agree that is the spoofing 680 00:22:27,750 --> 00:22:29,489 protection. What can we do with the 681 00:22:29,490 --> 00:22:31,049 specification? 682 00:22:31,050 --> 00:22:33,269 Well, we wrote an algorithm, 683 00:22:33,270 --> 00:22:35,459 an algorithm. You only give this IP 684 00:22:35,460 --> 00:22:38,189 assignment as above and to ruleset. 685 00:22:38,190 --> 00:22:40,349 And if the algorithm returns true, you 686 00:22:40,350 --> 00:22:42,329 definitely have spoofing protection in 687 00:22:42,330 --> 00:22:43,409 your firewall. 688 00:22:43,410 --> 00:22:45,209 And let me point out the cool thing about 689 00:22:45,210 --> 00:22:47,909 it. There you see this arbitrary Gummo, 690 00:22:47,910 --> 00:22:49,649 arbitrary in mathematics always means, 691 00:22:49,650 --> 00:22:51,209 well, it's all quantified. 692 00:22:51,210 --> 00:22:53,519 What does this all quantified gamma 693 00:22:53,520 --> 00:22:55,619 mean? Gamma was the set of 694 00:22:55,620 --> 00:22:57,689 all matching features 695 00:22:57,690 --> 00:22:59,519 our firewall model supports here. 696 00:22:59,520 --> 00:23:00,749 It's arbitrary. 697 00:23:00,750 --> 00:23:02,879 So our algorithm can tell 698 00:23:02,880 --> 00:23:05,159 if you are spoofing protection for any 699 00:23:05,160 --> 00:23:07,259 magic IP tables match condition you 700 00:23:07,260 --> 00:23:08,609 may have in your firewall. 701 00:23:08,610 --> 00:23:10,349 Even if the net filter team decides to 702 00:23:10,350 --> 00:23:12,149 implement a new cool matching feature in 703 00:23:12,150 --> 00:23:14,219 the future. Maybe they don't know yet 704 00:23:14,220 --> 00:23:15,959 that they will implement that feature 705 00:23:15,960 --> 00:23:18,059 here. The specifications as well. 706 00:23:18,060 --> 00:23:20,519 This algorithm will correctly understand 707 00:23:20,520 --> 00:23:21,839 it and check if you have spoofing 708 00:23:21,840 --> 00:23:23,939 protection anyway, even if there 709 00:23:23,940 --> 00:23:25,859 is some unknown cool future feature in 710 00:23:25,860 --> 00:23:28,049 it. And I think that's a pretty, pretty 711 00:23:28,050 --> 00:23:30,239 cool specification there that 712 00:23:30,240 --> 00:23:32,069 we have about the algorithm. 713 00:23:32,070 --> 00:23:34,289 So it essentially says we understand 714 00:23:34,290 --> 00:23:36,329 all possible match conditions you can 715 00:23:36,330 --> 00:23:37,769 ever use in your firewall. 716 00:23:39,270 --> 00:23:41,519 Well, so what about 717 00:23:41,520 --> 00:23:42,539 the specification? 718 00:23:42,540 --> 00:23:43,829 Well, you know, with normal 719 00:23:43,830 --> 00:23:46,709 specifications, well, they are quite 720 00:23:46,710 --> 00:23:48,899 imprecise and not really tell you what 721 00:23:48,900 --> 00:23:49,859 the algorithm does. 722 00:23:49,860 --> 00:23:52,499 This is a mathematical specification. 723 00:23:52,500 --> 00:23:54,119 It's concise, it's really precise. 724 00:23:54,120 --> 00:23:56,279 And it tells you exactly what the 725 00:23:56,280 --> 00:23:58,019 algorithm gives to you. 726 00:23:58,020 --> 00:24:00,039 What else about your specification? 727 00:24:00,040 --> 00:24:01,919 Well, very often they lie to you. 728 00:24:01,920 --> 00:24:03,779 They have some implicit assumptions. 729 00:24:03,780 --> 00:24:05,279 They don't tell you you have to call in a 730 00:24:05,280 --> 00:24:07,229 special way, but they didn't document it. 731 00:24:07,230 --> 00:24:08,549 Well, not in this case. 732 00:24:08,550 --> 00:24:10,769 We have a formal proof that our 733 00:24:10,770 --> 00:24:12,929 algorithm really fulfills this 734 00:24:12,930 --> 00:24:15,329 condition. So there is no implicit 735 00:24:15,330 --> 00:24:17,699 assumption somewhere this specification 736 00:24:17,700 --> 00:24:19,799 will never night will never lie to 737 00:24:19,800 --> 00:24:21,929 you and all the other 738 00:24:21,930 --> 00:24:23,489 for some other documentations. 739 00:24:23,490 --> 00:24:25,439 You always know that the documentation is 740 00:24:25,440 --> 00:24:27,719 usually quite outdated, especially for 741 00:24:27,720 --> 00:24:29,549 a particular project. 742 00:24:29,550 --> 00:24:31,919 Well, here we have a machine verifiable 743 00:24:31,920 --> 00:24:34,139 proof. You can run that proof 744 00:24:34,140 --> 00:24:35,549 on your computer. You don't have to 745 00:24:35,550 --> 00:24:36,539 reconstruct it by hand. 746 00:24:36,540 --> 00:24:38,639 You can give the proof to your computer 747 00:24:38,640 --> 00:24:40,679 and tell your computer to reject the 748 00:24:40,680 --> 00:24:43,739 proof at any time so you can 749 00:24:43,740 --> 00:24:45,419 check it all the time if this 750 00:24:45,420 --> 00:24:47,729 specification is still what the algorithm 751 00:24:47,730 --> 00:24:50,309 provides. So this specification 752 00:24:50,310 --> 00:24:51,599 will never be outdated. 753 00:24:51,600 --> 00:24:53,669 And I claim, well, this is probably the 754 00:24:53,670 --> 00:24:55,829 best way to document your code to prove 755 00:24:55,830 --> 00:24:57,929 it correctly. It will never be outdated. 756 00:24:57,930 --> 00:24:59,429 It's really precise what it does. 757 00:24:59,430 --> 00:25:01,079 It doesn't have any hidden assumptions 758 00:25:01,080 --> 00:25:02,969 and it will definitely not lie to you. 759 00:25:04,800 --> 00:25:07,409 So I said we have executable 760 00:25:07,410 --> 00:25:08,410 code. 761 00:25:09,070 --> 00:25:10,839 Well, if this looked like a lot of them 762 00:25:10,840 --> 00:25:13,089 just exited with executable code look 763 00:25:13,090 --> 00:25:15,499 like, well, we wrote the whole thing and 764 00:25:15,500 --> 00:25:17,649 approved it and once we 765 00:25:17,650 --> 00:25:20,049 got executable code, we can export 766 00:25:20,050 --> 00:25:21,189 it to different languages. 767 00:25:21,190 --> 00:25:23,229 Here we use Haskell and you can really 768 00:25:23,230 --> 00:25:25,059 run that algorithm on your machine. 769 00:25:25,060 --> 00:25:27,279 You don't need Izabel or anything 770 00:25:27,280 --> 00:25:28,449 to improve Aslambek. And it's a 771 00:25:28,450 --> 00:25:30,789 standalone program here. 772 00:25:30,790 --> 00:25:32,139 You can see how you can call it. 773 00:25:32,140 --> 00:25:34,299 You just feed your IP table safe 774 00:25:34,300 --> 00:25:35,619 timba into the tool. 775 00:25:35,620 --> 00:25:37,749 Daniels applied IP assignment, as we 776 00:25:37,750 --> 00:25:39,549 saw on the slide before, or probably 777 00:25:39,550 --> 00:25:41,679 generated by Conficker or 778 00:25:41,680 --> 00:25:43,749 IP address and the toolbar 779 00:25:43,750 --> 00:25:45,489 just automatically run. 780 00:25:45,490 --> 00:25:47,109 It doesn't need any additional input. 781 00:25:47,110 --> 00:25:48,759 You don't have to prove anything by hand. 782 00:25:48,760 --> 00:25:50,739 It will just check if you have spoofing 783 00:25:50,740 --> 00:25:52,809 protection on your firewall. 784 00:25:52,810 --> 00:25:54,369 So there we have it. 785 00:25:54,370 --> 00:25:56,649 We have a verified tool to verify 786 00:25:56,650 --> 00:25:57,939 that you are spoofing protection on your 787 00:25:57,940 --> 00:25:59,049 firewall. 788 00:25:59,050 --> 00:26:00,879 And because I'm running out of time, I 789 00:26:00,880 --> 00:26:02,829 just want to show you a short outlook 790 00:26:02,830 --> 00:26:05,049 what else we have in all verified 791 00:26:05,050 --> 00:26:06,279 toolset there? 792 00:26:06,280 --> 00:26:09,039 Well, probably you've seen 793 00:26:09,040 --> 00:26:09,969 on the slide before. 794 00:26:09,970 --> 00:26:11,259 How big was the firewall? 795 00:26:11,260 --> 00:26:13,449 Four thousand eight hundred was quite 796 00:26:13,450 --> 00:26:15,519 large. I guess this firewall was that 797 00:26:15,520 --> 00:26:17,319 now hit the 5000 words. 798 00:26:17,320 --> 00:26:18,729 And we had the question. 799 00:26:18,730 --> 00:26:20,859 Well, by the way, who is allowed to 800 00:26:20,860 --> 00:26:23,319 set up SSL connections with whom 801 00:26:23,320 --> 00:26:25,059 in a 5000 words firewall? 802 00:26:25,060 --> 00:26:27,159 We said, well, there 803 00:26:27,160 --> 00:26:28,160 is the answer. 804 00:26:29,290 --> 00:26:30,729 All of these ranges, you see their 805 00:26:30,730 --> 00:26:33,009 internal servers, ayna, they essentially 806 00:26:33,010 --> 00:26:35,199 correspond to the complete IP for address 807 00:26:35,200 --> 00:26:37,329 range. I just gave it symbolic names here 808 00:26:37,330 --> 00:26:39,609 because, well, those ranges 809 00:26:39,610 --> 00:26:41,829 are really split up, maybe noncontiguous 810 00:26:41,830 --> 00:26:43,389 because there are so many exceptions in 811 00:26:43,390 --> 00:26:44,559 there, but they are all clustered 812 00:26:44,560 --> 00:26:45,459 together. 813 00:26:45,460 --> 00:26:47,049 And we have to name a few things about 814 00:26:47,050 --> 00:26:48,819 this graph. It's the complete IP before 815 00:26:48,820 --> 00:26:49,989 Edwards range. 816 00:26:49,990 --> 00:26:51,629 All these IP addresses that are true 817 00:26:51,630 --> 00:26:53,349 together, for example, in the service or 818 00:26:53,350 --> 00:26:55,479 internal group really have the same 819 00:26:55,480 --> 00:26:56,409 access. Right. 820 00:26:56,410 --> 00:26:58,509 And this is the best possible 821 00:26:58,510 --> 00:27:00,549 solution you can get for this question, 822 00:27:00,550 --> 00:27:02,259 because you cannot compress this any 823 00:27:02,260 --> 00:27:04,239 further. You can't get a clearer or 824 00:27:04,240 --> 00:27:05,289 better answer to that. 825 00:27:06,730 --> 00:27:08,799 Well, you may ask, why 826 00:27:08,800 --> 00:27:10,479 do we have to on the left, iiNet and 827 00:27:10,480 --> 00:27:11,719 iiNet Prime? 828 00:27:11,720 --> 00:27:13,539 Well, because of a typo in the firewall, 829 00:27:13,540 --> 00:27:14,540 which is now fixed. 830 00:27:16,090 --> 00:27:17,619 Well, it's pretty clear in the graph that 831 00:27:17,620 --> 00:27:19,749 you don't want to Internets there and you 832 00:27:19,750 --> 00:27:21,459 can really see the box there. 833 00:27:21,460 --> 00:27:23,109 And what was really interesting 834 00:27:23,110 --> 00:27:25,239 essentially for us, we can we looked at 835 00:27:25,240 --> 00:27:27,459 a long list of servers there and 836 00:27:27,460 --> 00:27:29,679 Internet and really verified that all 837 00:27:29,680 --> 00:27:31,569 these IPS for the servers are the 838 00:27:31,570 --> 00:27:33,689 machines which should be accessible by 839 00:27:33,690 --> 00:27:35,389 the internal ones are the ones which 840 00:27:35,390 --> 00:27:37,149 should not be accessible by association. 841 00:27:37,150 --> 00:27:39,039 And one of our 5000 rules, as you can 842 00:27:39,040 --> 00:27:41,439 see, that there are more, if 843 00:27:41,440 --> 00:27:43,569 not more funny exceptions, which 844 00:27:43,570 --> 00:27:45,429 are funny access rights, which you 845 00:27:45,430 --> 00:27:46,850 probably also should look at. 846 00:27:47,880 --> 00:27:50,049 OK, that's 847 00:27:50,050 --> 00:27:52,179 it. Thank you for your attention. 848 00:27:52,180 --> 00:27:53,919 Well, it would be really, really great if 849 00:27:53,920 --> 00:27:55,989 you have some firewall rules that's lying 850 00:27:55,990 --> 00:27:58,269 around and would want to donate 851 00:27:58,270 --> 00:28:00,399 them for research, for research would 852 00:28:00,400 --> 00:28:01,389 be really, really happy. 853 00:28:01,390 --> 00:28:02,949 And of course, everything we are doing 854 00:28:02,950 --> 00:28:05,139 here is not only fully verified, but also 855 00:28:05,140 --> 00:28:06,159 completely open source. 856 00:28:06,160 --> 00:28:07,719 You can get everything. 857 00:28:07,720 --> 00:28:08,919 Thank you for your attention. 858 00:28:08,920 --> 00:28:10,479 I guess we have a few minutes left for 859 00:28:10,480 --> 00:28:11,480 questions. 860 00:28:22,700 --> 00:28:24,709 So, yeah, just line up in front of the 861 00:28:24,710 --> 00:28:26,779 microphones right here and here. 862 00:28:31,330 --> 00:28:32,649 I think there is one. 863 00:28:32,650 --> 00:28:33,650 There you go. 864 00:28:36,060 --> 00:28:38,249 So have you done any work 865 00:28:38,250 --> 00:28:40,409 or are you aware of any work that 866 00:28:40,410 --> 00:28:41,410 involves 867 00:28:42,960 --> 00:28:45,299 studying final sets 868 00:28:45,300 --> 00:28:47,879 of multiple cooperating 869 00:28:47,880 --> 00:28:50,299 firewalls, short 870 00:28:50,300 --> 00:28:51,630 answer possible with the law 871 00:28:52,980 --> 00:28:53,819 at the moment? 872 00:28:53,820 --> 00:28:56,579 No, but there is other work and research 873 00:28:56,580 --> 00:28:58,979 which already claims to have solved 874 00:28:58,980 --> 00:29:00,999 this problem, and they did. 875 00:29:01,000 --> 00:29:02,879 But they have a very limited firewall 876 00:29:02,880 --> 00:29:04,769 model. What we can do with our tool, you 877 00:29:04,770 --> 00:29:06,959 can give them you can give us an IP 878 00:29:06,960 --> 00:29:09,479 Tabors safe done 879 00:29:09,480 --> 00:29:11,249 with all the complex features you have in 880 00:29:11,250 --> 00:29:13,169 the firewall. We can simplify it either 881 00:29:13,170 --> 00:29:15,239 to an overall approximation, 882 00:29:15,240 --> 00:29:17,699 which will create a much more simplify 883 00:29:17,700 --> 00:29:19,949 it and simplify what rules it is, then 884 00:29:19,950 --> 00:29:22,079 actually understood by some tools which 885 00:29:22,080 --> 00:29:24,689 have been developed in academia. 886 00:29:24,690 --> 00:29:25,829 OK, thank you. 887 00:29:25,830 --> 00:29:27,509 We can preprocessed, but we don't have 888 00:29:27,510 --> 00:29:29,579 yet incorporated further analysis 889 00:29:29,580 --> 00:29:30,709 in a fully verified manner. 890 00:29:34,370 --> 00:29:36,529 I thank you for the talk is very, 891 00:29:37,700 --> 00:29:40,489 very well done, and I 892 00:29:40,490 --> 00:29:42,499 would like to get more involved in formal 893 00:29:42,500 --> 00:29:44,869 methods and proof 894 00:29:44,870 --> 00:29:47,479 theories and stuff like that, but 895 00:29:47,480 --> 00:29:49,369 I have trouble knowing where to start. 896 00:29:49,370 --> 00:29:51,559 I was wondering if you had some insight 897 00:29:51,560 --> 00:29:53,599 into what resources would be good to get 898 00:29:53,600 --> 00:29:56,119 started with programing and Isabella 899 00:29:56,120 --> 00:29:58,309 Colker even 900 00:29:58,310 --> 00:30:00,289 address things like that. 901 00:30:00,290 --> 00:30:02,599 So first you should look at theer 902 00:30:02,600 --> 00:30:03,799 improver at your choice. 903 00:30:03,800 --> 00:30:04,969 I prefer Isabella. 904 00:30:04,970 --> 00:30:06,739 If you're more from the programing 905 00:30:06,740 --> 00:30:09,199 community, you will probably 906 00:30:09,200 --> 00:30:10,849 enjoy COK more. 907 00:30:10,850 --> 00:30:13,009 It depends a lot on personal choice and 908 00:30:13,010 --> 00:30:14,989 everything. If you're a student at UT 909 00:30:14,990 --> 00:30:16,459 Munich, you should definitely go to 910 00:30:16,460 --> 00:30:19,159 Tobias Gnip course great courses 911 00:30:19,160 --> 00:30:20,959 because there we have the Isabella Group 912 00:30:20,960 --> 00:30:23,119 directly. And if you want to get started 913 00:30:23,120 --> 00:30:24,949 with Isabella, there's the book Concrete 914 00:30:24,950 --> 00:30:27,139 Semantics by Tobias Nick and Kevin 915 00:30:27,140 --> 00:30:28,729 Kline. And I hope I didn't miss another 916 00:30:28,730 --> 00:30:31,159 also, which is, I guess, 917 00:30:31,160 --> 00:30:32,869 freely available. 918 00:30:32,870 --> 00:30:34,309 You can also buy it. 919 00:30:34,310 --> 00:30:36,649 And all the examples in the book 920 00:30:36,650 --> 00:30:38,539 should be included in the default is 921 00:30:38,540 --> 00:30:40,189 about distribution. So that's the easiest 922 00:30:40,190 --> 00:30:41,209 way to get started. 923 00:30:41,210 --> 00:30:43,279 Download the complete Ysabel package. 924 00:30:43,280 --> 00:30:45,379 Look at the book it runs. 925 00:30:45,380 --> 00:30:46,819 Usually on your system, you don't have to 926 00:30:46,820 --> 00:30:48,919 compile any additional packets 927 00:30:48,920 --> 00:30:50,749 and get started with the book. 928 00:30:50,750 --> 00:30:52,209 OK, thank you very much. 929 00:30:52,210 --> 00:30:53,480 We're running out of time, but 930 00:30:55,520 --> 00:30:57,349 hey, we're running out of time. 931 00:30:57,350 --> 00:30:58,699 So there is time for one last question 932 00:30:58,700 --> 00:31:00,439 from the signal angel. 933 00:31:00,440 --> 00:31:01,759 Yes. 934 00:31:01,760 --> 00:31:03,679 On the IRS here, they would like to know 935 00:31:03,680 --> 00:31:05,509 was the time, complexity of the 936 00:31:05,510 --> 00:31:06,510 algorithm, 937 00:31:07,880 --> 00:31:10,429 the runtime complexity 938 00:31:10,430 --> 00:31:12,619 and, well, bad 939 00:31:12,620 --> 00:31:12,949 news. 940 00:31:12,950 --> 00:31:15,079 This preprocessing can blow up 941 00:31:15,080 --> 00:31:17,839 to exponentially many rules 942 00:31:17,840 --> 00:31:18,739 in theory. 943 00:31:18,740 --> 00:31:20,449 In practice, we looked at a lot of 944 00:31:20,450 --> 00:31:21,559 firewalls to. 945 00:31:21,560 --> 00:31:24,259 Well, and this exponential complexity 946 00:31:24,260 --> 00:31:26,449 is sort of exponential in 947 00:31:26,450 --> 00:31:28,909 how fucked up you managed to call 948 00:31:28,910 --> 00:31:30,769 your user defined chains. 949 00:31:30,770 --> 00:31:32,959 So usually you do that by hand or 950 00:31:32,960 --> 00:31:35,089 see me automated so it doesn't blow up 951 00:31:35,090 --> 00:31:36,949 that much. The worse things to tell you, 952 00:31:36,950 --> 00:31:39,049 real numbers I saw as it was about a 953 00:31:39,050 --> 00:31:41,449 500 word firewall based on a Schwarzwald 954 00:31:41,450 --> 00:31:43,099 setup, which was really, really quite 955 00:31:43,100 --> 00:31:44,719 well. It triggered that a lot. 956 00:31:44,720 --> 00:31:46,819 And also when we revised IP 957 00:31:46,820 --> 00:31:48,559 address ranges to non-negative zero 958 00:31:48,560 --> 00:31:50,209 range, which can also blow up a lot. 959 00:31:50,210 --> 00:31:52,639 The worst block we ever saw was from 5000 960 00:31:52,640 --> 00:31:54,719 to 20000 words, which are 961 00:31:54,720 --> 00:31:57,079 still very good lendable by our computer, 962 00:31:57,080 --> 00:31:58,999 because afterwards, basically all our 963 00:31:59,000 --> 00:32:01,279 reasons are mostly polynomial 964 00:32:01,280 --> 00:32:02,569 time, if not even linear. 965 00:32:02,570 --> 00:32:04,789 To tell you real numbers, this took 966 00:32:04,790 --> 00:32:06,529 about one minute of prepossessing for 967 00:32:06,530 --> 00:32:08,389 5000 words and then about one second per 968 00:32:08,390 --> 00:32:10,699 interface. And this took less than two 969 00:32:10,700 --> 00:32:11,700 minutes. 970 00:32:12,650 --> 00:32:14,809 Or the four or five thousand girls, so 971 00:32:14,810 --> 00:32:16,279 you can really run those things on your 972 00:32:16,280 --> 00:32:17,280 computer. 973 00:32:18,320 --> 00:32:19,320 Cool, thanks.