@@ -24,6 +24,8 @@ with Ada.Characters.Handling;
2424with Ada.Strings.Bounded ;
2525with Ada.Text_IO.Bounded_IO ;
2626
27+ with Interfaces.C.Strings ;
28+
2729with SPARK_Terminal ; pragma Elaborate_All (SPARK_Terminal);
2830
2931package body Tls_Server with SPARK_Mode is
@@ -35,6 +37,9 @@ package body Tls_Server with SPARK_Mode is
3537
3638 Success : WolfSSL.Subprogram_Result renames WolfSSL.Success;
3739
40+ subtype chars_ptr is WolfSSL.chars_ptr;
41+ subtype unsigned is WolfSSL.unsigned;
42+
3843 procedure Put (Char : Character) is
3944 begin
4045 Ada.Text_IO.Put (Char);
@@ -87,14 +92,66 @@ package body Tls_Server with SPARK_Mode is
8792
8893 Any_Inet_Addr : Inet_Addr_Type renames SPARK_Sockets.Any_Inet_Addr;
8994
90- CERT_FILE : constant String := " ../../../ certs/server-cert.pem" ;
91- KEY_FILE : constant String := " ../../../ certs/server-key.pem" ;
92- CA_FILE : constant String := " ../../../ certs/client-cert.pem" ;
95+ CERT_FILE : constant String := " ../../certs/server-cert.pem" ;
96+ KEY_FILE : constant String := " ../../certs/server-key.pem" ;
97+ CA_FILE : constant String := " ../../certs/client-cert.pem" ;
9398
9499 subtype Byte_Array is WolfSSL.Byte_Array;
95100
96101 Reply : constant Byte_Array := " I hear ya fa shizzle!" ;
97102
103+
104+ function PSK_Server_Callback
105+ (Unused : WolfSSL.WolfSSL_Type;
106+ Identity : chars_ptr;
107+ Key : chars_ptr;
108+ Key_Max_Length : unsigned) return unsigned
109+ with Convention => C;
110+
111+ function PSK_Server_Callback
112+ (Unused : WolfSSL.WolfSSL_Type;
113+ Identity : chars_ptr;
114+ Key : chars_ptr;
115+ Key_Max_Length : unsigned) return unsigned
116+ with
117+ SPARK_Mode => Off
118+ is
119+ use type Interfaces.C.unsigned;
120+
121+ -- Identity is OpenSSL testing default for openssl s_client, keep same
122+ Identity_String : constant String := " Client_identity" ;
123+ -- Test key in hex is 0x1a2b3c4d, in decimal 439,041,101
124+ Key_String : constant String :=
125+ Character'Val (26 )
126+ & Character'Val (43 )
127+ & Character'Val (60 )
128+ & Character'Val (77 );
129+ -- These values are aligned with test values in wolfssl/wolfssl/test.h
130+ -- and wolfssl-examples/psk/server-psk.c for testing interoperability.
131+
132+ begin
133+
134+ if Interfaces.C.Strings.Value
135+ (Item => Identity,
136+ Length => Identity_String'Length) /= Identity_String or else
137+ Key_Max_Length < Key_String'Length
138+ then
139+ return 0 ;
140+ end if ;
141+
142+ put_line (Interfaces.C.Strings.Value
143+ (Item => Identity,
144+ Length => Identity_String'Length) );
145+
146+ Interfaces.C.Strings.Update
147+ (Item => Key,
148+ Offset => 0 ,
149+ Str => Key_String,
150+ Check => False);
151+
152+ return Key_String'Length;
153+ end PSK_Server_Callback ;
154+
98155 procedure Run (Ssl : in out WolfSSL.WolfSSL_Type;
99156 Ctx : in out WolfSSL.Context_Type;
100157 L : in out SPARK_Sockets.Optional_Socket;
@@ -105,7 +162,7 @@ package body Tls_Server with SPARK_Mode is
105162 Ch : Character;
106163
107164 Result : WolfSSL.Subprogram_Result;
108- DTLS : Boolean;
165+ DTLS, PSK : Boolean;
109166 Shall_Continue : Boolean := True;
110167
111168 Input : WolfSSL.Read_Result;
@@ -119,14 +176,18 @@ package body Tls_Server with SPARK_Mode is
119176 end if ;
120177
121178 if SPARK_Terminal.Argument_Count > 1
122- or (SPARK_Terminal.Argument_Count = 1
123- and then SPARK_Terminal.Argument (1 ) /= " --dtls" )
179+ or (SPARK_Terminal.Argument_Count = 1 and then
180+ SPARK_Terminal.Argument (1 ) /= " --dtls" and then
181+ SPARK_Terminal.Argument (1 ) /= " --psk" )
124182 then
125- Put_Line (" usage: tls_server_main [--dtls]" );
183+ Put_Line (" usage: tls_server_main [--dtls | --psk ]" );
126184 return ;
127185 end if ;
128186
129- DTLS := (SPARK_Terminal.Argument_Count = 1 );
187+ if SPARK_Terminal.Argument_Count = 1 then
188+ DTLS := (SPARK_Terminal.Argument (1 ) = " --dtls" );
189+ PSK := (SPARK_Terminal.Argument (1 ) = " --psk" );
190+ end if ;
130191
131192 if DTLS then
132193 SPARK_Sockets.Create_Datagram_Socket (Socket => L);
@@ -197,63 +258,73 @@ package body Tls_Server with SPARK_Mode is
197258 return ;
198259 end if ;
199260
200- -- Require mutual authentication.
201- WolfSSL.Set_Verify
202- (Context => Ctx,
203- Mode => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert);
261+ if not PSK then
262+ -- Require mutual authentication.
263+ WolfSSL.Set_Verify
264+ (Context => Ctx,
265+ Mode => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert);
204266
205- -- Check verify is set correctly (GitHub #7461)
206- if WolfSSL.Get_Verify(Context => Ctx) /= (WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert) then
207- Put (" Error: Verify does not match requested" );
208- New_Line;
209- return ;
210- end if ;
267+ -- Check verify is set correctly (GitHub #7461)
268+ if WolfSSL.Get_Verify(Context => Ctx) /= (WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert) then
269+ Put (" Error: Verify does not match requested" );
270+ New_Line;
271+ return ;
272+ end if ;
211273
212- -- Load server certificates into WOLFSSL_CTX.
213- Result := WolfSSL.Use_Certificate_File (Context => Ctx,
214- File => CERT_FILE,
215- Format => WolfSSL.Format_Pem);
216- if Result /= Success then
217- Put (" ERROR: failed to load " );
218- Put (CERT_FILE);
219- Put (" , please check the file." );
220- New_Line;
221- SPARK_Sockets.Close_Socket (L);
222- WolfSSL.Free (Context => Ctx);
223- Set (Exit_Status_Failure);
224- return ;
225- end if ;
274+ -- Load server certificates into WOLFSSL_CTX.
275+ Result := WolfSSL.Use_Certificate_File (Context => Ctx,
276+ File => CERT_FILE,
277+ Format => WolfSSL.Format_Pem);
278+ if Result /= Success then
279+ Put (" ERROR: failed to load " );
280+ Put (CERT_FILE);
281+ Put (" , please check the file." );
282+ New_Line;
283+ SPARK_Sockets.Close_Socket (L);
284+ WolfSSL.Free (Context => Ctx);
285+ Set (Exit_Status_Failure);
286+ return ;
287+ end if ;
226288
227- -- Load server key into WOLFSSL_CTX.
228- Result := WolfSSL.Use_Private_Key_File (Context => Ctx,
229- File => KEY_FILE,
230- Format => WolfSSL.Format_Pem);
231- if Result /= Success then
232- Put (" ERROR: failed to load " );
233- Put (KEY_FILE);
234- Put (" , please check the file." );
235- New_Line;
236- SPARK_Sockets.Close_Socket (L);
237- WolfSSL.Free (Context => Ctx);
238- Set (Exit_Status_Failure);
239- return ;
240- end if ;
289+ -- Load server key into WOLFSSL_CTX.
290+ Result := WolfSSL.Use_Private_Key_File (Context => Ctx,
291+ File => KEY_FILE,
292+ Format => WolfSSL.Format_Pem);
293+ if Result /= Success then
294+ Put (" ERROR: failed to load " );
295+ Put (KEY_FILE);
296+ Put (" , please check the file." );
297+ New_Line;
298+ SPARK_Sockets.Close_Socket (L);
299+ WolfSSL.Free (Context => Ctx);
300+ Set (Exit_Status_Failure);
301+ return ;
302+ end if ;
241303
242- -- Load client certificate as "trusted" into WOLFSSL_CTX.
243- Result := WolfSSL.Load_Verify_Locations (Context => Ctx,
244- File => CA_FILE,
245- Path => " " );
246- if Result /= Success then
247- Put (" ERROR: failed to load " );
248- Put (CA_FILE);
249- Put (" , please check the file." );
250- New_Line;
251- SPARK_Sockets.Close_Socket (L);
252- WolfSSL.Free (Context => Ctx);
253- Set (Exit_Status_Failure);
254- return ;
304+ -- Load client certificate as "trusted" into WOLFSSL_CTX.
305+ Result := WolfSSL.Load_Verify_Locations (Context => Ctx,
306+ File => CA_FILE,
307+ Path => " " );
308+
309+ if Result /= Success then
310+ Put (" ERROR: failed to load " );
311+ Put (CA_FILE);
312+ Put (" , please check the file." );
313+ New_Line;
314+ SPARK_Sockets.Close_Socket (L);
315+ WolfSSL.Free (Context => Ctx);
316+ Set (Exit_Status_Failure);
317+ return ;
318+ end if ;
255319 end if ;
256320
321+ if PSK then
322+ -- Use PSK for authentication.
323+ WolfSSL.Set_Context_PSK_Server_Callback
324+ (Context => Ctx,
325+ Callback => PSK_Server_Callback'Access );
326+ end if ;
327+
257328 while Shall_Continue loop
258329 pragma Loop_Invariant (not C.Exists);
259330 pragma Loop_Invariant (not WolfSSL.Is_Valid (Ssl));
0 commit comments