diff --git a/wrapper/Ada/spark_sockets.adb b/wrapper/Ada/spark_sockets.adb new file mode 100644 index 000000000..e315f230e --- /dev/null +++ b/wrapper/Ada/spark_sockets.adb @@ -0,0 +1,138 @@ +-- spark_sockets.adb +-- +-- Copyright (C) 2006-2023 wolfSSL Inc. +-- +-- This file is part of wolfSSL. +-- +-- wolfSSL is free software; you can redistribute it and/or modify +-- it under the terms of the GNU General Public License as published by +-- the Free Software Foundation; either version 2 of the License, or +-- (at your option) any later version. +-- +-- wolfSSL 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. See the +-- GNU General Public License for more details. +-- +-- You should have received a copy of the GNU General Public License +-- along with this program; if not, write to the Free Software +-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA +-- + +with Interfaces.C; + +package body SPARK_Sockets is + + function Inet_Addr (Image : String) return Optional_Inet_Addr is + A : Inet_Addr_Type; + begin + A := GNAT.Sockets.Inet_Addr (Image); + return (Exists => True, Addr => A); + exception + when others => + return (Exists => False); + end Inet_Addr; + + procedure Create_Socket (Socket : in out Optional_Socket) is + S : Socket_Type; + begin + GNAT.Sockets.Create_Socket (S); + Socket := (Exists => True, Socket => S); + exception + when others => + Socket := (Exists => False); + end Create_Socket; + + function Connect_Socket (Socket : Socket_Type; + Server : Sock_Addr_Type) + return Subprogram_Result is + begin + GNAT.Sockets.Connect_Socket (Socket, Server); + return Success; + exception + when others => + return Failure; + end Connect_Socket; + + function To_C (Socket : Socket_Type) return Integer is + begin + -- The call to GNAT.Sockets.To_C can never raise an exception. + return GNAT.Sockets.To_C (Socket); + end To_C; + + procedure Close_Socket (Socket : in out Optional_Socket) is + begin + GNAT.Sockets.Close_Socket (Socket.Socket); + Socket := (Exists => False); + end Close_Socket; + + function Set_Socket_Option (Socket : Socket_Type; + Level : Level_Type; + Option : Option_Type) + return Subprogram_Result is + begin + GNAT.Sockets.Set_Socket_Option (Socket, Level, Option); + return Success; + exception + when others => + return Failure; + end Set_Socket_Option; + + function Bind_Socket (Socket : Socket_Type; + Address : Sock_Addr_Type) + return Subprogram_Result is + begin + GNAT.Sockets.Bind_Socket (Socket, Address); + return Success; + exception + when others => + return Failure; + end Bind_Socket; + + function Listen_Socket (Socket : Socket_Type; + Length : Natural) return Subprogram_Result is + begin + GNAT.Sockets.Listen_Socket (Socket, Length); + return Success; + exception + when others => + return Failure; + end Listen_Socket; + + procedure Accept_Socket (Server : Socket_Type; + Socket : out Optional_Socket; + Address : out Sock_Addr_Type; + Result : out Subprogram_Result) is + C : Socket_Type; + begin + GNAT.Sockets.Accept_Socket (Server, C, Address); + Socket := (Exists => True, Socket => C); + Result := Success; + exception + when others => + Socket := (Exists => False); + Address := (Family => GNAT.Sockets.Family_Unspec); + Result := Failure; + end Accept_Socket; + + procedure To_C (Item : String; + Target : out Byte_Array; + Count : out Byte_Index) is + begin + Interfaces.C.To_C (Item => Item, + Target => Target, + Count => Count, + Append_Nul => False); + end To_C; + + procedure To_Ada (Item : Byte_Array; + Target : out String; + Count : out Natural) is + begin + Interfaces.C.To_Ada (Item => Item, + Target => Target, + Count => Count, + Trim_Nul => False); + end To_Ada; + +end SPARK_Sockets; diff --git a/wrapper/Ada/spark_sockets.ads b/wrapper/Ada/spark_sockets.ads new file mode 100644 index 000000000..ee9864c6f --- /dev/null +++ b/wrapper/Ada/spark_sockets.ads @@ -0,0 +1,137 @@ +-- spark_sockets.ads +-- +-- Copyright (C) 2006-2023 wolfSSL Inc. +-- +-- This file is part of wolfSSL. +-- +-- wolfSSL is free software; you can redistribute it and/or modify +-- it under the terms of the GNU General Public License as published by +-- the Free Software Foundation; either version 2 of the License, or +-- (at your option) any later version. +-- +-- wolfSSL 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. See the +-- GNU General Public License for more details. +-- +-- You should have received a copy of the GNU General Public License +-- along with this program; if not, write to the Free Software +-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA +-- + +-- GNAT Library packages. +with GNAT.Sockets; + +-- The WolfSSL package. +with WolfSSL; + +-- This is a wrapper package around the GNAT.Sockets package. +-- GNAT.Sockets raises exceptions to signal errors but exceptions +-- are not supported by SPARK. This package converts raised exceptions +-- into returned enumeration values by functions indicating success +-- or failure. +-- +-- The intended use of this package is to demonstrate the usage +-- of the WolfSSL Ada binding in Ada/SPARK code. +package SPARK_Sockets with SPARK_Mode is + + subtype Byte_Array is WolfSSL.Byte_Array; + subtype Byte_Index is WolfSSL.Byte_Index; use type Byte_Index; + + subtype Port_Type is GNAT.Sockets.Port_Type; + + subtype Level_Type is GNAT.Sockets.Level_Type; + + subtype Socket_Type is GNAT.Sockets.Socket_Type; + subtype Option_Name is GNAT.Sockets.Option_Name; + subtype Option_Type is GNAT.Sockets.Option_Type; + subtype Family_Type is GNAT.Sockets.Family_Type; + + subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + + Socket_Error : exception renames GNAT.Sockets.Socket_Error; + + Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + + Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + + Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + use type GNAT.Sockets.Family_Type; + + Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + + subtype Subprogram_Result is WolfSSL.Subprogram_Result; + use type Subprogram_Result; + + Success : Subprogram_Result renames WolfSSL.Success; + Failure : Subprogram_Result renames WolfSSL.Failure; + + type Optional_Inet_Addr (Exists : Boolean := False) is record + case Exists is + when True => Addr : Inet_Addr_Type; + when False => null; + end case; + end record; + + function Inet_Addr (Image : String) return Optional_Inet_Addr; + + type Optional_Socket (Exists : Boolean := False) is record + case Exists is + when True => Socket : Socket_Type; + when False => null; + end case; + end record; + + procedure Create_Socket (Socket : in out Optional_Socket) with + Pre => not Socket.Exists; + + function Connect_Socket (Socket : Socket_Type; + Server : Sock_Addr_Type) + return Subprogram_Result; + + function To_C (Socket : Socket_Type) return Integer with Inline; + + -- Close a socket and more specifically a non-connected socket. + procedure Close_Socket (Socket : in out Optional_Socket) with + Pre => Socket.Exists, + Post => not Socket.Exists; + + function Set_Socket_Option (Socket : Socket_Type; + Level : Level_Type; + Option : Option_Type) + return Subprogram_Result; + -- Manipulate socket options. + + function Bind_Socket (Socket : Socket_Type; + Address : Sock_Addr_Type) + return Subprogram_Result; + + function Listen_Socket (Socket : Socket_Type; + Length : Natural) return Subprogram_Result; + -- To accept connections, a socket is first created with + -- Create_Socket, a willingness to accept incoming connections and + -- a queue Length for incoming connections are specified. + -- The queue length of 15 is an example value that should be + -- appropriate in usual cases. It can be adjusted according to each + -- application's particular requirements. + + procedure Accept_Socket (Server : Socket_Type; + Socket : out Optional_Socket; + Address : out Sock_Addr_Type; + Result : out Subprogram_Result) with + Post => (if Result = Success then Socket.Exists else not Socket.Exists); + + procedure To_C (Item : String; + Target : out Byte_Array; + Count : out Byte_Index) with + Pre => Item'Length <= Target'Length, + Post => Count <= Target'Last; + + procedure To_Ada (Item : Byte_Array; + Target : out String; + Count : out Natural) with + Pre => Item'Length <= Target'Length, + Post => Count <= Target'Last; + +end SPARK_Sockets; diff --git a/wrapper/Ada/spark_terminal.adb b/wrapper/Ada/spark_terminal.adb new file mode 100644 index 000000000..14bfb4b1f --- /dev/null +++ b/wrapper/Ada/spark_terminal.adb @@ -0,0 +1,18 @@ +package body SPARK_Terminal is + + procedure Set_Exit_Status (Status : Exit_Status) is + begin + Ada.Command_Line.Set_Exit_Status (Status); + end Set_Exit_Status; + + function Argument_Count return Natural is + begin + return Ada.Command_Line.Argument_Count; + end Argument_Count; + + function Argument (Number : Positive) return String is + begin + return Ada.Command_Line.Argument (Number); + end Argument; + +end SPARK_Terminal; diff --git a/wrapper/Ada/spark_terminal.ads b/wrapper/Ada/spark_terminal.ads new file mode 100644 index 000000000..1c516ca7b --- /dev/null +++ b/wrapper/Ada/spark_terminal.ads @@ -0,0 +1,43 @@ +-- spark_sockets.ads +-- +-- Copyright (C) 2006-2023 wolfSSL Inc. +-- +-- This file is part of wolfSSL. +-- +-- wolfSSL is free software; you can redistribute it and/or modify +-- it under the terms of the GNU General Public License as published by +-- the Free Software Foundation; either version 2 of the License, or +-- (at your option) any later version. +-- +-- wolfSSL 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. See the +-- GNU General Public License for more details. +-- +-- You should have received a copy of the GNU General Public License +-- along with this program; if not, write to the Free Software +-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA +-- + +with Ada.Command_Line; + +-- SPARK wrapper package around Ada.Command_Line and Interfaces.C +-- packages because these packages lack contracts in their specification +-- files that SPARK can use to verify the context in which +-- subprograms can safely be called. +package SPARK_Terminal with SPARK_Mode is + + subtype Exit_Status is Ada.Command_Line.Exit_Status; + + Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; + Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; + + procedure Set_Exit_Status (Status : Exit_Status) with + Global => null; + + function Argument_Count return Natural; + + function Argument (Number : Positive) return String with + Pre => Number <= Argument_Count; + +end SPARK_Terminal; diff --git a/wrapper/Ada/tls_client.adb b/wrapper/Ada/tls_client.adb index 97d43babe..a00303353 100644 --- a/wrapper/Ada/tls_client.adb +++ b/wrapper/Ada/tls_client.adb @@ -21,18 +21,13 @@ -- Ada Standard Library packages. with Ada.Characters.Handling; -with Ada.Command_Line; with Ada.Strings.Bounded; -with Ada.Text_IO.Bounded_IO; +with Ada.Text_IO; with Interfaces.C; --- GNAT Library packages. -with GNAT.Sockets; +with SPARK_Terminal; --- The WolfSSL package. -with WolfSSL; - -package body Tls_Client is +package body Tls_Client with SPARK_Mode is use type WolfSSL.Mode_Type; use type WolfSSL.Byte_Index; @@ -42,13 +37,8 @@ package body Tls_Client is subtype Byte_Type is WolfSSL.Byte_Type; - package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200); - use all type Messages.Bounded_String; - package Integer_IO is new Ada.Text_IO.Integer_IO (Integer); - package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages); - procedure Put (Text : String) is begin Ada.Text_IO.Put (Text); @@ -69,42 +59,39 @@ package body Tls_Client is Ada.Text_IO.New_Line; end New_Line; - procedure Put_Line (Text : Messages.Bounded_String) is + subtype Exit_Status is SPARK_Terminal.Exit_Status; + + Exit_Status_Success : Exit_Status renames SPARK_Terminal.Exit_Status_Success; + Exit_Status_Failure : Exit_Status renames SPARK_Terminal.Exit_Status_Failure; + + procedure Set (Status : Exit_Status) with Global => null is begin - Messages_IO.Put_Line (Text); - end Put_Line; - - subtype Exit_Status is Ada.Command_Line.Exit_Status; - - Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; - Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; - - procedure Set (Status : Exit_Status) is - begin - Ada.Command_Line.Set_Exit_Status (Status); + SPARK_Terminal.Set_Exit_Status (Status); end Set; - subtype Port_Type is GNAT.Sockets.Port_Type; + subtype Port_Type is SPARK_Sockets.Port_Type; - subtype Level_Type is GNAT.Sockets.Level_Type; + subtype Level_Type is SPARK_Sockets.Level_Type; - subtype Socket_Type is GNAT.Sockets.Socket_Type; - subtype Option_Name is GNAT.Sockets.Option_Name; - subtype Option_Type is GNAT.Sockets.Option_Type; - subtype Family_Type is GNAT.Sockets.Family_Type; + subtype Socket_Type is SPARK_Sockets.Socket_Type; + subtype Option_Name is SPARK_Sockets.Option_Name; + subtype Option_Type is SPARK_Sockets.Option_Type; + subtype Family_Type is SPARK_Sockets.Family_Type; - subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; - subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + subtype Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type; - Socket_Error : exception renames GNAT.Sockets.Socket_Error; + use type Family_Type; - Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + Socket_Error : exception renames SPARK_Sockets.Socket_Error; - Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address; - Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level; - Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet; + + Any_Inet_Addr : Inet_Addr_Type renames SPARK_Sockets.Any_Inet_Addr; CERT_FILE : constant String := "../certs/client-cert.pem"; KEY_FILE : constant String := "../certs/client-key.pem"; @@ -112,24 +99,26 @@ package body Tls_Client is subtype Byte_Array is WolfSSL.Byte_Array; - function Argument_Count return Natural is - begin - return Ada.Command_Line.Argument_Count; - end Argument_Count; + function Argument_Count return Natural renames + SPARK_Terminal.Argument_Count; + + function Argument (Number : Positive) return String with + Pre => Number <= Argument_Count; function Argument (Number : Positive) return String is begin - return Ada.Command_Line.Argument (Number); + return SPARK_Terminal.Argument (Number); end Argument; - procedure Run is + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + Client : in out SPARK_Sockets.Optional_Socket) is A : Sock_Addr_Type; - C : Socket_Type; -- Client socket. + C : SPARK_Sockets.Optional_Socket renames Client; D : Byte_Array (1 .. 200); P : constant Port_Type := 11111; - Ssl : WolfSSL.WolfSSL_Type; - Ctx : WolfSSL.Context_Type; + Addr : SPARK_Sockets.Optional_Inet_Addr; Bytes_Written : Integer; @@ -142,24 +131,44 @@ package body Tls_Client is Result : WolfSSL.Subprogram_Result; begin - if Argument_Count /= 1 then + if Argument_Count < 1 then Put_Line ("usage: tcl_client "); return; end if; - GNAT.Sockets.Create_Socket (Socket => C); + SPARK_Sockets.Create_Socket (C); + if not C.Exists then + Put_Line ("ERROR: Failed to create socket."); + return; + end if; + Addr := SPARK_Sockets.Inet_Addr (Argument (1)); + if not Addr.Exists or + (Addr.Exists and then Addr.Addr.Family /= Family_Inet) + then + Put_Line ("ERROR: please specify IPv4 address."); + SPARK_Sockets.Close_Socket (C); + Set (Exit_Status_Failure); + return; + end if; A := (Family => Family_Inet, - Addr => GNAT.Sockets.Inet_Addr (Argument (1)), + Addr => Addr.Addr, Port => P); - GNAT.Sockets.Connect_Socket (Socket => C, - Server => A); + Result := SPARK_Sockets.Connect_Socket (Socket => C.Socket, + Server => A); + if Result = Failure then + Put_Line ("ERROR: Failed to connect to server."); + SPARK_Sockets.Close_Socket (C); + Set (Exit_Status_Failure); + return; + end if; -- Create and initialize WOLFSSL_CTX. WolfSSL.Create_Context (Method => WolfSSL.TLSv1_3_Client_Method, Context => Ctx); if not WolfSSL.Is_Valid (Ctx) then Put_Line ("ERROR: failed to create WOLFSSL_CTX."); + SPARK_Sockets.Close_Socket (C); Set (Exit_Status_Failure); return; end if; @@ -173,6 +182,8 @@ package body Tls_Client is Put (CERT_FILE); Put (", please check the file."); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -186,6 +197,8 @@ package body Tls_Client is Put (KEY_FILE); Put (", please check the file."); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -199,6 +212,8 @@ package body Tls_Client is Put (CA_FILE); Put (", please check the file."); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -207,15 +222,20 @@ package body Tls_Client is WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl); if not WolfSSL.Is_Valid (Ssl) then Put_Line ("ERROR: failed to create WOLFSSL object."); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; -- Attach wolfSSL to the socket. Result := WolfSSL.Attach (Ssl => Ssl, - Socket => GNAT.Sockets.To_C (C)); + Socket => SPARK_Sockets.To_C (C.Socket)); if Result = Failure then Put_Line ("ERROR: Failed to set the file descriptor."); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -223,6 +243,9 @@ package body Tls_Client is Result := WolfSSL.Connect (Ssl); if Result = Failure then Put_Line ("ERROR: failed to connect to wolfSSL."); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -230,10 +253,9 @@ package body Tls_Client is Put ("Message for server: "); Ada.Text_IO.Get_Line (Text, Last); - Interfaces.C.To_C (Item => Text (1 .. Last), - Target => D, - Count => Count, - Append_Nul => False); + SPARK_Sockets.To_C (Item => Text (1 .. Last), + Target => D, + Count => Count); Bytes_Written := WolfSSL.Write (Ssl => Ssl, Data => D (1 .. Count)); if Bytes_Written < Last then @@ -244,6 +266,9 @@ package body Tls_Client is Put (Last); Put ("bytes were sent"); New_Line; + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); return; end if; @@ -251,19 +276,28 @@ package body Tls_Client is if Input.Result /= Success then Put_Line ("Read error."); Set (Exit_Status_Failure); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Ssl); + WolfSSL.Free (Context => Ctx); return; end if; - Interfaces.C.To_Ada (Item => Input.Buffer, - Target => Text, - Count => Last, - Trim_Nul => False); + if Input.Buffer'Length > Text'Length then + SPARK_Sockets.To_Ada (Item => Input.Buffer (1 .. 200), + Target => Text, + Count => Last); + else + SPARK_Sockets.To_Ada (Item => Input.Buffer, + Target => Text, + Count => Last); + end if; Put ("Server: "); Put (Text (1 .. Last)); New_Line; - GNAT.Sockets.Close_Socket (C); + SPARK_Sockets.Close_Socket (C); WolfSSL.Free (Ssl); WolfSSL.Free (Context => Ctx); + WolfSSL.Finalize; end Run; end Tls_Client; diff --git a/wrapper/Ada/tls_client.ads b/wrapper/Ada/tls_client.ads index 3b651f4f8..50a52b3cc 100644 --- a/wrapper/Ada/tls_client.ads +++ b/wrapper/Ada/tls_client.ads @@ -19,8 +19,19 @@ -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA -- -package Tls_Client is +-- The WolfSSL package. +with WolfSSL; pragma Elaborate_All (WolfSSL); - procedure Run; +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); + +package Tls_Client with SPARK_Mode is + + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + Client : in out SPARK_Sockets.Optional_Socket) with + Pre => (not Client.Exists and not + WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)), + Post => (not Client.Exists and not WolfSSL.Is_Valid (Ssl) and + not WolfSSL.Is_Valid (Ctx)); end Tls_Client; diff --git a/wrapper/Ada/tls_client_main.adb b/wrapper/Ada/tls_client_main.adb index 0cb7b89f3..ab50dab84 100644 --- a/wrapper/Ada/tls_client_main.adb +++ b/wrapper/Ada/tls_client_main.adb @@ -19,11 +19,15 @@ -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA -- -with Tls_Client; pragma Elaborate_All (Tls_Client); - +with Tls_Client; pragma Elaborate_All (Tls_Client); +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); +with WolfSSL; pragma Elaborate_All (WolfSSL); -- Application entry point for the Ada translation of the -- tls client v1.3 example in C. procedure Tls_Client_Main is + Ssl : WolfSSL.WolfSSL_Type; + Ctx : WolfSSL.Context_Type; + C : SPARK_Sockets.Optional_Socket; begin - Tls_Client.Run; + Tls_Client.Run (Ssl, Ctx, Client => C); end Tls_Client_Main; diff --git a/wrapper/Ada/tls_server.adb b/wrapper/Ada/tls_server.adb index 4b213fc3c..1eaca1349 100644 --- a/wrapper/Ada/tls_server.adb +++ b/wrapper/Ada/tls_server.adb @@ -21,17 +21,12 @@ -- Ada Standard Library packages. with Ada.Characters.Handling; -with Ada.Command_Line; with Ada.Strings.Bounded; with Ada.Text_IO.Bounded_IO; --- GNAT Library packages. -with GNAT.Sockets; +with SPARK_Terminal; pragma Elaborate_All (SPARK_Terminal); --- The WolfSSL package. -with WolfSSL; - -package body Tls_Server is +package body Tls_Server with SPARK_Mode is use type WolfSSL.Mode_Type; use type WolfSSL.Byte_Index; @@ -39,52 +34,57 @@ package body Tls_Server is use all type WolfSSL.Subprogram_Result; - package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200); - use all type Messages.Bounded_String; + procedure Put (Char : Character) is + begin + Ada.Text_IO.Put (Char); + end Put; - package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages); + procedure Put (Text : String) is + begin + Ada.Text_IO.Put (Text); + end Put; procedure Put_Line (Text : String) is begin Ada.Text_IO.Put_Line (Text); end Put_Line; - procedure Put_Line (Text : Messages.Bounded_String) is + procedure New_Line is begin - Messages_IO.Put_Line (Text); - end Put_Line; + Ada.Text_IO.New_Line; + end New_Line; - subtype Exit_Status is Ada.Command_Line.Exit_Status; + subtype Exit_Status is SPARK_Terminal.Exit_Status; - Exit_Status_Success : Exit_Status renames Ada.Command_Line.Success; - Exit_Status_Failure : Exit_Status renames Ada.Command_Line.Failure; + Exit_Status_Success : Exit_Status renames SPARK_Terminal.Exit_Status_Success; + Exit_Status_Failure : Exit_Status renames SPARK_Terminal.Exit_Status_Failure; - procedure Set (Status : Exit_Status) is + procedure Set (Status : Exit_Status) with Global => null is begin - Ada.Command_Line.Set_Exit_Status (Status); + SPARK_Terminal.Set_Exit_Status (Status); end Set; - subtype Port_Type is GNAT.Sockets.Port_Type; + subtype Port_Type is SPARK_Sockets.Port_Type; - subtype Level_Type is GNAT.Sockets.Level_Type; + subtype Level_Type is SPARK_Sockets.Level_Type; - subtype Socket_Type is GNAT.Sockets.Socket_Type; - subtype Option_Name is GNAT.Sockets.Option_Name; - subtype Option_Type is GNAT.Sockets.Option_Type; - subtype Family_Type is GNAT.Sockets.Family_Type; + subtype Socket_Type is SPARK_Sockets.Socket_Type; + subtype Option_Name is SPARK_Sockets.Option_Name; + subtype Option_Type is SPARK_Sockets.Option_Type; + subtype Family_Type is SPARK_Sockets.Family_Type; - subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type; - subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type; + subtype Sock_Addr_Type is SPARK_Sockets.Sock_Addr_Type; + subtype Inet_Addr_Type is SPARK_Sockets.Inet_Addr_Type; - Socket_Error : exception renames GNAT.Sockets.Socket_Error; + Socket_Error : exception renames SPARK_Sockets.Socket_Error; - Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address; + Reuse_Address : Option_Name renames SPARK_Sockets.Reuse_Address; - Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level; + Socket_Level : Level_Type renames SPARK_Sockets.Socket_Level; - Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet; + Family_Inet : Family_Type renames SPARK_Sockets.Family_Inet; - Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr; + Any_Inet_Addr : Inet_Addr_Type renames SPARK_Sockets.Any_Inet_Addr; CERT_FILE : constant String := "../certs/server-cert.pem"; KEY_FILE : constant String := "../certs/server-key.pem"; @@ -94,42 +94,64 @@ package body Tls_Server is Reply : constant Byte_Array := "I hear ya fa shizzle!"; - procedure Run is + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + L : in out SPARK_Sockets.Optional_Socket; + C : in out SPARK_Sockets.Optional_Socket) is A : Sock_Addr_Type; - L : Socket_Type; -- Listener socket. - C : Socket_Type; -- Client socket. P : constant Port_Type := 11111; Ch : Character; - Ssl : WolfSSL.WolfSSL_Type; - - Ctx : WolfSSL.Context_Type; Result : WolfSSL.Subprogram_Result; - M : Messages.Bounded_String; Shall_Continue : Boolean := True; Bytes_Written : Integer; Input : WolfSSL.Read_Result; + Option : Option_Type; begin - GNAT.Sockets.Create_Socket (Socket => L); - GNAT.Sockets.Set_Socket_Option (Socket => L, - Level => Socket_Level, - Option => (Name => Reuse_Address, - Enabled => True)); - GNAT.Sockets.Bind_Socket (Socket => L, - Address => (Family => Family_Inet, - Addr => Any_Inet_Addr, - Port => P)); - GNAT.Sockets.Listen_Socket (Socket => L, - Length => 5); + SPARK_Sockets.Create_Socket (Socket => L); + if not L.Exists then + Put_Line ("ERROR: Failed to create socket."); + return; + end if; + + Option := (Name => Reuse_Address, Enabled => True); + Result := SPARK_Sockets.Set_Socket_Option (Socket => L.Socket, + Level => Socket_Level, + Option => Option); + if Result = Failure then + Put_Line ("ERROR: Failed to set socket option."); + SPARK_Sockets.Close_Socket (L); + return; + end if; + + A := (Family => Family_Inet, + Addr => Any_Inet_Addr, + Port => P); + Result := SPARK_Sockets.Bind_Socket (Socket => L.Socket, + Address => A); + if Result = Failure then + Put_Line ("ERROR: Failed to bind socket."); + SPARK_Sockets.Close_Socket (L); + return; + end if; + + Result := SPARK_Sockets.Listen_Socket (Socket => L.Socket, + Length => 5); + if Result = Failure then + Put_Line ("ERROR: Failed to configure listener socket."); + SPARK_Sockets.Close_Socket (L); + return; + end if; -- Create and initialize WOLFSSL_CTX. WolfSSL.Create_Context (Method => WolfSSL.TLSv1_3_Server_Method, Context => Ctx); if not WolfSSL.Is_Valid (Ctx) then Put_Line ("ERROR: failed to create WOLFSSL_CTX."); + SPARK_Sockets.Close_Socket (L); Set (Exit_Status_Failure); return; end if; @@ -144,10 +166,12 @@ package body Tls_Server is File => CERT_FILE, Format => WolfSSL.Format_Pem); if Result = Failure then - M := Messages.To_Bounded_String ("ERROR: failed to load "); - Messages.Append (M, CERT_FILE); - Messages.Append (M, ", please check the file."); - Put_Line (M); + Put ("ERROR: failed to load "); + Put (CERT_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -157,10 +181,12 @@ package body Tls_Server is File => KEY_FILE, Format => WolfSSL.Format_Pem); if Result = Failure then - M := Messages.To_Bounded_String ("ERROR: failed to load "); - Messages.Append (M, KEY_FILE); - Messages.Append (M, ", please check the file."); - Put_Line (M); + Put ("ERROR: failed to load "); + Put (KEY_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -170,39 +196,53 @@ package body Tls_Server is File => CA_FILE, Path => ""); if Result = Failure then - M := Messages.To_Bounded_String ("ERROR: failed to load "); - Messages.Append (M, CA_FILE); - Messages.Append (M, ", please check the file."); - Put_Line (M); + Put ("ERROR: failed to load "); + Put (CA_FILE); + Put (", please check the file."); + New_Line; + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; while Shall_Continue loop + pragma Loop_Invariant (not C.Exists and + not WolfSSL.Is_Valid (Ssl) and + WolfSSL.Is_Valid (Ctx)); + Put_Line ("Waiting for a connection..."); - begin - GNAT.Sockets.Accept_Socket (Server => L, - Socket => C, - Address => A); - exception - when Socket_Error => - Shall_Continue := False; - Put_Line ("ERROR: failed to accept the connection."); - end; + SPARK_Sockets.Accept_Socket (Server => L.Socket, + Socket => C, + Address => A, + Result => Result); + if Result = Failure then + Put_Line ("ERROR: failed to accept the connection."); + SPARK_Sockets.Close_Socket (L); + WolfSSL.Free (Context => Ctx); + return; + end if; -- Create a WOLFSSL object. WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl); if not WolfSSL.Is_Valid (Ssl) then Put_Line ("ERROR: failed to create WOLFSSL object."); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; -- Attach wolfSSL to the socket. Result := WolfSSL.Attach (Ssl => Ssl, - Socket => GNAT.Sockets.To_C (C)); + Socket => SPARK_Sockets.To_C (C.Socket)); if Result = Failure then Put_Line ("ERROR: Failed to set the file descriptor."); + WolfSSL.Free (Ssl); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -211,6 +251,10 @@ package body Tls_Server is Result := WolfSSL.Accept_Connection (Ssl); if Result = Failure then Put_Line ("Accept error."); + WolfSSL.Free (Ssl); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; @@ -218,25 +262,27 @@ package body Tls_Server is Put_Line ("Client connected successfully."); Input := WolfSSL.Read (Ssl); - if Input.Result /= Success then Put_Line ("Read error."); + WolfSSL.Free (Ssl); + SPARK_Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (C); + WolfSSL.Free (Context => Ctx); Set (Exit_Status_Failure); return; end if; -- Print to stdout any data the client sends. - M := Messages.To_Bounded_String (""); for I in Input.Buffer'Range loop Ch := Character (Input.Buffer (I)); if Ada.Characters.Handling.Is_Graphic (Ch) then - Messages.Append (M, Ch); + Put (Ch); else null; -- Ignore the "newline" characters at end of message. end if; end loop; - Put_Line (M); + New_Line; -- Check for server shutdown command. if Input.Last >= 8 then @@ -252,12 +298,15 @@ package body Tls_Server is end if; Result := WolfSSL.Shutdown (Ssl); + if Result = Failure then + Put_Line ("ERROR: Failed to shutdown WolfSSL context."); + end if; WolfSSL.Free (Ssl); - GNAT.Sockets.Close_Socket (C); + SPARK_Sockets.Close_Socket (C); Put_Line ("Shutdown complete."); end loop; - GNAT.Sockets.Close_Socket (L); + SPARK_Sockets.Close_Socket (L); WolfSSL.Free (Context => Ctx); WolfSSL.Finalize; end Run; diff --git a/wrapper/Ada/tls_server.ads b/wrapper/Ada/tls_server.ads index fccb6610b..142fad2ce 100644 --- a/wrapper/Ada/tls_server.ads +++ b/wrapper/Ada/tls_server.ads @@ -18,8 +18,22 @@ -- along with this program; if not, write to the Free Software -- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA -- -package Tls_Server is - procedure Run; +-- SPARK wrapper package around GNAT Library packages. +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); + +-- The WolfSSL package. +with WolfSSL; pragma Elaborate_All (WolfSSL); + +package Tls_Server with SPARK_Mode is + + procedure Run (Ssl : in out WolfSSL.WolfSSL_Type; + Ctx : in out WolfSSL.Context_Type; + L : in out SPARK_Sockets.Optional_Socket; + C : in out SPARK_Sockets.Optional_Socket) with + Pre => (not C.Exists and not L.Exists and not + WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)), + Post => (not C.Exists and not L.Exists and not + WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)); end Tls_Server; diff --git a/wrapper/Ada/tls_server_main.adb b/wrapper/Ada/tls_server_main.adb index 7f3450335..80b3a88d7 100644 --- a/wrapper/Ada/tls_server_main.adb +++ b/wrapper/Ada/tls_server_main.adb @@ -21,9 +21,19 @@ with Tls_Server; pragma Elaborate_All (Tls_Server); +-- SPARK wrapper package around GNAT Library packages. +with SPARK_Sockets; pragma Elaborate_All (SPARK_Sockets); + +-- The WolfSSL package. +with WolfSSL; pragma Elaborate_All (WolfSSL); + -- Application entry point for the Ada translation of the -- tls server v1.3 example in C. procedure Tls_Server_Main is + Ssl : WolfSSL.WolfSSL_Type; + Ctx : WolfSSL.Context_Type; + L : SPARK_Sockets.Optional_Socket; + C : SPARK_Sockets.Optional_Socket; begin - Tls_Server.Run; + Tls_Server.Run (Ssl, Ctx, L, C); end Tls_Server_Main;