1---------------------------------------------------------------- 2-- IRONSIDES - DNS SERVER 3-- 4-- By: Martin C. Carlisle and Barry S. Fagin 5-- Department of Computer Science 6-- United States Air Force Academy 7-- 8-- This is free software; you can redistribute it and/or 9-- modify without restriction. We do ask that you please keep 10-- the original author information, and clearly indicate if the 11-- software has been modified. 12-- 13-- This software is distributed in the hope that it will be useful, 14-- but WITHOUT ANY WARRANTY; without even the implied warranty 15-- of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 16---------------------------------------------------------------- 17 18with System; 19with Protected_SPARK_IO_05; 20with DNS_Types; 21with Unsigned_Types; 22with DNS_Table_PKG; 23with DNS_Network_Receive; 24use type DNS_Types.Packet_Bytes_Range; 25use type DNS_Types.Packet_Length_Range; 26use type DNS_Types.Byte; 27use type DNS_Types.Query_Type; 28USE TYPE DNS_Types.Query_Class; 29use type Unsigned_Types.Unsigned8; 30use type Unsigned_Types.Unsigned16; 31use type Unsigned_Types.Unsigned32; 32use type DNS_Types.Unsigned_Short; 33use type DNS_Types.QNAME_PTR_RANGE; 34use type System.Bit_Order; 35--with Ada.Text_Io; 36with ada.Unchecked_Conversion; 37package body Process_Dns_Request is 38 procedure Set_Unsigned_32( 39 Bytes : in out DNS_Types.Bytes_Array_Type; 40 Start_Byte : in DNS_Types.Packet_Bytes_Range; 41 Value : in Unsigned_Types.Unsigned32) is 42 begin 43 Bytes(Start_Byte) := DNS_Types.Byte(Value/2**24); 44 Bytes(Start_Byte+1) := DNS_Types.Byte((Value/2**16) mod 256); 45 Bytes(Start_Byte+2) := DNS_Types.Byte((Value/2**8) mod 256); 46 Bytes(Start_Byte+3) := DNS_Types.Byte(Value mod 256); 47 end Set_Unsigned_32; 48 procedure Set_Unsigned_16( 49 Bytes : in out DNS_Types.Bytes_Array_Type; 50 Start_Byte : in DNS_Types.Packet_Bytes_Range; 51 Value : in Unsigned_Types.Unsigned16) is 52 begin 53 Bytes(Start_Byte) := DNS_Types.Byte((Value/2**8) mod 256); 54 Bytes(Start_Byte+1) := DNS_Types.Byte(Value mod 256); 55 end Set_Unsigned_16; 56 57 procedure Set_TTL_Data_IP( 58 Bytes : in out DNS_Types.Bytes_Array_Type; 59 Start_Byte : in DNS_Types.Packet_Bytes_Range; 60 A_Record : in Rr_Type.A_Record_Type.ARecordType) is 61 begin 62 -- TTL 63 Set_Unsigned_32(Bytes,Start_Byte,A_Record.ttlInSeconds); 64 -- DATA 4 bytes 65 Set_Unsigned_16(Bytes,Start_Byte+4,4); 66 -- IP address 67 Set_Unsigned_32(Bytes,Start_Byte+6,A_Record.ipv4); 68 end Set_TTL_Data_IP; 69 70 --base64 conversion 71 FUNCTION Lookup(Arg: IN Character) RETURN DNS_Types.Byte IS 72 ans : DNS_Types.Byte; 73 BEGIN 74 CASE Arg IS 75 WHEN 'A'..'Z' => ans := Character'Pos(Arg) - Character'Pos('A'); 76 WHEN 'a'..'z' => ans := (Character'Pos(Arg) - Character'Pos('a'))+26; 77 WHEN '0'..'9' => ans := (Character'Pos(Arg) - Character'Pos('0'))+52; 78 WHEN '+' => ans := 62; 79 WHEN '/' => ans := 63; 80 WHEN OTHERS => ans := 0; 81 end case; 82 return ans; 83 END Lookup; 84 85 --see http://rfc-ref.org/RFC-TEXTS/4034/chapter2.html for DNSKEY record format 86 procedure Set_TTL_Data_DNSKEY( --BSF 87 Bytes : in out DNS_Types.Bytes_Array_Type; 88 Start_Byte : in DNS_Types.Packet_Bytes_Range; 89 DNSKEY_Record : IN Rr_Type.DNSKEY_Record_Type.DNSKEYRecordType; 90 dstbytes : out rr_type.dnskey_record_type.keyLengthValueType) IS 91 srcByte : Integer; 92 KeyLength : Rr_Type.Dnskey_Record_Type.KeyLengthValueType; 93 SrcNum0, SrcNum1, SrcNum2, SrcNum3: Dns_Types.Byte; 94 dstNum0, dstNum1, dstNum2 : dns_types.byte; 95 begin 96 -- TTL (4 bytes) 97 Set_Unsigned_32(Bytes,Start_Byte,DNSKEY_Record.ttlInSeconds); 98 -- RDLENGTH (2 bytes, value is 4 plus the length of the key, placeholder at this point) 99 Set_Unsigned_16(Bytes,Start_Byte+4,4+Unsigned_Types.Unsigned16(DNSKEY_Record.keyLength)); 100 -- RDATA (4 bytes) 101 -- flags (2 bytes) 102 Set_Unsigned_16(Bytes,Start_Byte+6,DNSKEY_Record.Flags); 103 -- protocol (1 byte) 104 Bytes(Start_Byte+8) := DNS_types.Byte(DNSKEY_Record.Protocol); 105 -- algorithm (1 byte) 106 Bytes(Start_Byte+9) := DNS_types.Byte(DNSKEY_Record.Algorithm); 107 -- key field 108 srcByte := 1; 109 dstBytes := 1; 110 keyLength := DNSKEY_Record.KeyLength; 111 while srcByte + 3 <= keyLength loop --since it's base64 encoded, src key will always contain an exact multiple of 4 bytes 112 --# assert srcByte + 3 <= KeyLength and 113 --# KeyLength <= rr_type.DNSKEY_Record_Type.MaxDNSKeyLength and KeyLength = DNSKEY_Record.KeyLength and 114 --# dstBytes >= 1 and dstBytes <= srcByte and 115 --# Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-10-DNS_Types.Packet_Bytes_Range(DNSKEY_Record.keyLength); 116 srcNum0 := Lookup(DNSKEY_Record.Key(srcByte)); --00aaaaaa 117 srcNum1 := Lookup(DNSKEY_Record.Key(srcByte+1)); --00bbbbbb 118 srcNum2 := Lookup(DNSKEY_Record.Key(srcByte+2)); --00cccccc 119 SrcNum3 := Lookup(DNSKEY_Record.Key(SrcByte+3)); --00dddddd 120 121 DstNum0 := SrcNum0*4 + (Srcnum1/16); --aaaaaa00 + 000000bb = aaaaaabb 122 DstNum1 := Srcnum1*16 + (SrcNum2/4); --bbbb0000 + 0000cccc = bbbbcccc 123 DstNum2 := SrcNum2*64 + SrcNum3; --cc000000 + 00dddddd = ccdddddd 124 125 Bytes((Start_Byte+9)+DNS_Types.Packet_Bytes_Range(DstBytes)) := DstNum0; 126 Bytes((Start_Byte+9)+DNS_Types.Packet_Bytes_Range(DstBytes+1)) := DstNum1; 127 Bytes((Start_Byte+9)+DNS_Types.Packet_Bytes_Range(DstBytes+2)) := DstNum2; 128 129 srcByte := srcByte + 4; 130 DstBytes := DstBytes + 3; 131 END LOOP; 132 -- RDLENGTH (2 bytes, value is 4 plus the length of the key, which we now know) 133 dstBytes := dstbytes-1; --this is also an out parameter of this procedure 134 Set_Unsigned_16(Bytes,Start_Byte+4,4+Unsigned_Types.Unsigned16(dstBytes)); 135 END Set_TTL_Data_DNSKEY; 136 137--see http://tools.ietf.org/rfc/rfc3845.txt for NSEC wire format. If you're a masochist. 138 procedure Set_TTL_Data_NSEC( --BSF 139 Bytes : in out DNS_Types.Bytes_Array_Type; 140 Start_Byte : in DNS_Types.Packet_Bytes_Range; 141 NSEC_Record : IN Rr_Type.NSEC_Record_Type.NSECRecordType; 142 Dstbytes : OUT DNS_Types.Packet_Length_Range) IS --bytes used in RRDATA section 143 Current_Name_Length : RR_Type.WireStringTypeIndex; 144 blockOffset : DNS_Types.Packet_Bytes_Range; 145 BEGIN 146 -- TTL (4 bytes) 147 Set_Unsigned_32(Bytes,Start_Byte,NSEC_Record.TtlInSeconds); 148 -- RDLENGTH (2 bytes, value will be the length of the domain name plus the length of the bitmapped RRList) 149 -- placeholder for now 150 Set_Unsigned_16(Bytes,Start_Byte+4,Unsigned_Types.Unsigned16(0)); 151 152 -- NEXT DOMAIN NAME (Current_Name_Length bytes) 153 Current_Name_Length := RR_Type.WireNameLength(NSEC_Record.NextDomainName); 154 for i in RR_Type.WireStringTypeIndex range 1..Current_Name_Length loop 155 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) 156 --# and i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last 157 --# and Current_Name_Length >= RR_Type.WireStringTypeIndex'First and Current_Name_Length <= RR_Type.WireStringTypeIndex'Last 158 --# and (for all J in RR_Type.WireStringTypeIndex => (Character'Pos(NSEC_Record.NextDomainName(J)) >= 0 and (Character'Pos(NSEC_Record.NextDomainName(J)) <= 255))); 159 Bytes(((Start_Byte+6)-1)+DNS_Types.Packet_Bytes_Range(i)) := DNS_Types.Byte(Character'Pos(NSEC_Record.NextDomainName(i))); 160 END LOOP; 161 162 -- RR bitmap section (ugh) 163 dstBytes := 0; 164 BlockOffset := (((Start_Byte+6)-1)+DNS_Types.Packet_Bytes_Range(Current_Name_Length)); 165 FOR block IN rr_type.nsec_record_type.blockNumberValue range 1..NSEC_Record.NumberOfBlocks LOOP 166 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) 167 --# and Current_Name_Length >= RR_Type.WireStringTypeIndex'First and Current_Name_Length <= RR_Type.WireStringTypeIndex'Last 168 --# and blockOffset >= dns_types.packet_bytes_range'first 169 --# and blockOffset <= (((Start_Byte+6)-1)+DNS_Types.Packet_Bytes_Range(Current_Name_Length)) 170 --# + DNS_Types.Packet_Bytes_Range((block-1)*(2+rr_type.nsec_record_type.BlockLengthValue'last)) 171 --# and dstBytes <= dns_types.packet_length_range((block-1)*rr_type.nsec_record_type.BlockLengthValue'last) 172 --# and NSEC_Record.BlockLengths(Block) >= rr_type.nsec_record_type.BlockLengthValue'first 173 --# and NSEC_Record.BlockLengths(Block) <= rr_type.nsec_record_type.BlockLengthValue'last; 174 DstBytes := DstBytes + dns_types.Packet_Length_Range(NSEC_Record.BlockLengths(Block)); --sum up the block lengths, needed below 175 Bytes(BlockOffset +1) := NSEC_Record.BlockNumbers(Block); 176 Bytes(BlockOffset +2) := Dns_Types.Byte(NSEC_Record.BlockLengths(Block)); 177 FOR Byte IN rr_type.nsec_record_type.BlockLengthValue range 1..NSEC_Record.BlockLengths(Block) LOOP 178 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) 179 --# and Current_Name_Length >= RR_Type.WireStringTypeIndex'First and Current_Name_Length <= RR_Type.WireStringTypeIndex'Last 180 --# and blockOffset >= dns_types.packet_bytes_range'first 181 --# and blockOffset <= (((Start_Byte+6)-1)+DNS_Types.Packet_Bytes_Range(Current_Name_Length)) 182 --# + DNS_Types.Packet_Bytes_Range((block-1)*(2+rr_type.nsec_record_type.BlockLengthValue'last)) 183 --# and dstBytes <= dns_types.packet_length_range(block*rr_type.nsec_record_type.BlockLengthValue'last) 184 --# and byte >= rr_type.nsec_record_type.BlockLengthValue'first and byte <= rr_type.nsec_record_type.BlockLengthValue'last 185 --# and block = block%; 186 Bytes((BlockOffset+2)+Dns_Types.Packet_Bytes_Range(Byte)) := NSEC_Record.BitMaps(Block)(Byte); 187 END LOOP; 188 BlockOffset := (BlockOffset + 2) + dns_types.Packet_Bytes_Range(NSEC_Record.BlockLengths(Block)); 189 END LOOP; 190 DstBytes := DstBytes + dns_types.Packet_Length_Range(NSEC_Record.NumberOfBlocks*2); --add in the bytes for the block numbers and the block lengths 191 DstBytes := (DstBytes + dns_types.Packet_Length_Range(Current_Name_Length)); --sets final value of OUT parameter 192 -- RDLENGTH (2 bytes, can now set final value as the length of the domain name plus the length of the bitmapped RRList) 193 Set_Unsigned_16(Bytes,Start_Byte+4,unsigned_types.unsigned16(dstBytes)); 194 END Set_TTL_Data_NSEC; 195 196 --see http://www.rfc-editor.org/rfc/rfc4034.txt for RRSIG record format 197 procedure Set_TTL_Data_RRSIG( --BSF 198 Bytes : in out DNS_Types.Bytes_Array_Type; 199 Start_Byte : in DNS_Types.Packet_Bytes_Range; 200 RRSIG_Record : IN Rr_Type.RRSIG_Record_Type.RRSIGRecordType; 201 dstBytes : OUT DNS_Types.Packet_Bytes_Range) IS 202 WireVersion : RR_Type.WireStringType; 203 Current_Name_Length : RR_Type.WireStringTypeIndex; 204 srcByte : Integer; 205 sigLength : Rr_Type.Rrsig_Record_Type.sigLengthValueType; 206 sigOffset : DNS_Types.Packet_Bytes_Range; 207 SrcNum0, SrcNum1, SrcNum2, SrcNum3: Dns_Types.Byte; 208 DstNum0, DstNum1, DstNum2 : Dns_Types.Byte; 209 function From_Query_Type is new Ada.Unchecked_Conversion(DNS_Types.Query_Type,Unsigned_Types.Unsigned32); 210 function From_Bytes_Range is new Ada.Unchecked_Conversion(DNS_Types.Packet_Bytes_Range,Unsigned_Types.Unsigned32); 211 BEGIN 212 -- TTL (4 bytes) 213 Set_Unsigned_32(Bytes,Start_Byte,RRSIG_Record.ttlInSeconds); 214 -- RDLENGTH (2 bytes, value is 18 plus the length of the name plus the length of the signature, placeholder at this point) 215 Set_Unsigned_16(Bytes,Start_Byte+4,0); 216 -- TYPE COVERED (2 bytes) 217 --# accept Warning, 12, From_Query_Type, "unchecked conversions ok"; 218 -- Ugh. The things we do to make SPARK happy. mod is superfluous, used only to convince SPARK that the value is in type. 219 Set_Unsigned_16(Bytes,Start_Byte+6,Unsigned_Types.Unsigned16(from_query_type(RRSIG_Record.typeCovered) mod 65536)); 220 -- ALGORITHM (1 byte) 221 Bytes(Start_Byte+8) := DNS_Types.Byte(RRSIG_Record.Algorithm); 222 -- LABELS (1 byte) 223 Bytes(Start_Byte+9) := DNS_Types.Byte(RRSIG_Record.numLabels); 224 -- ORIG TTL (4 bytes) 225 Set_Unsigned_32(Bytes,Start_Byte+10,RRSIG_Record.OrigTTL); 226 -- SIG EXPIRATION (4 bytes) 227 Set_Unsigned_32(Bytes,Start_Byte+14,RRSIG_Record.SigExpiration); 228 -- SIG INCEPTION (4 bytes) (starring Leonardo DiCaprio) 229 Set_Unsigned_32(Bytes,Start_Byte+18,RRSIG_Record.SigInception); 230 -- KEY TAG (2 bytes) 231 Set_Unsigned_16(Bytes,Start_Byte+22,RRSIG_Record.KeyTag); 232 233 -- SIGNER'S NAME (Current_Name_Length bytes) 234 WireVersion := Rr_Type.ConvertDomainNameToWire(RRSIG_Record.SignerName); 235 Current_Name_Length := RR_Type.WireNameLength(WireVersion); 236 for i in RR_Type.WireStringTypeIndex range 1..Current_Name_Length loop 237 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-24)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) 238 --# and i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last 239 --# and Current_Name_Length >= RR_Type.WireStringTypeIndex'First and Current_Name_Length <= RR_Type.WireStringTypeIndex'Last 240 --# and (for all J in RR_Type.WireStringTypeIndex => (Character'Pos(WireVersion(J)) >= 0 and (Character'Pos(WireVersion(J)) <= 255))); 241 Bytes(((Start_Byte+24)-1)+DNS_Types.Packet_Bytes_Range(i)) := DNS_Types.Byte(Character'Pos(WireVersion(i))); 242 END LOOP; 243 244 -- SIGNATURE 245 srcByte := 1; 246 dstBytes := 1; 247 sigLength := RRSIG_Record.SignatureLength; 248 sigOffset := (((Start_Byte+24)-1)+DNS_Types.Packet_Bytes_Range(Current_Name_Length)); --this+1 is the index of the first byte of the signature 249 while (srcByte + 3 <= sigLength) loop --since it's base64 encoded, src key will always contain an exact multiple of 4 bytes 250 --# assert srcByte + 3 <= sigLength and 251 --# sigLength <= rr_type.RRSIG_Record_Type.MaxRRSIGLength and sigLength = RRSIG_Record.signatureLength and 252 --# dstBytes >= DNS_Types.Packet_Bytes_Range(1) and dstBytes <= DNS_Types.Packet_Bytes_Range(srcByte) and 253 --# Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-24-DNS_Types.Packet_Bytes_Range(rr_type.MaxDomainNameLength)-DNS_Types.Packet_Bytes_Range(sigLength) 254 --# and Current_Name_Length >= RR_Type.WireStringTypeIndex'First and Current_Name_Length <= RR_Type.WireStringTypeIndex'Last 255 --# and sigOffset = Start_Byte+24-1+DNS_Types.Packet_Bytes_Range(Current_Name_Length); 256 srcNum0 := Lookup(RRSIG_Record.signature(srcByte)); --00aaaaaa 257 srcNum1 := Lookup(RRSIG_Record.signature(srcByte+1)); --00bbbbbb 258 srcNum2 := Lookup(RRSIG_Record.signature(srcByte+2)); --00cccccc 259 SrcNum3 := Lookup(RRSIG_Record.signature(SrcByte+3)); --00dddddd 260 261 DstNum0 := SrcNum0*4 + (Srcnum1/16); --aaaaaa00 + 000000bb = aaaaaabb 262 DstNum1 := Srcnum1*16 + (SrcNum2/4); --bbbb0000 + 0000cccc = bbbbcccc 263 DstNum2 := SrcNum2*64 + SrcNum3; --cc000000 + 00dddddd = ccdddddd 264 265 Bytes(sigOffset + dstBytes) := DstNum0; 266 Bytes(sigOffset + (dstBytes+1)) := DstNum1; 267 Bytes(sigOffset + (dstBytes+2)) := DstNum2; 268 269 srcByte := srcByte + 4; 270 dstBytes := dstBytes + 3; 271 END LOOP; 272 273 -- Finally, we know how many bytes have been used on the wire (24 plus the length of the signer's name plus the length of the key) 274 dstBytes := DNS_Types.Packet_Bytes_Range(24+Current_Name_Length)+(dstBytes-DNS_Types.Packet_Bytes_Range(1)); --sets the out parameter of this procedure 275 -- and we can set RDLENGTH (2 bytes, value is 18 plus the length of the signer's name plus the length of the key) 276 --# accept Warning, 12, From_Bytes_Range, "unchecked conversions ok"; 277 -- The things we do to make SPARK happy. 278 Set_Unsigned_16(Bytes,Start_Byte+4,Unsigned_Types.Unsigned16(from_bytes_range(dstBytes-6) mod 65536)); 279 -- sets RDLENGTH field (TTL and RDLENGTH fields don't count, so subtract 4+2=6 bytes) 280 281 END Set_TTL_Data_RRSIG; 282 283 procedure Set_TTL_Data_NS_Response( 284 Bytes : in out DNS_Types.Bytes_Array_Type; 285 Start_Byte : in DNS_Types.Packet_Bytes_Range; 286 NS_Record : in Rr_Type.ns_record_type.NSRecordType; 287 Current_Name_Length : in RR_Type.WireStringTypeIndex) is 288 begin 289 -- TTL 290 Set_Unsigned_32(Bytes,Start_Byte,NS_Record.ttlInSeconds); 291 -- DATA # bytes is equal to length of WireString 292 Set_Unsigned_16(Bytes,Start_Byte+4,Unsigned_Types.Unsigned16(Current_name_Length)); 293 -- copy NS record 294 for i in RR_Type.WireStringTypeIndex range 1..Current_Name_Length loop 295 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) and 296 --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last; 297 Bytes((Start_Byte+5)+DNS_Types.Packet_Bytes_Range(I)) := DNS_Types.Byte( 298 Character'Pos(NS_Record.nameServer(i))); 299 end loop; 300 end Set_TTL_Data_NS_Response; 301 302 procedure Set_TTL_Data_PTR_Response( 303 Bytes : in out DNS_Types.Bytes_Array_Type; 304 Start_Byte : in DNS_Types.Packet_Bytes_Range; 305 PTR_Record : in Rr_Type.ptr_record_type.PTRRecordType; 306 Current_Name_Length : in RR_Type.WireStringTypeIndex) is 307 begin 308 -- TTL 309 Set_Unsigned_32(Bytes,Start_Byte,PTR_Record.ttlInSeconds); 310 -- DATA # bytes is equal to length of WireString 311 Set_Unsigned_16(Bytes,Start_Byte+4,Unsigned_Types.Unsigned16(Current_name_Length)); 312 -- copy NS record 313 for i in RR_Type.WireStringTypeIndex range 1..Current_Name_Length loop 314 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) and 315 --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last; 316 Bytes((Start_Byte+5)+DNS_Types.Packet_Bytes_Range(I)) := DNS_Types.Byte( 317 Character'Pos(PTR_Record.domainname(i))); 318 end loop; 319 end Set_TTL_Data_PTR_Response; 320 321 322 procedure Set_TTL_Data_MX_Response( 323 Bytes : in out DNS_Types.Bytes_Array_Type; 324 Start_Byte : in DNS_Types.Packet_Bytes_Range; 325 MX_Record : in Rr_Type.MX_record_type.MXRecordType; 326 Current_Name_Length : in RR_Type.WireStringTypeIndex) is 327 begin 328 -- TTL 329 Set_Unsigned_32(Bytes,Start_Byte,MX_Record.ttlInSeconds); 330 -- DATA # bytes is equal to length of WireString + 2 331 Set_Unsigned_16(Bytes,Start_Byte+4,Unsigned_Types.Unsigned16(Current_Name_Length+2)); 332 -- MAIL exchanger preference 333 Set_Unsigned_16(Bytes,Start_Byte+6,MX_Record.pref); 334 -- copy NS record 335 for i in RR_Type.WireStringTypeIndex range 1..Current_Name_Length loop 336 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-8)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) and 337 --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last; 338 Bytes((Start_Byte+7)+DNS_Types.Packet_Bytes_Range(I)) := DNS_Types.Byte( 339 Character'Pos(MX_Record.mailExchanger(i))); 340 end loop; 341 end Set_TTL_Data_MX_Response; 342 343 procedure Set_TTL_Data_SRV_Response( 344 Bytes : in out DNS_Types.Bytes_Array_Type; 345 Start_Byte : in DNS_Types.Packet_Bytes_Range; 346 SRV_Record : in Rr_Type.SRV_record_type.SRVRecordType; 347 Current_Name_Length : in RR_Type.WireStringTypeIndex) is 348 begin 349 -- TTL 350 Set_Unsigned_32(Bytes,Start_Byte,SRV_Record.ttlInSeconds); 351 -- DATA # bytes is equal to length of WireString + 6 352 Set_Unsigned_16(Bytes,Start_Byte+4,Unsigned_Types.Unsigned16(Current_Name_Length+6)); 353 -- Server preference 354 Set_Unsigned_16(Bytes,Start_Byte+6,SRV_Record.pref); 355 -- Server weight 356 Set_Unsigned_16(Bytes,Start_Byte+8,SRV_Record.weight); 357 -- Server port 358 Set_Unsigned_16(Bytes,Start_Byte+10,SRV_Record.portNum); 359 -- copy NS record 360 for i in RR_Type.WireStringTypeIndex range 1..Current_Name_Length loop 361 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-12)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) and 362 --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last; 363 Bytes((Start_Byte+11)+DNS_Types.Packet_Bytes_Range(I)) := DNS_Types.Byte( 364 Character'Pos(SRV_Record.ServerName(i))); 365 end loop; 366 end Set_TTL_Data_SRV_Response; 367 368 procedure Set_TTL_Data_SOA_Response( 369 Bytes : in out DNS_Types.Bytes_Array_Type; 370 Start_Byte : in DNS_Types.Packet_Bytes_Range; 371 SOA_Record : in Rr_Type.SOA_record_type.SOARecordType; 372 Nameserver_Name_Length : in RR_Type.WireStringTypeIndex; 373 Mailbox_Name_Length : in RR_Type.WireStringTypeIndex) is 374 Current_Byte : DNS_Types.Packet_Bytes_Range; 375 begin 376 -- TTL 377 Set_Unsigned_32(Bytes,Start_Byte,SOA_Record.ttlInSeconds); 378 -- DATA # bytes is equal to length of both WireStrings + 20 379 Set_Unsigned_16(Bytes,Start_Byte+4,Unsigned_Types.Unsigned16( 380 Nameserver_Name_Length + (Mailbox_Name_Length+20))); 381 -- copy NS record 382 for i in RR_Type.WireStringTypeIndex range 1..Nameserver_Name_Length loop 383 --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-20)- 384 --# DNS_Types.Packet_Bytes_Range(Mailbox_Name_Length+Nameserver_Name_Length) and 385 --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last; 386 Bytes((Start_Byte+5)+DNS_Types.Packet_Bytes_Range(I)) := DNS_Types.Byte( 387 Character'Pos(SOA_Record.nameServer(i))); 388 end loop; 389 Current_Byte := Start_Byte+DNS_Types.Packet_Bytes_Range( 390 5+(Nameserver_Name_Length)); 391 -- copy MB record 392 for i in RR_Type.WireStringTypeIndex range 1..Mailbox_Name_Length loop 393 --# assert Current_Byte>=1 and Current_Byte <= (DNS_Types.Packet_Bytes_Range'Last-20)- 394 --# DNS_Types.Packet_Bytes_Range(Mailbox_Name_Length) and 395 --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last; 396 Bytes(Current_Byte+DNS_Types.Packet_Bytes_Range(I)) := DNS_Types.Byte( 397 Character'Pos(SOA_Record.email(i))); 398 end loop; 399 Current_Byte := Start_Byte+DNS_Types.Packet_Bytes_Range( 400 6+(Nameserver_Name_Length + Mailbox_Name_Length)); 401 -- serial number 402 Set_Unsigned_32(Bytes,Current_Byte,SOA_Record.SerialNumber); 403 -- refresh interval 404 Set_Unsigned_32(Bytes,Current_Byte+4,SOA_Record.refresh); 405 -- retry interval 406 Set_Unsigned_32(Bytes,Current_Byte+8,SOA_Record.retry); 407 -- expiration limit 408 Set_Unsigned_32(Bytes,Current_Byte+12,SOA_Record.expiry); 409 -- minimum TTL 410 Set_Unsigned_32(Bytes,Current_Byte+16,SOA_Record.minimum); 411 end Set_TTL_Data_SOA_Response; 412 413 414 procedure Set_TTL_Data_AAAA_IP( 415 Bytes : in out DNS_Types.Bytes_Array_Type; 416 Start_Byte : in DNS_Types.Packet_Bytes_Range; 417 AAAA_Record : in Rr_Type.AAAA_Record_Type.AAAARecordType) is 418 begin 419 -- TTL 420 Set_Unsigned_32(Bytes,Start_Byte,AAAA_Record.ttlInSeconds); 421 -- DATA 16 bytes 422 Set_Unsigned_16(Bytes,Start_Byte+4,16); 423 for i in rr_type.aaaa_record_type.IPV6AddrTypeIndex loop 424 --# assert true; 425 -- IP address 426 Set_Unsigned_16(Bytes,Start_Byte+ 427 DNS_Types.Packet_Bytes_Range(6+2*(I-Rr_Type.Aaaa_Record_Type.IPV6AddrTypeIndex'First)), 428 AAAA_Record.Ipv6(i)); 429 end loop; 430 end Set_TTL_Data_AAAA_IP; 431 432 433 procedure Get_Query_Name_Type_Class( 434 Input_Packet : in DNS_Types.DNS_Packet; 435 Input_Bytes : in DNS_Types.Packet_Length_Range; 436 Domainname : out RR_Type.wireStringType; 437 Query_Type : out DNS_Types.Query_Type; 438 Query_Class : out DNS_Types.Query_Class; 439 End_Byte : out Dns_types.Packet_Bytes_Range) is 440 Byte : Dns_types.Packet_Bytes_Range := DNS_Types.Packet_Bytes_Range'First; 441 I : Natural := RR_Type.WireStringType'First; 442 QT_Natural, QC_Natural : Natural; 443 function Type_To_Natural is new Ada.Unchecked_Conversion(Dns_Types.Query_Type,Natural); 444 function to_type is new ada.Unchecked_Conversion(natural,dns_types.query_type); 445 function class_to_natural is new ada.Unchecked_Conversion(dns_types.query_class,natural); 446 function To_Class is new Ada.Unchecked_Conversion(Natural,Dns_Types.Query_Class); 447 begin 448 Domainname := RR_Type.WireStringType'(others => ' '); 449 while Integer(Byte) <= Integer(Input_Bytes-5) and then Input_Packet.Bytes(Byte)/=0 450 and then I < RR_Type.WireStringType'Last loop 451 --# assert I>=RR_Type.WireStringType'First and I < RR_Type.WireStringType'Last and 452 --# Byte >= DNS_Types.Packet_Bytes_Range'First and Integer(Byte) <= Integer(Input_Bytes-5); 453 Domainname(I) := Character'Val(Input_Packet.Bytes(Byte)); 454 I := I + 1; 455 Byte := Byte + 1; 456 end loop; 457 Domainname(I) := Character'Val(0); 458-- for I in Byte-2..Byte+4 loop 459-- Ada.Text_IO.Put_Line("byte: " & Dns_Types.Packet_Bytes_Range'Image(I) & ":" & 460-- Natural'Image(natural(Input_Packet.Bytes(I)))); 461-- end loop; 462 QT_Natural := Natural(Input_Packet.Bytes(Byte+1))*256+Natural(Input_Packet.Bytes(Byte+2)); 463 QC_Natural := Natural(Input_Packet.Bytes(Byte+3))*256+Natural(Input_Packet.Bytes(Byte+4)); 464-- ada.Text_IO.put_line("qt: " & natural'image(qt_natural)); 465-- ada.Text_IO.put_line("qc: " & natural'image(qc_natural)); 466 --# accept Warning, 12, type_To_Natural, "unchecked conversions ok"; 467 if QT_Natural >= type_To_Natural(DNS_Types.Query_Type'First) and QT_Natural <= type_To_Natural(DNS_Types.Query_Type'Last) then 468 --# end accept; 469 --# accept Warning, 12, To_Type, "unchecked conversions ok"; 470 Query_Type := To_Type(QT_Natural); 471 --# end accept; 472 if not Query_Type'Valid then 473 Query_Type := DNS_Types.UNIMPLEMENTED; 474 end if; 475 else 476 Query_Type := DNS_Types.UNIMPLEMENTED; 477 end if; 478 --# accept Warning, 12, class_To_Natural, "unchecked conversions ok"; 479 if QC_Natural >= class_to_natural(DNS_Types.Query_Class'First) and QC_Natural <= class_to_natural(DNS_Types.Query_Class'Last) then 480 --# end accept; 481 --# accept Warning, 12, To_Class, "unchecked conversions ok"; 482 Query_Class := To_Class(QC_Natural); 483 --# end accept; 484 if not Query_Class'Valid then 485 Query_Class := DNS_Types.NONE_CLASS; 486 end if; 487 else 488 Query_Class := DNS_Types.NONE_CLASS; 489 end if; 490 End_Byte := Byte + 4; 491 end Get_Query_Name_Type_Class; 492 493 procedure Create_Response_Error( 494 Input_Bytes : in DNS_Types.Packet_Length_Range; 495 Output_Packet : in out DNS_Types.DNS_Packet; 496 Output_Bytes : out DNS_Types.Packet_Length_Range) is 497 begin 498 Output_Packet.Header.AA := True; 499 Output_Packet.Header.RCODE := DNS_Types.Not_Implemented; 500 Output_Packet.Header.ANCount := 0; 501 Output_Bytes := Input_Bytes; 502 end Create_Response_Error; 503 504 procedure Create_Response_AAAA( 505 Start_Byte : in DNS_Types.Packet_Bytes_Range; 506 Domainname : in RR_Type.WireStringType; 507 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 508 Output_Packet : in out DNS_Types.DNS_Packet; 509 Answer_Count : in out DNS_Types.Unsigned_Short; 510 Output_Bytes : out DNS_Types.Packet_Length_Range) is 511 Current_Byte : DNS_Types.Packet_Bytes_Range; 512 ReturnedAAAARecords : Rr_Type.AAAA_Record_Type.AAAARecordBucketType; 513 NumFound : Natural; 514 Response_Counter : Natural; 515 NumAFound : Natural; 516 begin 517 -- accept Flow, 23, ReturnedAAAARecords, "it will fill in enough"; 518 DNS_Table_Pkg.DNS_Table.QueryAAAARecords(DomainName => Domainname, 519 ReturnedRecords => ReturnedAAAARecords, HowMany => NumFound); 520 -- end accept; 521 Current_Byte := Start_Byte; 522 523 if NumFound>=1 then 524 Response_Counter := 1; 525 while Response_Counter <= NumFound and Integer(Current_Byte) < DNS_Types.Packet_Size-(28+DNS_Types.Header_Bits/8) loop 526 --# assert Response_Counter >=1 and Response_Counter <= NumFound 527 --# and Answer_Count = Answer_Count~ 528 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 529 --# and Current_Byte = Start_Byte + 530 --# DNS_Types.Packet_Bytes_Range(28*(Response_Counter-1)) 531 --# and Integer(Current_Byte) < DNS_Types.Packet_Size-(28+DNS_Types.Header_Bits/8) 532 --# and numfound <= rr_type.MaxNumRecords ; 533 -- PTR to character of message 534 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 535 -- AAAA 536 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 537 Output_Packet.Bytes(Current_Byte+4) := 16#1C#; 538 -- IN 539 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 540 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 541 Set_TTL_Data_AAAA_IP(Output_Packet.Bytes,Current_Byte+7,ReturnedAAAARecords(ReturnedAAAARecords'First+(Response_Counter-1))); 542 Response_Counter := Response_Counter + 1; 543 Current_Byte := Current_Byte + 28; 544 end loop; 545 --Output_Bytes := Input_Bytes+DNS_Types.Packet_Length_Range(28*(Response_Counter-1)); 546 else 547 DNS_Table_Pkg.DNS_Table.CountARecords(DomainName => Domainname, 548 HowMany => NumAFound); 549 if NumAFound > 0 then 550 Output_Packet.Header.AA := True; 551 end if; 552 end if; 553 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 554 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(numFound); 555 -- accept Flow, 602, Output_Packet, ReturnedAAAARecords, "initialization is unneeded"; 556 end Create_Response_AAAA; 557 558 procedure Create_Response_A( 559 Start_Byte : in DNS_Types.Packet_Bytes_Range; 560 Domainname : in RR_Type.WireStringType; 561 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 562 Output_Packet : in out DNS_Types.DNS_Packet; 563 Answer_Count : in out DNS_Types.Unsigned_Short; 564 Output_Bytes : out DNS_Types.Packet_Length_Range) is 565 Current_Byte : DNS_Types.Packet_Bytes_Range; 566 ReturnedARecords : Rr_Type.A_Record_Type.ARecordBucketType; 567 NumFound : Natural; 568 Response_Counter : Natural; 569 NumAAAAFound : Natural; 570 begin 571 -- accept Flow, 23, ReturnedARecords, "it will fill in enough"; 572 DNS_Table_Pkg.DNS_Table.QueryARecords(DomainName => Domainname, 573 ReturnedRecords => ReturnedARecords, HowMany => NumFound); 574 -- end accept; 575 Current_Byte := Start_Byte; 576 577 578 if NumFound>=1 then 579 Response_Counter := 1; 580 while Response_Counter <= NumFound and Integer(Current_Byte) < DNS_Types.Packet_Size-(16+DNS_Types.Header_Bits/8) loop 581 --# assert Response_Counter >=1 and Response_Counter <= NumFound 582 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 583 --# and Answer_Count = Answer_Count~ 584 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 585 --# and Current_Byte = Start_Byte + 586 --# DNS_Types.Packet_Bytes_Range(16*(Response_Counter-1)) 587 --# and Integer(Current_Byte) < DNS_Types.Packet_Size-(16+DNS_Types.Header_Bits/8) 588 --# and numfound <= rr_type.MaxNumRecords ; 589 -- PTR to character of message 590 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 591 -- A 592 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 593 Output_Packet.Bytes(Current_Byte+4) := 16#01#; 594 -- IN 595 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 596 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 597 Set_TTL_Data_IP(Output_Packet.Bytes,Current_Byte+7,ReturnedARecords(ReturnedARecords'First+(Response_Counter-1))); 598 Response_Counter := Response_Counter + 1; 599 Current_Byte := Current_Byte + 16; 600 end loop; 601 --Output_Bytes := Input_Bytes+DNS_Types.Packet_Length_Range(16*(Response_Counter-1)); 602 else 603 DNS_Table_Pkg.DNS_Table.CountAAAARecords(DomainName => Domainname, 604 HowMany => NumAAAAFound); 605 if NumAAAAFound > 0 then 606 Output_Packet.Header.AA := True; 607 end if; 608 end if; 609 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 610 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(numFound); 611 -- accept Flow, 602, Output_Packet, ReturnedARecords, "initialization is unneeded"; 612 end Create_Response_A; 613 614--DNSSEC code here {DNSKEY, NSEC, RRSIG} --BSF 615 procedure Create_Response_DNSKEY( 616 Start_Byte : in DNS_Types.Packet_Bytes_Range; 617 Domainname : in RR_Type.WireStringType; 618 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 619 Output_Packet : in out DNS_Types.DNS_Packet; 620 Answer_Count : in out DNS_Types.Unsigned_Short; 621 Output_Bytes : OUT DNS_Types.Packet_Length_Range) IS 622 Current_Byte : DNS_Types.Packet_Bytes_Range; 623 ReturnedDNSKEYRecords : Rr_Type.DNSKEY_Record_Type.DNSKEYRecordBucketType; 624 NumFound : Natural; 625 Response_Counter : Natural; 626 CurrentRec : Rr_Type.DNSKEY_Record_Type.DNSKEYRecordType; 627 bytesUsedInEncodedKey : rr_type.dnskey_record_type.keyLengthValueType; 628 BEGIN 629 -- accept Flow, 23, ReturnedDNSKEYRecords, "it will fill in enough"; 630 DNS_Table_Pkg.DNS_Table.QueryDNSKEYRecords(DomainName => Domainname, 631 ReturnedRecords => ReturnedDNSKEYRecords, HowMany => NumFound); 632 -- end accept; 633 Current_Byte := Start_Byte; -- actually the last byte of the question section 634 if NumFound>=1 then 635 Response_Counter := 1; 636 CurrentRec := ReturnedDNSKEYRecords(Response_Counter); 637 --loop to build the return message 638 WHILE Response_Counter <= NumFound AND 639 Integer(Current_Byte) < DNS_Types.Packet_Size-((16 + Rr_Type.DNSKEY_Record_Type.MaxDNSKeyLength) + DNS_Types.Header_Bits/8) LOOP 640 --# assert Response_Counter >=1 and Response_Counter <= NumFound 641 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 642 --# and Answer_Count = Answer_Count~ 643 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 644 --# and Integer(Current_Byte) < DNS_Types.Packet_Size-(16 + Rr_Type.DNSKEY_Record_Type.MaxDNSKeyLength + DNS_Types.Header_Bits/8) 645 --# and numfound <= rr_type.MaxNumRecords; 646 -- NAME (2 bytes, PTR to name) 647 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 648 -- TYPE (2 bytes, DNSKEY --> 48) 649 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 650 Output_Packet.Bytes(Current_Byte+4) := 16#30#; 651 -- CLASS (2 bytes, IN --> 1) 652 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 653 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 654 --set TTL (4 bytes), RDLENGTH (2 bytes) and RDATA (4 bytes + keylength) fields 655 Set_TTL_Data_DNSKEY(Output_Packet.Bytes,Current_Byte+7,CurrentRec,bytesUsedInEncodedKey); 656 Current_Byte := Current_Byte + DNS_Types.Packet_Bytes_Range(16 + bytesUsedInEncodedKey); 657 Response_Counter := Response_Counter + 1; 658 if Response_Counter <= NumFound then 659 CurrentRec := ReturnedDNSKEYRecords(Response_Counter); 660 END IF; 661 END LOOP; 662 end if; --NumFound >= 1 663 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 664 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(numFound); 665 -- accept Flow, 602, Output_Packet, ReturnedDNSKEYRecords, "initialization is unneeded"; 666 END Create_Response_DNSKEY; 667 668 procedure Create_Response_NSEC( 669 Start_Byte : in DNS_Types.Packet_Bytes_Range; 670 Domainname : in RR_Type.WireStringType; 671 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 672 Output_Packet : in out DNS_Types.DNS_Packet; 673 Answer_Count : in out DNS_Types.Unsigned_Short; 674 Output_Bytes : OUT DNS_Types.Packet_Length_Range) IS 675 Current_Byte : DNS_Types.Packet_Bytes_Range; 676 ReturnedNSECRecords : Rr_Type.NSEC_Record_Type.NSECRecordBucketType; 677 NumFound : Natural; 678 Response_Counter : Natural; 679 CurrentRec : Rr_Type.NSEC_Record_Type.NSECRecordType; 680 bytesUsedInRRData : DNS_Types.Packet_Length_Range; 681 BEGIN 682 -- accept Flow, 23, ReturnedNSECRecords, "it will fill in enough"; 683 DNS_Table_Pkg.DNS_Table.QueryNSECRecords(DomainName => Domainname, 684 ReturnedRecords => ReturnedNSECRecords, HowMany => NumFound); 685 -- end accept; 686 Current_Byte := Start_Byte; -- actually the last byte of the question section 687 if NumFound>=1 then 688 Response_Counter := 1; 689 CurrentRec := ReturnedNSECRecords(Response_Counter); 690 WHILE Response_Counter <= NumFound AND Integer(Current_Byte) < 691 DNS_Types.Packet_Size-((((12 + Rr_Type.NSEC_Record_Type.MaxRRDataLength) 692 + rr_type.maxDomainNameLength)+1) + DNS_Types.Header_Bits/8) LOOP 693 -- NAME (2 bytes, PTR to name) 694 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 695 -- TYPE (2 bytes, NSEC --> 47) 696 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 697 Output_Packet.Bytes(Current_Byte+4) := 16#2f#; 698 -- CLASS (2 bytes, IN --> 1) 699 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 700 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 701 --set TTL (4 bytes), RDLENGTH (2 bytes) and RDATA (domainNameLength + rrListLength) fields 702 Set_TTL_Data_NSEC(Output_Packet.Bytes,Current_Byte+7,CurrentRec,bytesUsedInRRData); 703 --# assert Response_Counter >=1 and Response_Counter <= NumFound 704 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 705 --# and Answer_Count = Answer_Count~ 706 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 707 --# and Integer(Current_Byte) < DNS_Types.Packet_Size-((12 + Rr_Type.NSEC_Record_Type.MaxRRDataLength) 708 --# + (rr_type.maxDomainNameLength+1) + DNS_Types.Header_Bits/8) 709 --# and bytesUsedInRRData <= DNS_Types.Packet_Length_Range(Rr_Type.NSEC_Record_Type.MaxRRDataLength) 710 --# and numfound <= rr_type.MaxNumRecords; 711 Current_Byte := Current_Byte + DNS_Types.Packet_Bytes_Range(12 + bytesUsedInRRData); 712 Response_Counter := Response_Counter + 1; 713 if Response_Counter <= NumFound then 714 CurrentRec := ReturnedNSECRecords(Response_Counter); 715 END IF; 716 END LOOP; 717 end if; --NumFound >= 1 718 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 719 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(numFound); 720 -- accept Flow, 602, Output_Packet, ReturnedNSECRecords, "initialization is unneeded"; 721 END Create_Response_NSEC; 722 723 procedure Create_Response_RRSIG( 724 Start_Byte : in DNS_Types.Packet_Bytes_Range; 725 Domainname : in RR_Type.WireStringType; 726 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 727 Output_Packet : in out DNS_Types.DNS_Packet; 728 Answer_Count : in out DNS_Types.Unsigned_Short; 729 Output_Bytes : OUT DNS_Types.Packet_Length_Range) IS 730 Current_Byte : DNS_Types.Packet_Bytes_Range; 731 ReturnedRRSIGRecords : Rr_Type.RRSIG_Record_Type.RRSIGRecordBucketType; 732 NumFound : Natural; 733 Response_Counter : Natural; 734 CurrentRec : Rr_Type.RRSIG_Record_Type.RRSIGRecordType; 735 bytesUsedOnWire : DNS_Types.Packet_Bytes_Range; 736 BEGIN 737 -- accept Flow, 23, ReturnedRRSIGRecords, "it will fill in enough"; 738 DNS_Table_Pkg.DNS_Table.QueryRRSIGRecords(DomainName => Domainname, 739 ReturnedRecords => ReturnedRRSIGRecords, HowMany => NumFound); 740 -- end accept; 741 Current_Byte := Start_Byte; -- actually the last byte of the question section 742 IF NumFound>=1 THEN 743 Response_Counter := 1; 744 CurrentRec := ReturnedRRSIGRecords(Response_Counter); 745 --loop to build the return message 746 WHILE Response_Counter <= NumFound AND 747 Integer(Current_Byte) < DNS_Types.Packet_Size-(((30 + Rr_Type.MaxDomainNameLength) + Rr_Type.Rrsig_Record_Type.maxrrsigLength) + DNS_Types.Header_Bits/8) LOOP 748 --# assert Response_Counter >=1 and Response_Counter <= NumFound 749 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 750 --# and Answer_Count = Answer_Count~ 751 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 752 --# and Integer(Current_Byte) < DNS_Types.Packet_Size-(((30 + Rr_Type.MaxDomainNameLength) + Rr_Type.Rrsig_Record_Type.maxrrsigLength) + DNS_Types.Header_Bits/8) 753 --# and numfound <= rr_type.MaxNumRecords; 754 -- NAME (2 bytes, PTR to name) 755 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 756 -- TYPE (2 bytes, DNSKEY --> 46) 757 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 758 Output_Packet.Bytes(Current_Byte+4) := 16#2E#; 759 -- CLASS (2 bytes, IN --> 1) 760 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 761 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 762 --set TTL (4 bytes), RDLENGTH (2 bytes) and RDATA (18 bytes + name length + sig length) fields 763 Set_TTL_Data_RRSIG(Output_Packet.Bytes,Current_Byte+7,CurrentRec,bytesUsedOnWire); 764 Current_Byte := (Current_Byte + 6) + bytesUsedOnWire; 765 Response_Counter := Response_Counter + 1; 766 if Response_Counter <= NumFound then 767 CurrentRec := ReturnedRRSIGRecords(Response_Counter); 768 END IF; 769 end loop; 770 end if; --NumFound >= 1 771 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 772 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(numFound); 773 -- accept Flow, 602, Output_Packet, ReturnedRRSIGRecords, "initialization is unneeded"; 774 END Create_Response_RRSIG; 775 776 procedure Create_Response_NS( 777 Start_Byte : in DNS_Types.Packet_Bytes_Range; 778 Domainname : in RR_Type.WireStringType; 779 Num_Found : out RR_Type.NumberOfRecordsType; 780 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 781 Qname_Locations : out QNAME_PTR_RANGE_Array; 782 Replies : out RR_Type.ns_record_type.NSRecordBucketType; 783 Output_Packet : in out DNS_Types.DNS_Packet; 784 Answer_Count : in out DNS_Types.Unsigned_Short; 785 Output_Bytes : out DNS_Types.Packet_Length_Range) is 786 Response_Counter : Natural; 787 Current_Byte : DNS_Types.Packet_Bytes_Range; 788 Current_Name_Length : RR_Type.WireStringTypeIndex; 789 begin 790 Qname_Locations := QNAME_PTR_RANGE_Array'(others => 0); 791 Current_Byte := Start_Byte; 792 -- accept Flow, 23, Replies, "it will fill in enough"; 793 DNS_Table_Pkg.DNS_Table.QueryNSRecords( 794 DomainName => Domainname, 795 ReturnedRecords => Replies, 796 HowMany => Num_Found); 797 -- end accept; 798 if Num_Found>=1 then 799 Response_Counter := 1; 800 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).nameServer); 801 while Response_Counter <= Num_Found and then 802 Integer(Current_Byte) < (DNS_Types.Packet_Size-(12+DNS_Types.Header_Bits/8))- 803 (Current_Name_Length) loop 804 --# assert Response_Counter >=1 and Response_Counter <= Num_Found 805 --# and current_name_length >=1 and current_name_length<=rr_type.WireStringTypeIndex'last 806 --# and Num_Found <= rr_type.MaxNumRecords 807 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 808 --# and Answer_Count = Answer_Count~ 809 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 810 --# and Integer(Current_Byte) < (DNS_Types.Packet_Size-(12+DNS_Types.Header_Bits/8))- 811 --# (Current_Name_Length) 812 --# and Current_Byte >= 0; 813 -- PTR to character of message 814 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 815 -- NS 816 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 817 Output_Packet.Bytes(Current_Byte+4) := 16#02#; 818 -- IN 819 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 820 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 821 Qname_Locations(Response_Counter) := DNS_Types.QNAME_PTR_RANGE( 822 (Current_Byte+12)+ DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 823 Set_TTL_Data_NS_Response(Output_Packet.Bytes,Current_Byte+7, 824 Replies(Response_Counter),Current_Name_Length); 825 Response_Counter := Response_Counter + 1; 826 Current_Byte := (Current_Byte + 12) + DNS_Types.Packet_Bytes_Range(Current_Name_Length); 827 if Response_Counter <= Num_Found then 828 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).nameServer); 829 end if; 830 end loop; 831 end if; 832 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 833 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(Num_Found); 834 -- accept Flow, 602, Output_Packet, Replies, "initialization is unneeded"; 835 -- accept Flow, 602, Output_Bytes, Replies, "initialization is unneeded"; 836 -- accept Flow, 602, Replies, Replies, "initialization is unneeded"; 837 -- accept Flow, 602, Qname_Locations, Replies, "initialization is unneeded"; 838 end Create_Response_NS; 839 840 procedure Create_Response_PTR( 841 Start_Byte : in DNS_Types.Packet_Bytes_Range; 842 Domainname : in RR_Type.WireStringType; 843 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 844 Output_Packet : in out DNS_Types.DNS_Packet; 845 Answer_Count : in out DNS_Types.Unsigned_Short; 846 Output_Bytes : out DNS_Types.Packet_Length_Range) is 847 Num_Found : RR_Type.NumberOfRecordsType; 848 Response_Counter : Natural; 849 Current_Byte : DNS_Types.Packet_Bytes_Range; 850 Current_Name_Length : RR_Type.WireStringTypeIndex; 851 Replies : RR_Type.PTR_record_type.PTRRecordBucketType; 852 begin 853 Current_Byte := Start_Byte; 854 -- accept Flow, 23, Replies, "it will fill in enough"; 855 DNS_Table_Pkg.DNS_Table.QueryPTRRecords( 856 DomainName => Domainname, 857 ReturnedRecords => Replies, 858 HowMany => Num_Found); 859 -- end accept; 860 if Num_Found>=1 then 861 Response_Counter := 1; 862 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).domainname); 863 while Response_Counter <= Num_Found and then 864 Integer(Current_Byte) < (DNS_Types.Packet_Size-(12+DNS_Types.Header_Bits/8))- 865 (Current_Name_Length) loop 866 --# assert Response_Counter >=1 and Response_Counter <= Num_Found 867 --# and current_name_length >=1 and current_name_length<=rr_type.WireStringTypeIndex'last 868 --# and Num_Found <= rr_type.MaxNumRecords 869 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 870 --# and Answer_Count = Answer_Count~ 871 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 872 --# and Integer(Current_Byte) < (DNS_Types.Packet_Size-(12+DNS_Types.Header_Bits/8))- 873 --# (Current_Name_Length) 874 --# and Current_Byte >= 0; 875 -- PTR to character of message 876 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 877 -- PTR 878 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 879 Output_Packet.Bytes(Current_Byte+4) := 16#0C#; 880 -- IN 881 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 882 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 883 Set_TTL_Data_PTR_Response(Output_Packet.Bytes,Current_Byte+7, 884 Replies(Response_Counter),Current_Name_Length); 885 Response_Counter := Response_Counter + 1; 886 Current_Byte := (Current_Byte + 12) + DNS_Types.Packet_Bytes_Range(Current_Name_Length); 887 if Response_Counter <= Num_Found then 888 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).domainname); 889 end if; 890 end loop; 891 end if; 892 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 893 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(Num_Found); 894 -- accept Flow, 602, Output_Packet, Replies, "initialization is unneeded"; 895 -- accept Flow, 602, Output_Bytes, Replies, "initialization is unneeded"; 896 end Create_Response_PTR; 897 898 procedure Create_Response_MX( 899 Start_Byte : in DNS_Types.Packet_Bytes_Range; 900 Domainname : in RR_Type.WireStringType; 901 Num_Found : out RR_Type.NumberOfRecordsType; 902 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 903 Qname_Locations : out QNAME_PTR_RANGE_Array; 904 Replies : out RR_Type.mx_record_type.MXRecordBucketType; 905 Output_Packet : in out DNS_Types.DNS_Packet; 906 Answer_Count : in out DNS_Types.Unsigned_Short; 907 Output_Bytes : out DNS_Types.Packet_Length_Range) is 908 Response_Counter : Natural; 909 Current_Byte : DNS_Types.Packet_Bytes_Range; 910 Current_Name_Length : RR_Type.WireStringTypeIndex; 911 begin 912 Qname_Locations := QNAME_PTR_RANGE_Array'(others => 0); 913 Current_Byte := Start_Byte; 914 -- accept Flow, 23, Replies, "it will fill in enough"; 915 DNS_Table_Pkg.DNS_Table.QueryMXRecords( 916 DomainName => Domainname, 917 ReturnedRecords => Replies, 918 HowMany => Num_Found); 919 -- end accept; 920 if Num_Found>=1 then 921 Response_Counter := 1; 922 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).mailExchanger); 923 while Response_Counter <= Num_Found and then 924 Integer(Current_Byte) < (DNS_Types.Packet_Size-(14+DNS_Types.Header_Bits/8))- 925 (Current_Name_Length) loop 926 --# assert Response_Counter >=1 and Response_Counter <= Num_Found 927 --# and current_name_length >=1 and current_name_length<=rr_type.WireStringTypeIndex'last 928 --# and Num_Found <= rr_type.MaxNumRecords 929 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 930 --# and Answer_Count = Answer_Count~ 931 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 932 --# and Integer(Current_Byte) < (DNS_Types.Packet_Size-(14+DNS_Types.Header_Bits/8))- 933 --# (Current_Name_Length) 934 --# and Current_Byte >= 0; 935 -- PTR to character of message 936 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 937 -- MX 938 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 939 Output_Packet.Bytes(Current_Byte+4) := 16#0F#; 940 -- IN 941 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 942 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 943 Qname_Locations(Response_Counter) := DNS_Types.QNAME_PTR_RANGE( 944 (Current_Byte+14)+ DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 945 Set_TTL_Data_MX_Response(Output_Packet.Bytes,Current_Byte+7, 946 Replies(Response_Counter),Current_Name_Length); 947 Response_Counter := Response_Counter + 1; 948 Current_Byte := (Current_Byte + 14) + DNS_Types.Packet_Bytes_Range(Current_Name_Length); 949 if Response_Counter <= Num_Found then 950 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).mailExchanger); 951 end if; 952 end loop; 953 end if; 954 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 955 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(Num_Found); 956 -- accept Flow, 602, Output_Packet, Replies, "initialization is unneeded"; 957 -- accept Flow, 602, Output_Bytes, Replies, "initialization is unneeded"; 958 -- accept Flow, 602, Replies, Replies, "initialization is unneeded"; 959 -- accept Flow, 602, Qname_Locations, Replies, "initialization is unneeded"; 960 end Create_Response_MX; 961 962 procedure Create_Response_SRV( 963 Start_Byte : in DNS_Types.Packet_Bytes_Range; 964 Domainname : in RR_Type.WireStringType; 965 Num_Found : out RR_Type.NumberOfRecordsType; 966 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 967 Qname_Locations : out QNAME_PTR_RANGE_Array; 968 Replies : out RR_Type.srv_record_type.SRVRecordBucketType; 969 Output_Packet : in out DNS_Types.DNS_Packet; 970 Answer_Count : in out DNS_Types.Unsigned_Short; 971 Output_Bytes : out DNS_Types.Packet_Length_Range) is 972 Response_Counter : Natural; 973 Current_Byte : DNS_Types.Packet_Bytes_Range; 974 Current_Name_Length : RR_Type.WireStringTypeIndex; 975 begin 976 Qname_Locations := QNAME_PTR_RANGE_Array'(others => 0); 977 Current_Byte := Start_Byte; 978 -- accept Flow, 23, Replies, "it will fill in enough"; 979 DNS_Table_Pkg.DNS_Table.QuerySRVRecords( 980 DomainName => Domainname, 981 ReturnedRecords => Replies, 982 HowMany => Num_Found); 983 -- end accept; 984 if Num_Found>=1 then 985 Response_Counter := 1; 986 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).ServerName); 987 while Response_Counter <= Num_Found and then 988 Integer(Current_Byte) < (DNS_Types.Packet_Size-(18+DNS_Types.Header_Bits/8))- 989 (Current_Name_Length) loop 990 --# assert Response_Counter >=1 and Response_Counter <= Num_Found 991 --# and current_name_length >=1 and current_name_length<=rr_type.WireStringTypeIndex'last 992 --# and Num_Found <= rr_type.MaxNumRecords 993 --# and Integer(Start_Byte) <= DNS_Types.Packet_Size 994 --# and Answer_Count = Answer_Count~ 995 --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords) 996 --# and Integer(Current_Byte) < (DNS_Types.Packet_Size-(18+DNS_Types.Header_Bits/8))- 997 --# (Current_Name_Length) 998 --# and Current_Byte >= 0; 999 -- PTR to character of message 1000 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 1001 -- SRV 1002 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 1003 Output_Packet.Bytes(Current_Byte+4) := 16#21#; 1004 -- IN 1005 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 1006 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 1007 Qname_Locations(Response_Counter) := DNS_Types.QNAME_PTR_RANGE( 1008 (Current_Byte+18)+ DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); -- offset = 18 1009 Set_TTL_Data_SRV_Response(Output_Packet.Bytes,Current_Byte+7, 1010 Replies(Response_Counter),Current_Name_Length); 1011 Response_Counter := Response_Counter + 1; 1012 Current_Byte := (Current_Byte + 18) + DNS_Types.Packet_Bytes_Range(Current_Name_Length); -- offset = 18 1013 if Response_Counter <= Num_Found then 1014 Current_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).serverName); 1015 end if; 1016 end loop; 1017 end if; 1018 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 1019 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(Num_Found); 1020 -- accept Flow, 602, Output_Packet, Replies, "initialization is unneeded"; 1021 -- accept Flow, 602, Output_Bytes, Replies, "initialization is unneeded"; 1022 -- accept Flow, 602, Replies, Replies, "initialization is unneeded"; 1023 -- accept Flow, 602, Qname_Locations, Replies, "initialization is unneeded"; 1024 end Create_Response_SRV; 1025 1026 procedure Create_Response_SOA( 1027 Start_Byte : in DNS_Types.Packet_Bytes_Range; 1028 Domainname : in RR_Type.WireStringType; 1029 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 1030 Output_Packet : in out DNS_Types.DNS_Packet; 1031 Answer_Count : in out DNS_Types.Unsigned_Short; 1032 Output_Bytes : out DNS_Types.Packet_Length_Range) is 1033 Response_Counter : Natural; 1034 Current_Byte : DNS_Types.Packet_Bytes_Range; 1035 Nameserver_Name_Length : RR_Type.WireStringTypeIndex; 1036 Mailbox_Name_Length : RR_Type.WireStringTypeIndex; 1037 Num_Found : RR_Type.NumberOfRecordsType; 1038 Replies : RR_Type.SOA_record_type.SOARecordBucketType; 1039 begin 1040 Current_Byte := Start_Byte; 1041 -- accept Flow, 23, Replies, "it will fill in enough"; 1042 DNS_Table_Pkg.DNS_Table.QuerySOARecords( 1043 DomainName => Domainname, 1044 ReturnedRecords => Replies, 1045 HowMany => Num_Found); 1046 -- end accept; 1047 if Num_Found>=1 then 1048 Response_Counter := 1; 1049 Nameserver_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).nameserver); 1050 Mailbox_Name_Length := RR_Type.WireNameLength(Replies(Response_Counter).email); 1051 if Integer(Current_Byte) < (DNS_Types.Packet_Size-(32+DNS_Types.Header_Bits/8))- 1052 (Nameserver_Name_Length+Mailbox_Name_Length) then 1053 -- PTR to character of message 1054 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 1055 -- SOA 1056 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 1057 Output_Packet.Bytes(Current_Byte+4) := 16#06#; 1058 -- IN 1059 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 1060 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 1061 Set_TTL_Data_SOA_Response(Output_Packet.Bytes,Current_Byte+7, 1062 Replies(Response_Counter),Nameserver_Name_Length,Mailbox_Name_Length); 1063 Current_Byte := (Current_Byte + 32) + DNS_Types.Packet_Bytes_Range( 1064 Nameserver_Name_Length+Mailbox_name_Length); 1065 end if; 1066 end if; 1067 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 1068 Answer_Count := Answer_Count + DNS_Types.Unsigned_Short(Num_Found); 1069 -- accept Flow, 602, Output_Packet, Replies, "initialization is unneeded"; 1070 -- accept Flow, 602, Output_Bytes, Replies, "initialization is unneeded"; 1071 end Create_Response_SOA; 1072 1073 1074 procedure Process_Response_Cname( 1075 Start_Byte : in DNS_Types.Packet_Bytes_Range; 1076 Cnames : in RR_Type.cname_record_type.CNAMERecordBucketType; 1077 Domainname : out RR_Type.WireStringType; 1078 Qname_Location : in out DNS_Types.QNAME_PTR_RANGE; 1079 Output_Packet : in out DNS_Types.DNS_Packet; 1080 Output_Bytes : out DNS_Types.Packet_Length_Range) is 1081 Current_Byte : DNS_Types.Packet_Bytes_Range; 1082 Name_Length : RR_Type.WireStringTypeIndex; 1083 I : RR_Type.WireStringTypeIndex; 1084 begin 1085-- Cnames(Cnames'First).CanonicalDomainName := Character'Val(8) & "carlisle" & Character'Val(4) & 1086-- "dfcs" & Character'Val(5) & "usafa" & Character'Val(3) & "edu" & Character'Val(0) & 1087-- " "; 1088 Current_Byte := Start_Byte; 1089 Domainname := Cnames(Cnames'First).CanonicalDomainName; 1090 Name_Length := RR_Type.WirenameLength(Cnames(Cnames'First).CanonicalDomainName); 1091 if Integer(Current_Byte) < DNS_Types.Packet_Size-(12+DNS_Types.Header_Bits/8) then 1092 -- PTR to character of message 1093 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+1,Unsigned_Types.Unsigned16(Qname_Location)+16#C000#); 1094 -- CNAME 1095 Output_Packet.Bytes(Current_Byte+3) := 16#00#; 1096 Output_Packet.Bytes(Current_Byte+4) := 16#05#; 1097 -- IN 1098 Output_Packet.Bytes(Current_Byte+5) := 16#00#; 1099 Output_Packet.Bytes(Current_Byte+6) := 16#01#; 1100 -- TTL 1101 Set_Unsigned_32(Output_Packet.Bytes,Current_Byte+7,Cnames(Cnames'First).TtlInSeconds); 1102 Set_Unsigned_16(Output_Packet.Bytes,Current_Byte+11,Unsigned_Types.Unsigned16(Name_Length)); 1103 Current_Byte := Current_Byte + 12; 1104 end if; 1105 Qname_Location := DNS_Types.QNAME_PTR_RANGE( 1106 (Integer(Current_Byte)) + DNS_Types.Header_Bits/8); 1107 I := 1; 1108 while I<=Name_Length and I<RR_Type.WireStringTypeIndex'Last and 1109 Integer(Current_Byte)+DNS_Types.Header_Bits/8<DNS_Types.Packet_Size loop 1110 --# assert I<RR_Type.WireStringTypeIndex'Last and 1111 --# I<=Name_Length and 1112 --# Output_Packet.Header.ANCount = 0 and 1113 --# Current_Byte >= Start_Byte and 1114 --# Integer(Current_Byte)+DNS_Types.Header_Bits/8<DNS_Types.Packet_Size; 1115 Current_Byte := Current_Byte + 1; 1116 Output_Packet.Bytes(Current_Byte) := DNS_Types.Byte(Character'Pos(Cnames(Cnames'First).CanonicalDomainName(I))); 1117 I := I + 1; 1118 end loop; 1119 Output_Bytes := DNS_Types.Packet_Length_Range(Current_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 1120 Output_Packet.Header.ANCount := Output_Packet.Header.ANCount + 1; 1121 end Process_Response_Cname; 1122 1123 procedure Trim_Name( 1124 Domainname : in RR_Type.WireStringType; 1125 Trimmed_name : out RR_Type.WireStringType; 1126 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 1127 New_Qname_Location : out DNS_Types.QNAME_PTR_RANGE) is 1128 Zone_Length : Natural; 1129 begin 1130 Zone_Length := natural(character'pos(domainname(domainname'first))+1); 1131 Trimmed_Name := RR_Type.WireStringType'(others => ' '); 1132 New_Qname_Location := Qname_Location; 1133 if Zone_Length > 0 and Zone_Length < Rr_Type.WireStringTypeIndex'Last then 1134 New_Qname_Location := New_Qname_Location + DNS_Types.QNAME_PTR_RANGE(Zone_Length); 1135 -- the assertion below is kind of interesting b/c we need to tell SPARK 1136 -- that zone_Length hasn't changed, and I don't really use it in the loop 1137 for I in RR_Type.WireStringTypeIndex range 1..RR_Type.WireStringTypeIndex'Last-natural(character'pos(domainname(domainname'first))+1) loop 1138 --# assert I+Zone_Length<=RR_Type.WireStringTypeIndex'Last and I>=1 and 1139 --# zone_length = natural(character'pos(domainname(domainname'first))+1); 1140 Trimmed_Name(I) := Domainname(I+natural(character'pos(domainname(domainname'first))+1)); 1141 end loop; 1142 end if; 1143 end Trim_Name; 1144 1145 procedure Create_NXDOMAIN_Response( 1146 Start_Byte : in DNS_Types.Packet_Bytes_Range; 1147 Domainname : in RR_Type.WireStringType; 1148 Qname_Location : in DNS_Types.QNAME_PTR_RANGE; 1149 Output_Packet : in out DNS_Types.DNS_Packet; 1150 Output_Bytes : out DNS_Types.Packet_Length_Range) is 1151 Answer_Count : DNS_Types.Unsigned_Short := 0; 1152 Amount_Trimmed : Natural := 0; 1153 Trimmed_Name : RR_Type.WireStringType; 1154 Current_Name : RR_Type.WireStringType; 1155 Current_Qname_Location : DNS_Types.QNAME_PTR_RANGE; 1156 New_Qname_Location : DNS_Types.QNAME_PTR_RANGE; 1157 begin 1158 Current_Qname_Location := Qname_Location; 1159 Output_Bytes := DNS_Types.Packet_Length_Range(Start_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 1160 Current_Name := Domainname; 1161 Output_Packet.Header.RCODE := DNS_Types.Name_Error; 1162 Output_Packet.Header.ANCount := 0; 1163 1164 -- Amount_Trimmed is used to guarantee we don't end up in an infinite loop 1165 while Answer_Count=0 and Amount_Trimmed<RR_Type.WireStringType'Last and 1166 Natural(Character'Pos(Current_Name(Current_Name'First)))/=0 and 1167 Current_Qname_Location <= DNS_Types.QNAME_PTR_RANGE(Output_Bytes) loop 1168 --# assert Answer_Count=0 and Amount_Trimmed>=0 and Amount_Trimmed<RR_Type.WireStringType'Last 1169 --# and Output_Bytes <= DNS_Types.Packet_Length_Range'Last 1170 --# and Current_Qname_Location <= DNS_Types.QNAME_PTR_RANGE(Output_Bytes); 1171 Trim_Name( 1172 Domainname => Current_Name, 1173 Trimmed_Name => Trimmed_Name, 1174 Qname_Location => Current_Qname_Location, 1175 New_Qname_Location => New_Qname_Location); 1176 Create_Response_SOA( 1177 Start_Byte => Start_Byte, 1178 Domainname => Trimmed_name, 1179 Qname_Location => New_Qname_Location, 1180 Output_Packet => Output_Packet, 1181 Answer_Count => Answer_Count, 1182 Output_Bytes => Output_Bytes); 1183 Current_Name := Trimmed_Name; 1184 Current_Qname_Location := New_Qname_Location; 1185 Amount_Trimmed := Amount_Trimmed + Natural(Character'Pos(Domainname(Domainname'First))+1); 1186 end loop; 1187 if Answer_Count >= 1 then 1188 Output_Packet.Header.AA := True; 1189 end if; 1190 Output_Packet.Header.NSCount := Answer_Count; 1191 end Create_NXDOMAIN_Response; 1192 1193 -- if we get in an EDNS option, we will add a response in kind 1194 procedure Create_Response_EDNS( 1195 Input_Packet : in DNS_Types.DNS_Packet; 1196 Input_Bytes : in DNS_Types.Packet_Length_Range; 1197 Query_End_Byte : in DNS_Types.Packet_Bytes_Range; 1198 Start_Byte : in DNS_Types.Packet_Bytes_Range; 1199 Output_Packet : in out DNS_Types.DNS_Packet; 1200 Output_Bytes : out DNS_Types.Packet_Length_Range; 1201 Additional_Count : in out DNS_Types.Unsigned_Short; 1202 DNSSEC : out Boolean; 1203 Max_Transmit : out DNS_Types.Packet_Length_Range) is 1204 EDNS_Rec : DNS_Types.EDNS_Record; 1205 function To_Query_Type is new Ada.Unchecked_Conversion(DNS_Types.Unsigned_Short,DNS_Types.Query_Type); 1206 function From_Query_Type is new Ada.Unchecked_Conversion(DNS_Types.Query_Type,DNS_Types.Unsigned_Short); 1207 begin 1208 Max_Transmit := DNS_Types.UDP_Max_Size; 1209 Output_Bytes := DNS_Types.Packet_Length_Range(Start_Byte + DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 1210 DNSSEC := False; 1211 1212 -- if there's more to the packet, check for the OPT code 1213 if (Integer(Query_End_Byte)+11)+(DNS_Types.Header_Bits/8)<=Integer(Input_Bytes) and 1214 (Integer(Start_Byte)+11)+(DNS_Types.Header_Bits/8)<DNS_Types.Packet_Size then 1215 EDNS_Rec.Root := Character'Val(Input_Packet.Bytes(Query_End_Byte+1)); 1216 --# accept Warning, 12, To_Query_Type, "unchecked conversions ok"; 1217 EDNS_Rec.Code := To_Query_Type(DNS_Types.Unsigned_Short( 1218 Input_Packet.Bytes(Query_End_Byte+2))*256+ 1219 DNS_Types.Unsigned_Short(Input_Packet.Bytes(Query_End_Byte+3))); 1220 if EDNS_Rec.Root = Character'Val(0) and 1221 EDNS_Rec.Code = DNS_Types.OPT then 1222 EDNS_Rec.Payload_Size := DNS_Types.Unsigned_Short(Input_Packet.Bytes( 1223 Query_End_Byte+4))*256+ 1224 DNS_Types.Unsigned_Short(Input_Packet.Bytes(Query_End_Byte+5)); 1225 --EDNS_Rec.RCODE := Input_Packet.Bytes(Query_End_Byte+6); 1226 --EDNS_Rec.Version := Input_Packet.Bytes(Query_End_Byte+7); 1227 EDNS_Rec.ZTop := Input_Packet.Bytes(Query_End_Byte+8); 1228 --EDNS_Rec.ZBottom := Input_Packet.Bytes(Query_End_Byte+9); 1229 --EDNS_Rec.RDLEN := DNS_Types.Unsigned_Short( 1230 -- Input_Packet.Bytes(Query_End_Byte+10))*256+ 1231 -- DNS_Types.Unsigned_Short(Input_Packet.Bytes(Query_End_Byte+11)); 1232 1233 -- when we respond, we'll respond with AT LEAST UDP_Max_Size, 1234 -- but no bigger than our Packet_Size 1235 Max_Transmit := DNS_Types.Packet_Length_Range( 1236 DNS_Types.Unsigned_Short'Min(DNS_Types.Packet_Size, 1237 EDNS_Rec.Payload_Size)); 1238 Max_Transmit := DNS_Types.Packet_Length_Range'Max( 1239 DNS_Types.UDP_Max_Size, Max_Transmit); 1240 1241 Output_Packet.Bytes(Start_Byte+1) := 0; 1242 -- high order byte of OPT is 0 1243 Output_Packet.Bytes(Start_Byte+2) := 0; 1244 -- the mod here is superfluous as OPT = 41 1245 --# accept Warning, 12, From_Query_Type, "unchecked conversions ok"; 1246 Output_Packet.Bytes(Start_Byte+3) := DNS_Types.Byte( 1247 From_Query_Type(DNS_Types.OPT) mod 256); 1248 1249 -- split unsigned short into two bytes 1250 Output_Packet.Bytes(Start_Byte+4) := DNS_Types.Byte( 1251 Max_Transmit/256); 1252 Output_Packet.Bytes(Start_Byte+5) := DNS_Types.Byte( 1253 Max_Transmit mod 256); 1254 1255 Output_Packet.Bytes(Start_Byte+6) := 0; 1256 Output_Packet.Bytes(Start_Byte+7) := 0; 1257 -- FLAGS (DNSSEC ONLY), see RFC 3225 1258 if (EDNS_Rec.ZTop and Dns_Types.DNSSECMASK) /= 0 then 1259 Output_Packet.Bytes(Start_Byte+8) := Dns_Types.DNSSECMASK; 1260 DNSSEC := True; 1261 else 1262 Output_Packet.Bytes(Start_Byte+8) := 0; 1263 end if; 1264 Output_Packet.Bytes(Start_Byte+9) := 0; 1265 -- RDLEN = 0 1266 Output_Packet.Bytes(Start_Byte+10) := 0; 1267 Output_Packet.Bytes(Start_Byte+11) := 0; 1268 1269 Additional_Count := Additional_Count + 1; 1270 Output_Bytes := DNS_Types.Packet_Length_Range((Start_Byte + 11) + 1271 DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8)); 1272 end if; 1273 end if; 1274 end Create_Response_EDNS; 1275 1276 procedure Create_Response( 1277 Input_Packet : in DNS_Types.DNS_Packet; 1278 Input_Bytes : in DNS_Types.Packet_Length_Range; 1279 Output_Packet : in out DNS_Types.DNS_Packet; 1280 Output_Bytes : out DNS_Types.Packet_Length_Range; 1281 Max_Transmit : out DNS_Types.Packet_Length_Range) is 1282 Start_Byte : DNS_Types.Packet_Bytes_Range; 1283 Query_End_Byte : DNS_Types.Packet_Bytes_Range; 1284 Domainname : RR_Type.WireStringType; 1285 Query_Type : DNS_Types.Query_Type; 1286 Query_Class : DNS_Types.Query_Class; 1287 NumFound : Natural; 1288 Counter : Natural; 1289 Qname_Location : DNS_Types.QNAME_PTR_RANGE := 12; 1290 Qname_Locations : QNAME_PTR_RANGE_Array; 1291 ReturnedCNAMERecords : Rr_Type.CNAME_Record_Type.CNAMERecordBucketType; 1292 NS_Replies : RR_Type.Ns_Record_Type.NSRecordBucketType; 1293 MX_Replies : RR_Type.MX_Record_Type.MXRecordBucketType; 1294 SRV_Replies : RR_Type.srv_record_type.SRVRecordBucketType; 1295 Answer_Count : DNS_Types.Unsigned_Short; 1296 Additional_Count : DNS_Types.Unsigned_Short; 1297 DNSSEC : Boolean; 1298 begin 1299 1300 -- I would like to only copy the header here, but I get a flow error!! 1301 --# accept Flow, 10, Output_Packet.Header.QR, 1302 --# "The rest of the header fields retain their newly assigned values"; 1303 --# accept Flow, 10, Output_Packet.Header.ANCOUNT, 1304 --# "The rest of the header fields retain their newly assigned values"; 1305 --# accept Flow, 10, Output_Packet.Header.AA, 1306 --# "The rest of the header fields retain their newly assigned values"; 1307 -- accept Flow, 10, Output_Packet.Header.RCODE, 1308 -- "The rest of the header fields retain their newly assigned values"; 1309 Output_Packet.Header := Input_Packet.Header; 1310 Output_Packet.Header.AA := False; 1311 --# end accept; 1312 --# end accept; 1313 --# end accept; 1314 -- end accept; 1315 Output_Packet.Header.QR := True; 1316 -- Keep # of queries and send the query back!! (i.e. don't do line below) 1317 -- Response_Header.QDCOUNT := 0; 1318 1319 --# assert Integer(Input_Bytes) >=DNS_Types.Header_Bits/8+1 1320 --# and Qname_Location >=0 and Qname_Location < 16384 1321 --# and Integer(Input_Bytes) < 312; 1322 Get_Query_Name_Type_Class(Input_Packet, Input_Bytes, Domainname, Query_Type, Query_Class, Query_End_Byte); 1323 Start_Byte := Query_End_Byte; 1324 --Start_Byte := DNS_Types.Packet_Bytes_Range(Input_Bytes) - 1325 -- DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8); 1326 for I in DNS_Types.Packet_Bytes_Range range 1..Start_Byte loop 1327 --# assert Integer(Input_Bytes) >=DNS_Types.Header_Bits/8 1328 --# and Qname_Location >=0 and Qname_Location < 16384 1329 --# and Integer(Input_Bytes) < 312 1330 --# and Start_Byte <= DNS_Types.Packet_Bytes_Range(Input_Bytes) and Start_Byte >= 4; 1331 Output_Packet.Bytes(I) := Input_Packet.Bytes(I); 1332 end loop; 1333 1334 -- we start out with no responses 1335 Output_Packet.Header.ANCount := 0; 1336 1337 -- accept Flow, 23, ReturnedCNAMERecords, "it will fill in enough"; 1338 DNS_Table_Pkg.DNS_Table.QueryCNAMERecords(DomainName => Domainname, 1339 ReturnedRecords => ReturnedCNAMERecords, HowMany => NumFound); 1340 -- end accept; 1341 if NumFound>1 then 1342 Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"more than one cname?", 0); 1343 elsif NumFound=1 then 1344 Process_Response_Cname( 1345 Start_Byte => Start_Byte, 1346 Cnames => ReturnedCNAMERecords, 1347 Domainname => Domainname, 1348 Qname_Location => Qname_Location, 1349 Output_Packet => Output_Packet, 1350 Output_Bytes => Output_Bytes); 1351 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1352 DNS_Types.Header_Bits/8); 1353 end if; 1354 Answer_Count := Output_Packet.Header.ANCount; 1355 Additional_Count := 0; 1356 --ada.text_io.put_line("numfound: " & integer'image(numfound)); 1357 if Query_Class /= DNS_Types.IN_CLASS then 1358 Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"bad query class", 0); 1359-- ada.text_io.put_line("qc: " & dns_types.Query_Class'image(Query_Class)); 1360 Create_Response_Error( 1361 Input_Bytes => Input_Bytes, 1362 Output_Packet => Output_Packet, 1363 Output_Bytes => Output_Bytes); 1364 elsif Query_Type = DNS_Types.ANY then 1365 Create_Response_A( 1366 Start_Byte => Start_Byte, 1367 Domainname => Domainname, 1368 Qname_Location => Qname_Location, 1369 Output_Packet => Output_Packet, 1370 Answer_Count => Answer_Count, 1371 Output_Bytes => Output_Bytes); 1372 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1373 DNS_Types.Header_Bits/8); 1374 Create_Response_AAAA( 1375 Start_Byte => Start_Byte, 1376 Domainname => Domainname, 1377 Qname_Location => Qname_Location, 1378 Output_Packet => Output_Packet, 1379 Answer_Count => Answer_Count, 1380 Output_Bytes => Output_Bytes); 1381 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1382 DNS_Types.Header_Bits/8); 1383--# accept Flow, 10, MX_Replies, "not needed for ANY query"; 1384--# accept Flow, 10, Qname_Locations, "not needed for ANY query"; 1385--# accept Flow, 10, NumFound, "not needed for any query"; 1386 Create_Response_MX( 1387 Start_Byte => Start_Byte, 1388 Domainname => Domainname, 1389 Num_Found => NumFound, 1390 Qname_Location => Qname_Location, 1391 Qname_Locations => Qname_Locations, 1392 Replies => MX_Replies, 1393 Output_Packet => Output_Packet, 1394 Answer_Count => Answer_Count, 1395 Output_Bytes => Output_Bytes); 1396--# end accept; 1397--# end accept; 1398--# end accept; 1399 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1400 DNS_Types.Header_Bits/8); 1401--# accept Flow, 10, NS_Replies, "not needed for ANY query"; 1402--# accept Flow, 10, Qname_Locations, "not needed for ANY query"; 1403--# accept Flow, 10, NumFound, "not needed for any query"; 1404 Create_Response_NS( 1405 Start_Byte => Start_Byte, 1406 Domainname => Domainname, 1407 Num_Found => NumFound, 1408 Qname_Location => Qname_Location, 1409 Qname_Locations => Qname_Locations, 1410 Replies => NS_Replies, 1411 Output_Packet => Output_Packet, 1412 Answer_Count => Answer_Count, 1413 Output_Bytes => Output_Bytes); 1414--# end accept; 1415--# end accept; 1416--# end accept; 1417 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1418 DNS_Types.Header_Bits/8); 1419--# accept Flow, 10, SRV_Replies, "not needed for ANY query"; 1420--# accept Flow, 10, Qname_Locations, "not needed for ANY query"; 1421--# accept Flow, 10, NumFound, "not needed for any query"; 1422 Create_Response_SRV( 1423 Start_Byte => Start_Byte, 1424 Domainname => Domainname, 1425 Num_Found => NumFound, 1426 Qname_Location => Qname_Location, 1427 Qname_Locations => Qname_Locations, 1428 Replies => SRV_Replies, 1429 Output_Packet => Output_Packet, 1430 Answer_Count => Answer_Count, 1431 Output_Bytes => Output_Bytes); 1432--# end accept; 1433--# end accept; 1434--# end accept; 1435 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1436 DNS_Types.Header_Bits/8); 1437 Create_Response_PTR( 1438 Start_Byte => Start_Byte, 1439 Domainname => Domainname, 1440 Qname_Location => Qname_Location, 1441 Output_Packet => Output_Packet, 1442 Answer_Count => Answer_Count, 1443 Output_Bytes => Output_Bytes); 1444 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1445 DNS_Types.Header_Bits/8); 1446 Create_Response_SOA( 1447 Start_Byte => Start_Byte, 1448 Domainname => Domainname, 1449 Qname_Location => Qname_Location, 1450 Output_Packet => Output_Packet, 1451 Answer_Count => Answer_Count, 1452 Output_Bytes => Output_Bytes); --DNS_Types.ANY 1453 elsif Query_Type = DNS_Types.SOA then 1454 Create_Response_SOA( 1455 Start_Byte => Start_Byte, 1456 Domainname => Domainname, 1457 Qname_Location => Qname_Location, 1458 Output_Packet => Output_Packet, 1459 Answer_Count => Answer_Count, 1460 Output_Bytes => Output_Bytes); 1461 elsif Query_Type = DNS_Types.PTR then 1462 Create_Response_PTR( 1463 Start_Byte => Start_Byte, 1464 Domainname => Domainname, 1465 Qname_Location => Qname_Location, 1466 Output_Packet => Output_Packet, 1467 Answer_Count => Answer_Count, 1468 Output_Bytes => Output_Bytes); 1469 elsif Query_Type = DNS_Types.A then 1470 Create_Response_A( 1471 Start_Byte => Start_Byte, 1472 Domainname => Domainname, 1473 Qname_Location => Qname_Location, 1474 Output_Packet => Output_Packet, 1475 Answer_Count => Answer_Count, 1476 Output_Bytes => Output_Bytes); 1477 elsif Query_Type = DNS_Types.AAAA then 1478 Create_Response_AAAA( 1479 Start_Byte => Start_Byte, 1480 Domainname => Domainname, 1481 Qname_Location => Qname_Location, 1482 Output_Packet => Output_Packet, 1483 Answer_Count => Answer_Count, 1484 Output_Bytes => Output_Bytes); 1485 elsif Query_Type = DNS_Types.DNSKEY then --BSF 24 Aug 2012 1486 Create_Response_DNSKEY( 1487 Start_Byte => Start_Byte, 1488 Domainname => Domainname, 1489 Qname_Location => Qname_Location, 1490 Output_Packet => Output_Packet, 1491 Answer_Count => Answer_Count, 1492 Output_Bytes => Output_Bytes); 1493 elsif Query_Type = DNS_Types.NSEC then --BSF 2 Oct 2012 1494 Create_Response_NSEC( 1495 Start_Byte => Start_Byte, 1496 Domainname => Domainname, 1497 Qname_Location => Qname_Location, 1498 Output_Packet => Output_Packet, 1499 Answer_Count => Answer_Count, 1500 Output_Bytes => Output_Bytes); 1501 elsif Query_Type = DNS_Types.RRSIG then --BSF 11 Sep 2012 1502 Create_Response_RRSIG( 1503 Start_Byte => Start_Byte, 1504 Domainname => Domainname, 1505 Qname_Location => Qname_Location, 1506 Output_Packet => Output_Packet, 1507 Answer_Count => Answer_Count, 1508 Output_Bytes => Output_Bytes); 1509 elsif Query_Type = DNS_Types.MX then 1510 Create_Response_MX( 1511 Start_Byte => Start_Byte, 1512 Domainname => Domainname, 1513 Num_Found => NumFound, 1514 Qname_Location => Qname_Location, 1515 Qname_Locations => Qname_Locations, 1516 Replies => MX_Replies, 1517 Output_Packet => Output_Packet, 1518 Answer_Count => Answer_Count, 1519 Output_Bytes => Output_Bytes); 1520 Counter := 1; 1521 Additional_Count := 0; 1522 while Counter <= NumFound and Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short( 1523 2*Rr_Type.MaxNumRecords) loop 1524 --# assert Counter >= 1 and Counter<=NumFound and 1525 --# Answer_Count >=0 and Answer_Count <= 65535 and 1526 --# Additional_Count >= 0 and 1527 --# (for all Z in RR_Type.ReturnedRecordsIndexType => 1528 --# (Qname_Locations(Z) >= 0 and Qname_Locations(Z) < 16384)) and 1529 --# Qname_Location >=0 and Qname_Location <= 16383 and 1530 --# Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short( 1531 --# 2*Rr_Type.MaxNumRecords) and 1532 --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and 1533 --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and 1534 --# Integer(Output_Bytes) <= DNS_Types.Packet_Size; 1535 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1536 DNS_Types.Header_Bits/8); 1537 Create_Response_A( 1538 Start_Byte => Start_Byte, 1539 Domainname => MX_Replies(Counter).mailExchanger, 1540 Qname_Location => Qname_Locations(Counter), 1541 Output_Packet => Output_Packet, 1542 Answer_Count => Additional_Count, 1543 Output_Bytes => Output_Bytes); 1544 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1545 DNS_Types.Header_Bits/8); 1546 Create_Response_AAAA( 1547 Start_Byte => Start_Byte, 1548 Domainname => MX_Replies(Counter).mailExchanger, 1549 Qname_Location => Qname_Locations(Counter), 1550 Output_Packet => Output_Packet, 1551 Answer_Count => Additional_Count, 1552 Output_Bytes => Output_Bytes); 1553 Counter := Counter + 1; 1554 end loop; 1555 elsif Query_Type = DNS_Types.SRV then 1556 Create_Response_SRV( 1557 Start_Byte => Start_Byte, 1558 Domainname => Domainname, 1559 Num_Found => NumFound, 1560 Qname_Location => Qname_Location, 1561 Qname_Locations => Qname_Locations, 1562 Replies => SRV_Replies, 1563 Output_Packet => Output_Packet, 1564 Answer_Count => Answer_Count, 1565 Output_Bytes => Output_Bytes); 1566 Counter := 1; 1567 Additional_Count := 0; 1568 while Counter <= NumFound and Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short( 1569 2*Rr_Type.MaxNumRecords) loop 1570 --# assert Counter >= 1 and Counter<=NumFound and 1571 --# Answer_Count >=0 and Answer_Count <= 65535 and 1572 --# Additional_Count >= 0 and 1573 --# (for all Z in RR_Type.ReturnedRecordsIndexType => 1574 --# (Qname_Locations(Z) >= 0 and Qname_Locations(Z) < 16384)) and 1575 --# Qname_Location >=0 and Qname_Location <= 16383 and 1576 --# Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short( 1577 --# 2*Rr_Type.MaxNumRecords) and 1578 --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and 1579 --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and 1580 --# Integer(Output_Bytes) <= DNS_Types.Packet_Size; 1581 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1582 DNS_Types.Header_Bits/8); 1583 Create_Response_A( 1584 Start_Byte => Start_Byte, 1585 Domainname => SRV_Replies(Counter).servername, 1586 Qname_Location => Qname_Locations(Counter), 1587 Output_Packet => Output_Packet, 1588 Answer_Count => Additional_Count, 1589 Output_Bytes => Output_Bytes); 1590 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1591 DNS_Types.Header_Bits/8); 1592 Create_Response_AAAA( 1593 Start_Byte => Start_Byte, 1594 Domainname => SRV_Replies(Counter).servername, 1595 Qname_Location => Qname_Locations(Counter), 1596 Output_Packet => Output_Packet, 1597 Answer_Count => Additional_Count, 1598 Output_Bytes => Output_Bytes); 1599 Counter := Counter + 1; 1600 end loop; 1601 elsif Query_Type = DNS_Types.NS then 1602 Create_Response_NS( 1603 Start_Byte => Start_Byte, 1604 Domainname => Domainname, 1605 Num_Found => NumFound, 1606 Qname_Location => Qname_Location, 1607 Qname_Locations => Qname_Locations, 1608 Replies => NS_Replies, 1609 Output_Packet => Output_Packet, 1610 Answer_Count => Answer_Count, 1611 Output_Bytes => Output_Bytes); 1612 Counter := 1; 1613 Additional_Count := 0; 1614 while Counter <= NumFound and Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short( 1615 2*Rr_Type.MaxNumRecords) loop 1616 --# assert Counter >= 1 and Counter<=NumFound and 1617 --# (for all Z in RR_Type.ReturnedRecordsIndexType => 1618 --# (Qname_Locations(Z) >= 0 and Qname_Locations(Z) < 16384)) and 1619 --# Qname_Location >=0 and Qname_Location <= 16383 and 1620 --# Answer_Count >=0 and Answer_Count <= 65535 and 1621 --# Additional_Count >= 0 and 1622 --# Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short( 1623 --# 2*Rr_Type.MaxNumRecords) and 1624 --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and 1625 --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and 1626 --# Integer(Output_Bytes) <= DNS_Types.Packet_Size; 1627 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1628 DNS_Types.Header_Bits/8); 1629 Create_Response_A( 1630 Start_Byte => Start_Byte, 1631 Domainname => NS_Replies(Counter).nameserver, 1632 Qname_Location => Qname_Locations(Counter), 1633 Output_Packet => Output_Packet, 1634 Answer_Count => Additional_Count, 1635 Output_Bytes => Output_Bytes); 1636 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1637 DNS_Types.Header_Bits/8); 1638 Create_Response_AAAA( 1639 Start_Byte => Start_Byte, 1640 Domainname => NS_Replies(Counter).nameserver, 1641 Qname_Location => Qname_Locations(Counter), 1642 Output_Packet => Output_Packet, 1643 Answer_Count => Additional_Count, 1644 Output_Bytes => Output_Bytes); 1645 Counter := Counter + 1; 1646 end loop; 1647 else 1648 Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"bad query type", 0); 1649-- ada.text_io.put_line("qc: " & dns_types.Query_Type'image(Query_Type)); 1650 Create_Response_Error( 1651 Input_Bytes => Input_Bytes, 1652 Output_Packet => Output_Packet, 1653 Output_Bytes => Output_Bytes); 1654 end if; 1655 1656 -- this assert helps with the VCG Heap overflow 1657 --# assert 1658 --# Answer_Count >=0 and Answer_Count <= 65535 and 1659 --# Qname_Location >=0 and Qname_Location < 16384 and 1660 --# Additional_Count >= 0 and 1661 --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and 1662 --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and 1663 --# Integer(Output_Bytes) <= DNS_Types.Packet_Size; 1664 1665 DNSSEC := False; 1666 Max_Transmit := DNS_Types.UDP_Max_Size; 1667 -- Handle EDNS additional OPT record here! 1668 if Input_Packet.Header.QDCount = 1 and 1669 Input_Packet.Header.ARCount = 1 and 1670 Additional_Count < DNS_Types.Unsigned_Short'Last then 1671 Start_Byte := DNS_Types.Packet_Bytes_Range(Integer(Output_Bytes) - 1672 DNS_Types.Header_Bits/8); 1673 Create_Response_EDNS( 1674 Input_Packet => Input_Packet, 1675 Input_Bytes => Input_Bytes, 1676 Query_End_Byte => Query_End_Byte, 1677 Start_Byte => Start_Byte, 1678 Output_Packet => Output_Packet, 1679 Output_Bytes => Output_Bytes, 1680 Additional_Count => Additional_Count, 1681 DNSSEC => DNSSEC, 1682 Max_Transmit => Max_Transmit); 1683 elsif Input_Packet.Header.QDCount /= 1 then 1684 Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"query count > 1", 0); 1685 elsif Input_Packet.Header.ARCount > 1 then 1686 Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"ar count > 1", 0); 1687 end if; 1688 1689 -- this assert helps with the VCG Heap overflow 1690 --# assert 1691 --# Answer_Count >=0 and Answer_Count <= 65535 and 1692 --# Qname_Location >=0 and Qname_Location < 16384 and 1693 --# Additional_Count >= 0 and 1694 --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and 1695 --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and 1696 --# Integer(Max_Transmit) <= DNS_Types.Packet_Size and Max_Transmit >= DNS_Types.UDP_Max_Size and 1697 --# Integer(Output_Bytes) <= DNS_Types.Packet_Size; 1698 1699 1700 if DNSSEC and Answer_Count > 0 then 1701 Output_Bytes := (Output_Bytes-1)+1; 1702 end if; 1703 1704 Output_Packet.Header.ANCount := Answer_Count; 1705 Output_Packet.Header.ARCount := Additional_Count; 1706 if Answer_Count > 0 then 1707 -- our answer is authoritative 1708 Output_Packet.Header.AA := True; 1709 Output_Packet.Header.RCODE := DNS_Types.No_Error; 1710 elsif Output_Packet.Header.AA = False then 1711 Create_NXDOMAIN_Response( 1712 Start_Byte => DNS_Types.Packet_Bytes_Range(Input_Bytes) - 1713 DNS_Types.Packet_Bytes_Range(DNS_Types.Header_Bits/8), 1714 Domainname => Domainname, 1715 Qname_Location => Qname_Location, 1716 Output_Packet => Output_Packet, 1717 Output_Bytes => Output_Bytes); 1718 end if; 1719 -- accept Flow, 602, Output_Packet, ReturnedCNAMERecords, "initialization is unneeded"; 1720 -- accept Flow, 602, Output_Bytes, ReturnedCNAMERecords, "initialization is unneeded"; 1721 end Create_Response; 1722 1723 1724 procedure Process_Request_Tcp( 1725 Reply_Socket : in DNS_Network.DNS_Socket) 1726 is 1727 Input_Packet : DNS_Types.DNS_Tcp_Packet; 1728 Input_Bytes : DNS_Types.Packet_Length_Range; 1729 Output_Packet : DNS_Types.DNS_Tcp_Packet; 1730 Output_Bytes : DNS_Types.Packet_Length_Range; 1731 Max_Transmit : DNS_Types.Packet_Length_Range; 1732 Failure : Boolean; 1733 begin 1734 --Output_Packet.Rest.Bytes := DNS_Types.Bytes_Array_Type'(others => 0); 1735 1736 DNS_Network_Receive.Receive_DNS_Packet_Tcp( 1737 Packet => Input_Packet, 1738 Number_Bytes => Input_Bytes, 1739 Socket => Reply_Socket, 1740 Failure => Failure); 1741-- SPARK_IO_05.Put_Line(SPARK_IO_05.Standard_Output,"Input ID", 0); 1742-- SPARK_IO_05.Put_Integer(SPARK_IO_05.Standard_Output, 1743-- Integer(Input_Packet.Rest.Header.MessageID), 0, 16); 1744-- SPARK_IO_05.New_Line(SPARK_IO_05.Standard_Output,1); 1745 if Failure then 1746 --Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"Receive failed", 0); 1747 null; 1748 else 1749 --Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"got packet", 0); 1750 --# accept Flow, 23, Output_Packet.Rest, "init not needed"; 1751 --# accept Flow, 10, Max_Transmit, "only needed for UDP"; 1752 Create_Response( 1753 Input_Packet => Input_Packet.Rest, 1754 Input_Bytes => Input_Bytes, 1755 Output_Packet => Output_Packet.Rest, 1756 Output_Bytes => Output_Bytes, 1757 Max_Transmit => Max_Transmit); 1758 --# end accept; 1759 --# end accept; 1760 --Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"Reply created", 0); 1761 --# accept Flow, 22, 1762 --# "allow use of static expression for portability across platforms"; 1763 if System.Default_Bit_Order=System.Low_Order_First then 1764 --# end accept; 1765 Output_Packet.Length := DNS_Types.Byte_Swap_US(DNS_Types.Unsigned_Short(Output_Bytes)); 1766 else 1767 Output_Packet.Length := DNS_Types.Unsigned_Short(Output_Bytes); 1768 end if; 1769-- SPARK_IO_05.Put_Line(SPARK_IO_05.Standard_Output,"Output ID", 0); 1770-- SPARK_IO_05.Put_Integer(SPARK_IO_05.Standard_Output, 1771-- Integer(Output_Packet.Rest.Header.MessageID), 0, 16); 1772-- SPARK_IO_05.New_Line(SPARK_IO_05.Standard_Output,1); 1773-- Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"sending", 0); 1774 1775 DNS_Network.Send_DNS_Packet_Tcp( 1776 Packet => Output_Packet, 1777 Number_Bytes => Output_Bytes, 1778 Socket => Reply_Socket, 1779 Failure => Failure); 1780 if Failure then 1781 Protected_SPARK_IO_05.SPARK_IO_PO.Put_Integer(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output, 1782 Integer(Output_Packet.Rest.Header.MessageID), 0, 16); 1783 Protected_SPARK_IO_05.SPARK_IO_PO.Put_Line(Protected_SPARK_IO_05.SPARK_IO_PO.Standard_Output,"Respond failed", 0); 1784 end if; 1785 end if; 1786 --# accept Flow, 602, DNS_Network.Network, Output_Packet.Rest, "initialization is unneeded"; 1787 --# accept Flow, 602, Protected_SPARK_IO_05.SPARK_IO_PO, Output_Packet.Rest, "initialization is unneeded"; 1788 --# accept Flow, 33, Max_Transmit, "Max_Transmit only for UDP"; 1789 end Process_Request_Tcp; 1790 1791 1792 1793end Process_Dns_Request; 1794 1795