269 lines
11 KiB
Plaintext
269 lines
11 KiB
Plaintext
*******************************************************
|
|
Listing of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*******************************************************
|
|
|
|
|
|
Line
|
|
----------------------------------------------------------------
|
|
-- IRONSIDES - DNS SERVER
|
|
--
|
|
-- By: Martin C. Carlisle and Barry S. Fagin
|
|
-- Department of Computer Science
|
|
-- United States Air Force Academy
|
|
--
|
|
-- This is free software; you can redistribute it and/or
|
|
-- modify without restriction. We do ask that you please keep
|
|
-- the original author information, and clearly indicate if the
|
|
-- software has been modified.
|
|
--
|
|
-- This software is distributed in the hope that it will be useful,
|
|
-- but WITHOUT ANY WARRANTY; without even the implied warranty
|
|
-- of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
|
|
----------------------------------------------------------------
|
|
|
|
with Ada.Streams;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
with System;
|
|
use type System.Bit_Order;
|
|
with Socket_Timeout;
|
|
^
|
|
--- Warning :391: If the identifier Socket_Timeout represents a
|
|
package which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with Ada.Unchecked_Conversion;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
--with Ada.Text_Io;
|
|
--use ada.text_io;
|
|
package body DNS_Network is
|
|
--# hide DNS_Network;
|
|
Server : Gnat.Sockets.Socket_Type;
|
|
Address : Gnat.Sockets.Sock_Addr_Type;
|
|
UDP_Socket : Gnat.Sockets.Socket_Type;
|
|
UDP_Address : Gnat.Sockets.Sock_Addr_Type;
|
|
|
|
procedure Initialize_UDP is
|
|
begin
|
|
|
|
-- create the socket which will listen for the UDP DNS query
|
|
Gnat.Sockets.Create_Socket(
|
|
Socket => UDP_Socket,
|
|
Family => Gnat.Sockets.Family_Inet,
|
|
Mode => Gnat.Sockets.Socket_Datagram);
|
|
|
|
-- Allow socket to be bound to address already in use
|
|
Gnat.Sockets.Set_Socket_Option(UDP_Socket,
|
|
Gnat.Sockets.Socket_Level, (Gnat.Sockets.Reuse_Address, True));
|
|
|
|
-- bind the socket to the first IP address on localhost, port 53
|
|
--Address.Addr := Gnat.Sockets.Addresses(
|
|
-- Gnat.Sockets.Get_Host_By_Name(Gnat.Sockets.Host_Name), 1);
|
|
-- bind to any IP address available
|
|
UDP_Address.Addr := Gnat.Sockets.ANY_INET_ADDR;
|
|
UDP_Address.Port := 53;
|
|
Gnat.Sockets.Bind_Socket(UDP_Socket,UDP_Address);
|
|
|
|
|
|
end Initialize_UDP;
|
|
|
|
procedure Initialize_TCP is
|
|
begin
|
|
|
|
|
|
-- create the socket which will listen for the TCP query
|
|
Gnat.Sockets.Create_Socket(
|
|
Socket => Server,
|
|
Family => Gnat.Sockets.Family_Inet,
|
|
Mode => Gnat.Sockets.Socket_Stream);
|
|
|
|
-- -- Allow socket to be bound to address already in use
|
|
--Gnat.Sockets.Set_Socket_Option(Server,
|
|
-- Gnat.Sockets.Socket_Level, (Gnat.Sockets.Reuse_Address, True));
|
|
Address.Addr := Gnat.Sockets.ANY_INET_ADDR;
|
|
|
|
-- bind the socket to the first IP address on localhost, port 53
|
|
-- below doesn't work on Linux, as it doesn't resolve host_name correctly
|
|
-- Address.Addr := Gnat.Sockets.Addresses(
|
|
-- Gnat.Sockets.Get_Host_By_Name(Gnat.Sockets.Host_Name), 1);
|
|
Address.Port := 53;
|
|
Gnat.Sockets.Bind_Socket(Server,Address);
|
|
Gnat.Sockets.Listen_Socket(Socket => Server);
|
|
end Initialize_TCP;
|
|
|
|
procedure Get_Connection_TCP(
|
|
Socket : out DNS_Socket)
|
|
is
|
|
function Convert is new Ada.Unchecked_Conversion(DNS_Socket,
|
|
Socket_Timeout.Socket_Type);
|
|
begin
|
|
Gnat.Sockets.Accept_Socket(Server => Server,
|
|
Socket => Gnat.Sockets.Socket_Type(Socket),
|
|
Address => Address);
|
|
Socket_Timeout.Set_Socket_Timeout(
|
|
Socket => Convert(Socket),
|
|
Milliseconds => Socket_Timeout_Milliseconds);
|
|
end Get_Connection_TCP;
|
|
|
|
procedure Receive_DNS_Packet_TCP
|
|
(Packet : out DNS_Types.DNS_Tcp_Packet;
|
|
Number_Bytes : out DNS_Types.Packet_Length_Range;
|
|
Socket : in DNS_Socket;
|
|
Failure : out Boolean)
|
|
is
|
|
USE TYPE Dns_Types.Packet_Length_Range;
|
|
use type ada.streams.Stream_Element_Offset;
|
|
Last_Value : Ada.Streams.Stream_Element_Offset;
|
|
Item : Ada.Streams.Stream_Element_Array (1 .. DNS_Types.DNS_Packet'Size/8);
|
|
for Item'Address use Packet'Address;
|
|
begin
|
|
Gnat.Sockets.Receive_Socket(
|
|
Socket => Gnat.Sockets.Socket_Type(Socket),
|
|
Item => Item,
|
|
Last => Last_Value);
|
|
Number_Bytes := DNS_Types.Packet_Length_Range(Last_Value)-2;
|
|
if System.Default_Bit_Order=System.Low_Order_First then
|
|
DNS_Types.Byte_Swap(Packet.Rest.Header);
|
|
end if;
|
|
Failure := (Number_Bytes < DNS_Types.Packet_Length_Range(1+DNS_Types.Header_Bits/8))
|
|
OR (Number_Bytes > MAX_QUERY_SIZE);
|
|
exception when others =>
|
|
--ada.text_io.put_line("failure!");
|
|
Failure := True;
|
|
end Receive_DNS_Packet_Tcp;
|
|
|
|
-------------------------
|
|
-- Send_DNS_Packet_Tcp --
|
|
-------------------------
|
|
|
|
procedure Send_DNS_Packet_Tcp
|
|
(Packet : in out DNS_Types.DNS_Tcp_Packet;
|
|
Number_Bytes : in DNS_Types.Packet_Length_Range;
|
|
Socket : in DNS_Socket;
|
|
Failure : out Boolean)
|
|
is
|
|
USE TYPE Dns_Types.Packet_Length_Range;
|
|
use type ada.streams.Stream_Element_Offset;
|
|
Response_Stream : Ada.Streams.Stream_Element_Array (1 .. DNS_Types.DNS_Packet'Size/8);
|
|
for Response_Stream'Address use Packet'Address;
|
|
Result_Last : Ada.Streams.Stream_Element_Offset;
|
|
begin
|
|
if System.Default_Bit_Order=System.Low_Order_First then
|
|
DNS_Types.Byte_Swap(Packet.Rest.Header);
|
|
end if;
|
|
|
|
Gnat.Sockets.Send_Socket(
|
|
Socket => Gnat.Sockets.Socket_Type(Socket),
|
|
Item => Response_Stream (1 .. Ada.Streams.Stream_Element_Offset(Number_Bytes+2)),
|
|
Last => Result_Last);
|
|
-- put_line("Num bytes sent" & Ada.Streams.Stream_Element_Offset'image(result_last));
|
|
if Result_Last /= Ada.Streams.Stream_Element_Offset(Number_Bytes+2) then
|
|
Failure := True;
|
|
else
|
|
Failure := False;
|
|
end if;
|
|
Gnat.Sockets.Close_Socket(Gnat.Sockets.Socket_Type(Socket));
|
|
|
|
exception when others =>
|
|
Failure := True;
|
|
end Send_DNS_Packet_Tcp;
|
|
|
|
procedure Discard_Socket(Socket : in DNS_Socket) is
|
|
begin
|
|
Gnat.Sockets.Close_Socket(Gnat.Sockets.Socket_Type(Socket));
|
|
exception when others =>
|
|
null;
|
|
end Discard_Socket;
|
|
|
|
--# global in out Network;
|
|
--# derives Network from *;
|
|
------------------------
|
|
-- Receive_DNS_Packet --
|
|
------------------------
|
|
|
|
procedure Receive_DNS_Packet
|
|
(Packet : out DNS_Types.DNS_Packet;
|
|
Number_Bytes : out DNS_Types.Packet_Length_Range;
|
|
Reply_Address : out Network_Address_and_Port;
|
|
Failure : out Boolean)
|
|
is
|
|
USE TYPE Dns_Types.Packet_Length_Range;
|
|
use type ada.streams.Stream_Element_Offset;
|
|
Last_Value : Ada.Streams.Stream_Element_Offset;
|
|
Item : Ada.Streams.Stream_Element_Array (1 .. DNS_Types.DNS_Packet'Size/8);
|
|
for Item'Address use Packet'Address;
|
|
begin
|
|
Gnat.Sockets.Receive_Socket(
|
|
Socket => UDP_Socket,
|
|
Item => Item,
|
|
Last => Last_Value,
|
|
From => Gnat.Sockets.Sock_Addr_Type(Reply_Address));
|
|
Number_Bytes := DNS_Types.Packet_Length_Range(Last_Value);
|
|
-- put_line("Num bytes" & dns_types.packet_length_range'image(number_bytes));
|
|
if System.Default_Bit_Order=System.Low_Order_First then
|
|
DNS_Types.Byte_Swap(Packet.Header);
|
|
end if;
|
|
--Gnat.Sockets.Close_Socket(Socket);
|
|
Failure := False;
|
|
exception when others =>
|
|
Failure := True;
|
|
end Receive_DNS_Packet;
|
|
|
|
---------------------
|
|
-- Send_DNS_Packet --
|
|
---------------------
|
|
|
|
procedure Send_DNS_Packet
|
|
(Packet : in out DNS_Types.DNS_Packet;
|
|
Number_Bytes : in DNS_Types.Packet_Length_Range;
|
|
To_Address : in Network_Address_and_Port;
|
|
Failure : out Boolean)
|
|
is
|
|
USE TYPE Dns_Types.Packet_Length_Range;
|
|
use type ada.streams.Stream_Element_Offset;
|
|
Response_Stream : Ada.Streams.Stream_Element_Array (1 .. DNS_Types.DNS_Packet'Size/8);
|
|
for Response_Stream'Address use Packet'Address;
|
|
Result_Last : Ada.Streams.Stream_Element_Offset;
|
|
begin
|
|
if System.Default_Bit_Order=System.Low_Order_First then
|
|
DNS_Types.Byte_Swap(Packet.Header);
|
|
end if;
|
|
-- connect back to client
|
|
-- Gnat.Sockets.Connect_Socket(
|
|
-- Socket => Reply_UDP_Socket,
|
|
-- Server => Gnat.Sockets.Sock_Addr_Type(To_Address));
|
|
|
|
Gnat.Sockets.Send_Socket(
|
|
Socket => UDP_Socket,
|
|
Item => Response_Stream (1 .. Ada.Streams.Stream_Element_Offset(Number_Bytes)),
|
|
Last => Result_Last,
|
|
To => Gnat.Sockets.Sock_Addr_Type(To_Address));
|
|
-- put_line("Num bytes" & Ada.Streams.Stream_Element_Offset'image(result_last));
|
|
|
|
if Result_Last /= Ada.Streams.Stream_Element_Offset(Number_Bytes) then
|
|
Failure := True;
|
|
else
|
|
Failure := False;
|
|
end if;
|
|
|
|
exception when others =>
|
|
Failure := True;
|
|
end Send_DNS_Packet;
|
|
|
|
end DNS_Network;
|
|
|
|
--- Warning : 10: The body of package DNS_Network is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
|
|
|
|
--End of file--------------------------------------------------
|