luna - wolfssl/wrapper/Ada/wolfssl.ads

  1-- wolfssl.ads
  2--
  3-- Copyright (C) 2006-2026 wolfSSL Inc.
  4--
  5-- This file is part of wolfSSL.
  6--
  7-- wolfSSL is free software; you can redistribute it and/or modify
  8-- it under the terms of the GNU General Public License as published by
  9-- the Free Software Foundation; either version 3 of the License, or
 10-- (at your option) any later version.
 11--
 12-- wolfSSL is distributed in the hope that it will be useful,
 13-- but WITHOUT ANY WARRANTY; without even the implied warranty of
 14-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 15-- GNU General Public License for more details.
 16--
 17-- You should have received a copy of the GNU General Public License
 18-- along with this program; if not, write to the Free Software
 19-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
 20--
 21with Interfaces.C;
 22
 23--  This package is annotated "with SPARK_Mode" that SPARK can verify
 24--  the API of this package is used correctly.
 25package WolfSSL with SPARK_Mode is
 26
 27   type Subprogram_Result is new Integer;
 28   Success : constant Subprogram_Result;
 29   --  Indicates success for some functions.
 30   --  Do not use, unless you know what you do.
 31
 32   Failure : constant Subprogram_Result;
 33   --  Indicates failure for some functions.
 34   --  Do not use, unless you know what you do.
 35
 36   Exception_Error : constant := -1234567;
 37   --  Indicates an exception was raised during a subprogram call.
 38
 39   function Initialize return Subprogram_Result;
 40   --  Initializes the wolfSSL library for use. Must be called once per
 41   --  application and before any other call to the library.
 42
 43   function Finalize return Subprogram_Result;
 44   --  Un-initializes the wolfSSL library from further use.
 45   --  Doesn't have to be called, though it will free any resources
 46   --  used by the library.
 47
 48   subtype unsigned is Interfaces.C.unsigned;
 49
 50   subtype Byte_Type  is Interfaces.C.char;
 51   subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000;
 52   subtype Byte_Array is Interfaces.C.char_array;
 53
 54   use type Interfaces.C.size_t;
 55
 56   type Context_Type is limited private with
 57     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
 58   --  Instances of this type are called SSL Contexts.
 59
 60   function Is_Valid (Context : Context_Type) return Boolean with
 61      Annotate => (GNATprove, Ownership, "Needs_Reclamation");
 62   --  Indicates if the SSL Context has successfully been initialized.
 63   --  If initialized, the SSL Context has allocated resources
 64   --  that needs to be deallocated before application exit.
 65   --  Annotation added for GNATprove ownership analysis.
 66   --    https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
 67
 68   type Method_Type is limited private with
 69     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
 70
 71   function Is_Valid (Method : Method_Type) return Boolean with
 72      Annotate => (GNATprove, Ownership, "Needs_Reclamation");
 73   --  Annotation added for GNATprove ownership analysis.
 74   --    https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
 75
 76   function TLSv1_2_Server_Method return Method_Type;
 77   --  This function is used to indicate that the application is a server
 78   --  and will only support the TLS 1.2 protocol.
 79
 80   function TLSv1_2_Client_Method return Method_Type;
 81   --  This function is used to indicate that the application is a client
 82   --  and will only support the TLS 1.2 protocol.
 83
 84   function TLSv1_3_Server_Method return Method_Type;
 85   --  This function is used to indicate that the application is a server
 86   --  and will only support the TLS 1.3 protocol.
 87
 88   function TLSv1_3_Client_Method return Method_Type;
 89   --  This function is used to indicate that the application is a client
 90   --  and will only support the TLS 1.3 protocol.
 91
 92   function DTLSv1_2_Server_Method return Method_Type;
 93   --  This function is used to indicate that the application is a server
 94   --  and will only support the DTLS 1.2 protocol.
 95
 96   function DTLSv1_2_Client_Method return Method_Type;
 97   --  This function is used to indicate that the application is a client
 98   --  and will only support the DTLS 1.2 protocol.
 99
100   function DTLSv1_3_Server_Method return Method_Type;
101   --  This function is used to indicate that the application is a server
102   --  and will only support the DTLS 1.3 protocol.
103
104   function DTLSv1_3_Client_Method return Method_Type;
105   --  This function is used to indicate that the application is a client
106   --  and will only support the DTLS 1.3 protocol.
107
108   procedure Create_Context (Method  : in out Method_Type;
109                             Context : out Context_Type) with
110      Post => not Is_Valid (Method);
111   --  This function creates a new SSL context, taking a desired SSL/TLS
112   --  protocol method for input.
113   --  If successful Is_Valid (Context) = True, otherwise False.
114   --  The Method is consumed by this operation and set to null.
115
116   procedure Free (Context : in out Context_Type) with
117      Post => not Is_Valid (Context);
118   --  This function frees an allocated SSL Context object.
119   --  If Context is not valid, this is a no-op.
120
121   type Mode_Type is private;
122
123   function "or" (Left, Right : Mode_Type) return Mode_Type;
124
125   Verify_None : constant Mode_Type;
126   --  Client mode: the client will not verify the certificate received
127   --  from the server and the handshake will continue as normal.
128   --
129   --  Server mode: the server will not send a certificate request to
130   --  the client. As such, client verification will not be enabled.
131
132   Verify_Peer : constant Mode_Type;
133   --  Client mode: the client will verify the certificate received from
134   --  the server during the handshake. This is turned on by default
135   --  in wolfSSL, therefore, using this option has no effect.
136   --
137   --  Server mode: the server will send a certificate request to
138   --  the client and verify the client certificate received.
139
140   Verify_Fail_If_No_Peer_Cert : constant Mode_Type;
141   --  Client mode: no effect when used on the client side.
142   --
143   --  Server mode: the verification will fail on the server side if
144   --  the client fails to send a certificate when requested to do so
145   --  (when using Verify_Peer on the SSL server).
146
147   Verify_Client_Once : constant Mode_Type;
148
149   Verify_Post_Handshake : constant Mode_Type;
150
151   Verify_Fail_Except_Psk : constant Mode_Type;
152   --  Client mode: no effect when used on the client side.
153   --
154   --  Server mode: the verification is the same as
155   --  Verify_Fail_If_No_Peer_Cert except in the case of a PSK connection.
156   --  If a PSK connection is being made then the connection
157   --  will go through without a peer cert.
158
159   Verify_Default : constant Mode_Type;
160
161   procedure Set_Verify (Context : Context_Type;
162                         Mode    : Mode_Type) with
163      Pre => Is_Valid (Context);
164   --  This function sets the verification method for remote peers
165
166   function Get_Verify (Context : Context_Type) return Mode_Type;
167
168   type File_Format is private;
169
170   Format_Asn1    : constant File_Format;
171   Format_Pem     : constant File_Format;
172   Format_Default : constant File_Format;
173
174   function Use_Certificate_File (Context : Context_Type;
175                                  File    : String;
176                                  Format  : File_Format)
177                                  return Subprogram_Result with
178      Pre => Is_Valid (Context);
179   --  This function loads a certificate file into the SSL context.
180   --  The file is provided by the file argument. The format argument
181   --  specifies the format type of the file, either ASN1 or
182   --  PEM file types. Please see the examples for proper usage.
183
184   function Use_Certificate_Buffer (Context : Context_Type;
185                                    Input   : Byte_Array;
186                                    Format  : File_Format)
187                                    return Subprogram_Result with
188      Pre => Is_Valid (Context);
189   --  This function loads a certificate buffer into the SSL Context.
190   --  It behaves like the non-buffered version (Use_Certificate_File),
191   --  only differing in its ability to be called with a buffer as input
192   --  instead of a file. The buffer is provided by the Input argument.
193   --  Format specifies the format type of the buffer; ASN1 or PEM.
194   --  Please see the examples for proper usage.
195
196   function Use_Private_Key_File (Context : Context_Type;
197                                  File    : String;
198                                  Format  : File_Format)
199                                  return Subprogram_Result with
200      Pre => Is_Valid (Context);
201   --  This function loads a private key file into the SSL context.
202   --  The file is provided by the File argument. The Format argument
203   --  specifies the format type of the file - ASN1 or PEM.
204   --  Please see the examples for proper usage.
205
206   function Use_Private_Key_Buffer (Context : Context_Type;
207                                    Input   : Byte_Array;
208                                    Format  : File_Format)
209                                    return Subprogram_Result with
210      Pre => Is_Valid (Context);
211   --  This function loads a private key buffer into the SSL Context.
212   --  It behaves like the non-buffered version (Use_Private_Key_File),
213   --  only differing in its ability to be called with a buffer as input
214   --  instead of a file. The buffer is provided by the Input argument.
215   --  Format specifies the format type of the buffer; ASN1 or PEM.
216   --  Please see the examples for proper usage.
217
218   function Load_Verify_Locations (Context : Context_Type;
219                                   File    : String;
220                                   Path    : String)
221                                   return Subprogram_Result with
222      Pre => Is_Valid (Context);
223   --  This function loads PEM-formatted CA certificate files into
224   --  the SSL context. These certificates will be treated as trusted
225   --  root certificates and used to verify certs received from peers
226   --  during the SSL handshake. The root certificate file,
227   --  provided by the File argument, may be a single certificate or
228   --  a file containing multiple certificates. If multiple CA certs
229   --  are included in the same file, wolfSSL will load them in the same
230   --  order they are presented in the file. The path argument is
231   --  a pointer to the name of a directory that contains certificates
232   --  of trusted root CAs. If the value of File is not empty "",
233   --  path may be specified as "" if not needed. If path is specified
234   --  and NO_WOLFSSL_DIR was not defined when building the library,
235   --  wolfSSL will load all CA certificates located in the given
236   --  directory. This function will attempt to load all files in
237   --  the directory. This function expects PEM formatted CERT_TYPE file
238   --  with header "--BEGIN CERTIFICATE--".
239
240   function Load_Verify_Buffer (Context : Context_Type;
241                                Input   : Byte_Array;
242                                Format  : File_Format)
243                                return Subprogram_Result with
244      Pre => Is_Valid (Context);
245   --  This function loads a CA certificate buffer into the SSL
246   --  Context. It behaves like the non-buffered version, only differing
247   --  in its ability to be called with a buffer as input instead of
248   --  a file. The buffer is provided by the Input argument.
249   --  Format specifies the format type of the buffer; ASN1 or PEM.
250   --  More than one CA certificate may be loaded
251   --  per buffer as long as the format is in PEM.
252   --  Please see the examples for proper usage.
253
254   type WolfSSL_Type is limited private with
255     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
256   --  Instances of this type are called SSL Sessions.
257
258   function Is_Valid (Ssl : WolfSSL_Type) return Boolean with
259      Annotate => (GNATprove, Ownership, "Needs_Reclamation");
260   --  Indicates if the SSL Session has successfully been initialized.
261   --  If initialized, the SSL Session has allocated resources
262   --  that needs to be deallocated before application exit.
263   --  Annotation added for GNATprove ownership analysis.
264   --    https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
265
266   procedure Create_WolfSSL (Context : Context_Type;
267                             Ssl     : out WolfSSL_Type) with
268      Pre => Is_Valid (Context);
269   --  This function creates a new SSL session, taking an already created
270   --  SSL context as input.
271   --  If successful Is_Valid (Ssl) = True, otherwise False.
272
273   function Use_Certificate_File (Ssl     : WolfSSL_Type;
274                                  File    : String;
275                                  Format  : File_Format)
276                                  return Subprogram_Result with
277      Pre => Is_Valid (Ssl);
278   --  This function loads a certificate file into the SSL session.
279   --  The certificate file is provided by the file argument.
280   --  The format argument specifies the format type of the file
281   --  either ASN1 or PEM.
282
283   function Use_Certificate_Buffer (Ssl     : WolfSSL_Type;
284                                    Input   : Byte_Array;
285                                    Format  : File_Format)
286                                    return Subprogram_Result with
287      Pre => Is_Valid (Ssl);
288   --  This function loads a certificate buffer into the SSL session
289   --  object. It behaves like the non-buffered version, only differing
290   --  in its ability to be called with a buffer as input instead
291   --  of a file. The buffer is provided by the Input argument.
292   --  Format specifies the format type of the buffer; ASN1 or PEM.
293   --  Please see the examples for proper usage.
294
295   function Use_Private_Key_File (Ssl     : WolfSSL_Type;
296                                  File    : String;
297                                  Format  : File_Format)
298                                  return Subprogram_Result with
299      Pre => Is_Valid (Ssl);
300   --  This function loads a private key file into the SSL session.
301   --  The key file is provided by the File argument. The Format argument
302   --  specifies the format type of the file - ASN1 or PEM.
303
304   function Use_Private_Key_Buffer (Ssl     : WolfSSL_Type;
305                                    Input   : Byte_Array;
306                                    Format  : File_Format)
307                                    return Subprogram_Result with
308      Pre => Is_Valid (Ssl);
309   --  This function loads a private key buffer into the SSL session
310   --  object. It behaves like the non-buffered version, only differing
311   --  in its ability to be called with a buffer as input instead
312   --  of a file. The buffer is provided by the Input argument.
313   --  Format specifies the format type of the buffer; ASN1 or PEM.
314   --  Please see the examples for proper usage.
315
316   function Attach (Ssl    : WolfSSL_Type;
317                    Socket : Integer)
318                    return Subprogram_Result with
319      Pre => Is_Valid (Ssl);
320   --  Attach wolfSSL to the socket.
321   --
322   --  This function assigns a file descriptor (Socket) as
323   --  the input/output facility for the SSL connection.
324   --  Typically this will be a socket file descriptor.
325
326   procedure Keep_Arrays (Ssl : WolfSSL_Type) with
327      Pre => Is_Valid (Ssl);
328   --  Normally, at the end of the SSL handshake, wolfSSL frees
329   --  temporary arrays. Calling this function before the handshake
330   --  begins will prevent wolfSSL from freeing temporary arrays.
331   --  Temporary arrays may be needed for things such as
332   --  wolfSSL_get_keys() or PSK hints. When the user is done with
333   --  temporary arrays, either Free_Arrays(..) may be called to free
334   --  the resources immediately, or alternatively the resources will
335   --  be freed when the associated SSL object is freed.
336
337   procedure Free_Arrays (Ssl : WolfSSL_Type) with
338      Pre => Is_Valid (Ssl);
339   --  Normally, at the end of the SSL handshake, wolfSSL frees temporary
340   --  arrays. If Keep_Arrays(..) has been called before the handshake,
341   --  wolfSSL will not free temporary arrays. This function explicitly
342   --  frees temporary arrays and should be called when the user is done
343   --  with temporary arrays and does not want to wait for the SSL object
344   --  to be freed to free these resources.
345
346   function Accept_Connection (Ssl : WolfSSL_Type)
347                               return Subprogram_Result with
348      Pre => Is_Valid (Ssl);
349   --  The name of this function is not Accept (..) because the word
350   --  "accept" is a reserved keyword in the Ada language.
351   --
352   --  This function is called on the server side and waits for an
353   --  SSL client to initiate the SSL/TLS handshake. When this function
354   --  is called, the underlying communication channel has already been
355   --  set up. This function works with both blocking and
356   --  non-blocking I/O. When the underlying I/O is non-blocking,
357   --  Accept_Connection (..) will return when the underlying I/O could
358   --  not satisfy the needs of Accept_Connection (..) to continue
359   --  the handshake. In this case, a call to Get_Error(..) will
360   --  yield either Error_Want_Read or Error_Want_Write.
361   --  The calling process must then repeat the call to
362   --  Accept_Connection (..) when data is available to read and
363   --  wolfSSL will pick up where it left off. When using a
364   --  non_blocking socket, nothing needs to be done, but select() can
365   --  be used to check for the required condition.
366   --  If the underlying I/O is blocking, Accept_Connection (..) will
367   --  only return once the handshake has been finished or
368   --  an error occurred.
369
370   --  This record type has discriminants with default values to be able
371   --  to compile this code under the restriction No Secondary Stack.
372   type Read_Result (Success : Boolean := False;
373                     Last    : Byte_Index := Byte_Index'Last) is record
374      case Success is
375         when True  => Buffer : Byte_Array (1 .. Last);
376         when False => Code : Subprogram_Result; --  Error code
377      end case;
378   end record;
379
380   procedure Read (Ssl : WolfSSL_Type;
381                   Result : out Read_Result) with
382      Pre => Is_Valid (Ssl);
383   --  This function reads a number of bytes from the SSL session (ssl)
384   --  internal read buffer into the buffer data. The bytes read are
385   --  removed from the internal receive buffer.
386   --  If necessary Read(..) will negotiate an SSL/TLS session
387   --  if the handshake has not already
388   --  been performed yet by Connect(..) or Accept_Connection (..).
389   --  The SSL/TLS protocol uses SSL records which have a maximum size
390   --  of 16kB (the max record size can be controlled by the
391   --  MAX_RECORD_SIZE define in /wolfssl/internal.h). As such, wolfSSL
392   --  needs to read an entire SSL record internally before it is able
393   --  to process and decrypt the record. Because of this, a call to
394   --  Read(..) will only be able to return the maximum buffer
395   --  size which has been decrypted at the time of calling. There may
396   --  be additional not-yet-decrypted data waiting in the internal
397   --  wolfSSL receive buffer which will be retrieved and decrypted with
398   --  the next call to Read(..).
399
400   --  This record type has discriminants with default values to be able
401   --  to compile this code under the restriction No Secondary Stack.
402   type Write_Result (Success : Boolean := False) is record
403      case Success is
404         when True  => Bytes_Written : Byte_Index;
405         when False => Code : Subprogram_Result; --  Error code
406      end case;
407   end record;
408
409   procedure Write (Ssl  : WolfSSL_Type;
410                    Data : Byte_Array;
411                    Result : out Write_Result) with
412      Pre => Is_Valid (Ssl);
413   --  The number of bytes written is returned.
414   --  This function writes bytes from the buffer, Data,
415   --  to the SSL connection, ssl. If necessary, Write(..) will
416   --  negotiate an SSL/TLS session if the handshake has not already
417   --  been performed yet by Connect(..) or Accept_Connection(..).
418   --  Write(..) works with both blocking and non-blocking I/O.
419   --  When the underlying I/O is non-blocking, Write(..) will return
420   --  when the underlying I/O could not satisfy the needs of Write(..)
421   --  to continue. In this case, a call to Get_Error(..) will
422   --  yield either Error_Want_Read or Error_Want_Write.
423   --  The calling process must then repeat the call to Write(..)
424   --  when the underlying I/O is ready. If the underlying I/O is
425   --  blocking, Write(..) will only return once the buffer data
426   --  has been completely written or an error occurred.
427
428   function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result with
429      Pre => Is_Valid (Ssl);
430   --  This function shuts down an active SSL/TLS connection using
431   --  the SSL session, ssl. This function will try to send a
432   --  "close notify" alert to the peer. The calling application can
433   --  choose to wait for the peer to send its "close notify" alert
434   --  in response or just go ahead and shut down the underlying
435   --  connection after directly calling wolfSSL_shutdown (to save
436   --  resources). Either option is allowed by the TLS specification.
437   --  If the underlying connection will be used again in the future,
438   --  the complete two_directional shutdown procedure must be performed
439   --  to keep synchronization intact between the peers.
440   --  Shutdown(..) works with both blocking and non_blocking I/O.
441   --  When the underlying I/O is non_blocking, Shutdown(..) will
442   --  return an error if the underlying I/O could not satisfy the needs
443   --  of Shutdown(..) to continue. In this case, a call to
444   --  Get_Error(..) will yield either Error_Want_Read or
445   --  Error_Want_Write. The calling process must then repeat
446   --  the call to Shutdown() when the underlying I/O is ready.
447
448   procedure Free (Ssl : in out WolfSSL_Type) with
449      Post => not Is_Valid (Ssl);
450   --  Frees the resources allocated by the SSL session object.
451   --  If Ssl is not valid, this is a no-op.
452
453   function Connect (Ssl : WolfSSL_Type) return Subprogram_Result with
454      Pre => Is_Valid (Ssl);
455   --  This function is called on the client side and initiates
456   --  an SSL/TLS handshake with a server. When this function is called,
457   --  the underlying communication channel has already been set up.
458   --  Connect(..) works with both blocking and non_blocking I/O.
459   --  When the underlying I/O is non_blocking, Connect(..) will
460   --  return when the underlying I/O could not satisfy the needs
461   --  of wolfSSL_connect to continue the handshake. In this case,
462   --  a call to Get_Error(..) will yield either
463   --  Error_Want_Read or SSL_ERROR_WANT_WRITE. The calling process
464   --  must then repeat the call to Connect(..) when
465   --  the underlying I/O is ready and wolfSSL will pick up where
466   --  it left off. When using a non_blocking socket, nothing needs
467   --  to be done, but select() can be used to check for the required
468   --  condition. If the underlying I/O is blocking, Connect(..)
469   --  will only return once the handshake has been finished or an error
470   --  occurred. wolfSSL takes a different approach to certificate
471   --  verification than OpenSSL does. The default policy for the client
472   --  is to verify the server, this means that if you don't load CAs
473   --  to verify the server you'll get a connect error,
474   --  unable to verify. It you want to mimic OpenSSL behavior
475   --  of having SSL_connect succeed even if verifying the server fails
476   --  and reducing security you can do this by calling:
477   --  Set_Verify (Ctx, Verify_None, 0); before calling
478   --  Create_WolfSSL(...); Though it's not recommended.
479
480   type Error_Code is new Integer;
481
482   Error_Want_Read  : constant Error_Code;
483   Error_Want_Write : constant Error_Code;
484
485   function Get_Error (Ssl    : WolfSSL_Type;
486                       Result : Subprogram_Result) return Error_Code;
487   --  This function returns a unique error code describing why
488   --  the previous API function call (Connect, Accept_Connection,
489   --  Read, Write, etc.) resulted in an error return code.
490   --  After Get_Error is called and returns the unique error code,
491   --  wolfSSL_ERR_error_string() may be called to get a human readable
492   --  error string.
493
494   subtype Error_Message_Index is Natural range 0 .. 80;
495   --  The default error message length is 80 in WolfSSL unless
496   --  configured to another value. See the result
497   --  of the Max_Error_Size function.
498
499   type Error_Message (Last : Error_Message_Index := 0) is record
500      Text : String (1 .. Last);
501   end record;
502
503   procedure Error (Code    : in  Error_Code;
504                    Message : in out Error_Message);
505   --  This function converts an error code returned by Get_Error(..)
506   --  into a more human readable error string. Code is the error code
507   --  returned by Get_error(). The maximum length of error strings is
508   --  80 characters by default, as defined by MAX_ERROR_SZ
509   --  is wolfssl/wolfcrypt/error.h.
510   --
511   --  If Message has not been updated with a text, it may be because
512   --  an exception was raised during the execution of the subprogram.
513
514   function Max_Error_Size return Natural;
515   --  Returns the value of the defined MAX_ERROR_SZ integer
516   --  in wolfssl/wolfcrypt/error.h.
517
518   type RNG_Type is limited private with
519     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
520
521   function Is_Valid (Key : RNG_Type) return Boolean with
522      Annotate => (GNATprove, Ownership, "Needs_Reclamation");
523   --  Indicates if the RNG has successfully been initialized.
524   --  Annotation added for GNATprove ownership analysis.
525   --    https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
526
527   procedure Create_RNG (Key    : in out RNG_Type;
528                         Result : out Integer) with
529     Pre => not Is_Valid (Key),
530     Post => (if Result = 0 then Is_Valid (Key));
531   --  If successful Result = 0.
532
533   procedure Free_RNG (Key : in out RNG_Type) with
534     Pre => Is_Valid (Key),
535     Post => not Is_Valid (Key);
536   --  Frees resources associated with RNG and releases the underlying C object.
537
538   procedure RNG_Generate_Block (RNG    : RNG_Type;
539                                 Output : out Byte_Array;
540                                 Result : out Integer) with
541     Pre => Is_Valid (RNG);
542
543   type HMAC_Hash is (MD5, SHA, SHA256, SHA384, SHA512, SHA3_224,
544                      SHA3_256, SHA3_384, SHA3_512);
545
546   procedure PBKDF2 (Output     : out Byte_Array;
547                     Password   : Byte_Array;
548                     Salt       : Byte_Array;
549                     Iterations : Positive;
550                     Key_Length : Positive;
551                     HMAC       : HMAC_Hash;
552                     Result     : out Integer);
553
554   type RSA_Key_Type is limited private with
555     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
556
557   function Is_Valid (Key : RSA_Key_Type) return Boolean with
558      Annotate => (GNATprove, Ownership, "Needs_Reclamation");
559   --  Indicates if the RSA has successfully been initialized.
560   --  Annotation added for GNATprove ownership analysis.
561   --    https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
562
563   procedure Create_RSA (Key    : in out RSA_Key_Type;
564                         Result : out Integer) with
565     Pre => not Is_Valid (Key),
566     Post => (if Result = 0 then Is_Valid (Key));
567   --  If successful Result = 0.
568
569   procedure Free_RSA (Key : in out RSA_Key_Type) with
570     Pre => Is_Valid (Key),
571     Post => not Is_Valid (Key);
572   --  Frees resources associated with RSA and releases the underlying C object.
573
574   procedure Rsa_Public_Key_Decode (Input : Byte_Array;
575                                    Index : in out Byte_Index;
576                                    Key   : in out RSA_Key_Type;
577                                    Size  : Integer;
578                                    Result : out Integer) with
579     Pre => Is_Valid (Key);
580   --  This function parses a DER-formatted RSA public key,
581   --  extracts the public key and stores it in the RsaKey structure
582   --  specified by the Key input argument. It also sets the distance
583   --  parsed in Index.
584   --  Note: A RsaKey structure contains two parts,
585   --        one public and one private key.
586
587   procedure Rsa_Private_Key_Decode (Input : Byte_Array;
588                                     Index : in out Byte_Index;
589                                     Key   : in out RSA_Key_Type;
590                                     Size  : Integer;
591                                     Result : out Integer) with
592     Pre => Is_Valid (Key);
593   --  This function parses a DER-formatted RSA private key,
594   --  extracts the private key and stores it in the RsaKey structure
595   --  specified by the Key input argument. It also sets the distance
596   --  parsed in Index.
597   --  Note: A RsaKey structure contains two parts,
598   --        one public and one private key.
599
600   procedure Rsa_Set_RNG (Key    : in out Rsa_Key_Type;
601                          RNG    : in out RNG_Type;
602                          Result : out Integer);
603
604   procedure Rsa_SSL_Sign (Input  : Byte_Array;
605                           Output : in out Byte_Array;
606                           RSA    : in out RSA_Key_Type;
607                           RNG    : in out RNG_Type;
608                           Result : out Integer) with
609     Pre => Is_Valid (RSA) and Is_Valid (RNG);
610   --  The Output buffer must have the same size as the RSA key.
611   --  If successful Result = 0.
612   --  If Result < 0, then failure.
613   --  If Result > 0, then Success and is the size of the RSA key in bytes.
614
615   procedure Rsa_SSL_Verify (Input  : Byte_Array;
616                             Output : in out Byte_Array;
617                             RSA    : in out RSA_Key_Type;
618                             Result : out Integer) with
619     Pre => Is_Valid (RSA);
620   --  If Result < 0, then failure.
621   --  If Result > 0, then digital signature in Input
622   --                 successfully verified.
623
624   procedure RSA_Public_Encrypt (Input  : Byte_Array;
625                                 Output : in out Byte_Array;
626                                 Index  :    out Byte_Index;
627                                 RSA    : in out RSA_Key_Type;
628                                 RNG    : in out RNG_Type;
629                                 Result :    out Integer) with
630     Pre => Is_Valid (RSA);
631   --  This function encrypts a message from Input and stores the result
632   --  in Output. It requires an initialized public key and a random
633   --  number generator. As a side effect, this function will return
634   --  the bytes written to Output in Index.
635
636   procedure RSA_Private_Decrypt (Input  : Byte_Array;
637                                  Output : in out Byte_Array;
638                                  Index  :    out Byte_Index;
639                                  RSA    : in out RSA_Key_Type;
640                                  Result :    out Integer) with
641     Pre => Is_Valid (RSA);
642   --  This functions provides private RSA decryption.
643
644   type SHA256_Type is limited private with
645     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
646
647   function Is_Valid (SHA256 : SHA256_Type) return Boolean with
648      Annotate => (GNATprove, Ownership, "Needs_Reclamation");
649   --  Indicates if the SHA256 has successfully been initialized.
650   --  Annotation added for GNATprove ownership analysis.
651   --    https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
652
653   procedure Create_SHA256 (SHA256 : in out SHA256_Type;
654                            Result : out Integer) with
655     Pre  => not Is_Valid (SHA256),
656     Post => (if Result = 0 then Is_Valid (SHA256));
657   --  If successful Result = 0.
658
659   procedure Free_SHA256 (SHA256 : in out SHA256_Type) with
660     Pre  => Is_Valid (SHA256),
661     Post => not Is_Valid (SHA256);
662   --  Frees resources associated with SHA256 and releases the underlying C object.
663   --  If successful Result = 0.
664
665   procedure Update_SHA256 (SHA256 : in out SHA256_Type;
666                            Byte   : Byte_Array;
667                            Result : out Integer) with
668     Pre => Is_Valid (SHA256);
669   --  If successful Result = 0.
670
671   subtype SHA256_As_String is String (1 .. 64);
672
673   subtype SHA256_Hash is Byte_Array (1 .. 32);
674
675   procedure Finalize_SHA256 (SHA256 : in out SHA256_Type;
676                              Hash   : out SHA256_Hash;
677                              Result : out Integer) with
678     Pre => Is_Valid (SHA256);
679   --  If successful Result = 0.
680
681   type Device_Identifier is new Integer;
682
683   function Invalid_Device return Device_Identifier;
684
685   type AES_Type is limited private with
686     Annotate => (GNATprove, Ownership, "Needs_Reclamation");
687
688   function Is_Valid (AES : AES_Type) return Boolean with
689      Annotate => (GNATprove, Ownership, "Needs_Reclamation");
690   --  Indicates if the AES has successfully been initialized.
691   --  Annotation added for GNATprove ownership analysis.
692   --    https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
693
694   procedure Create_AES (Device : Device_Identifier;
695                         AES    : in out AES_Type;
696                         Result : out Integer) with
697     Pre  => not Is_Valid (AES),
698     Post => (if Result = 0 then Is_Valid (AES));
699   --  If successful Is_Valid (AES) = True, and Result = 0.
700
701   procedure AES_Free (AES : in out AES_Type;
702                       Result : out Integer) with
703     Pre  => Is_Valid (AES),
704     Post => (if Result = 0 then not Is_Valid (AES));
705   --  Frees resources associated with AES and releases the underlying C object.
706
707   procedure AES_Set_Key (AES    : AES_Type;
708                          Key    : Byte_Array;
709                          Length : Integer;
710                          IV     : Byte_Array;
711                          Dir    : Integer;
712                          Result : out Integer) with
713     Pre => Is_Valid (AES);
714
715   procedure AES_Set_IV (AES : AES_Type;
716                         IV  : Byte_Array;
717                         Result : out Integer) with
718     Pre => Is_Valid (AES);
719
720   procedure AES_Set_Cbc_Encrypt (AES : AES_Type;
721                                  Output : out Byte_Array;
722                                  Input : Byte_Array;
723                                  Size : Integer;
724                                  Result : out Integer) with
725     Pre => Is_Valid (AES);
726
727   procedure AES_Set_Cbc_Decrypt (AES : AES_Type;
728                                  Output : out Byte_Array;
729                                  Input : Byte_Array;
730                                  Size : Integer;
731                                  Result : out Integer) with
732     Pre => Is_Valid (AES);
733
734   --  (Removed duplicate AES_Free declaration)
735
736private
737   pragma SPARK_Mode (Off);
738
739   type chars_ptr is access all Character;
740   pragma Convention (C, chars_ptr);
741
742   pragma No_Strict_Aliasing (chars_ptr);
743   --  Since this type is used for external interfacing, with the pointer
744   --  coming from who knows where, it seems a good idea to turn off any
745   --  strict aliasing assumptions for this type.
746
747   subtype int is Interfaces.C.int; use type int;
748
749   type Opaque_Method  is limited null record;
750   type Opaque_Context is limited null record;
751   type Opaque_WolfSSL is limited null record;
752
753   --  Access-to-object types with convention C uses the same amount of
754   --  memory for storing pointers as is done in the C programming
755   --  language. The following access type definitions are used in
756   --  the Ada binding to the WolfSSL library:
757   type Context_Type is access Opaque_Context with Convention => C;
758   type Method_Type  is access Opaque_Method  with Convention => C;
759   type WolfSSL_Type is access Opaque_WolfSSL with Convention => C;
760
761   subtype Unsigned_32 is Interfaces.Unsigned_32; use type Unsigned_32;
762
763   type Mode_Type is new Unsigned_32;
764
765   --  The following imported subprograms are used to initialize
766   --  the constants defined in the public part of this package
767   --  specification. They cannot therefore be moved to the body
768   --  of this package.
769
770   function WolfSSL_Verify_None return int with
771     Convention    => C,
772     External_Name => "get_wolfssl_verify_none",
773     Import        => True;
774
775   function WolfSSL_Verify_Peer return int with
776     Convention    => C,
777     External_Name => "get_wolfssl_verify_peer",
778     Import        => True;
779
780   function WolfSSL_Verify_Fail_If_No_Peer_Cert return int with
781     Convention    => C,
782     External_Name => "get_wolfssl_verify_fail_if_no_peer_cert",
783     Import        => True;
784
785   function WolfSSL_Verify_Client_Once return int with
786     Convention    => C,
787     External_Name => "get_wolfssl_verify_client_once",
788     Import        => True;
789
790   function WolfSSL_Verify_Post_Handshake return int with
791     Convention    => C,
792     External_Name => "get_wolfssl_verify_post_handshake",
793     Import        => True;
794
795   function WolfSSL_Verify_Fail_Except_Psk return int with
796     Convention    => C,
797     External_Name => "get_wolfssl_verify_fail_except_psk",
798     Import        => True;
799
800   function WolfSSL_Verify_Default return int with
801     Convention    => C,
802     External_Name => "get_wolfssl_verify_default",
803     Import        => True;
804
805   pragma Warnings (Off, "pragma Restrictions (No_Exception_Propagation)");
806   --  The compiler may check for warnings related to no exception
807   --  propagation if this code is compiled with the Zero
808   --  Footprint run-time. The constants exposed here in the Ada binding
809   --  have valid values defined in the WolfSSL library but the compiler
810   --  cannot know this since the values become known during run-time.
811
812   Verify_None : constant Mode_Type := Mode_Type (WolfSSL_Verify_None);
813   Verify_Peer : constant Mode_Type := Mode_Type (WolfSSL_Verify_Peer);
814
815   Verify_Fail_If_No_Peer_Cert : constant Mode_Type :=
816     Mode_Type (WolfSSL_Verify_Fail_If_No_Peer_Cert);
817
818   Verify_Client_Once : constant Mode_Type :=
819     Mode_Type (WolfSSL_Verify_Client_Once);
820
821   Verify_Post_Handshake : constant Mode_Type :=
822     Mode_Type (WolfSSL_Verify_Post_Handshake);
823
824   Verify_Fail_Except_Psk : constant Mode_Type :=
825     Mode_Type (WolfSSL_Verify_Fail_Except_Psk);
826
827   Verify_Default : constant Mode_Type :=
828     Mode_Type (WolfSSL_Verify_Default);
829   pragma Warnings (On, "pragma Restrictions (No_Exception_Propagation)");
830
831   type File_Format is new Unsigned_32;
832
833   function WolfSSL_Filetype_Asn1 return int with
834     Convention    => C,
835     External_Name => "get_wolfssl_filetype_asn1",
836     Import        => True;
837
838   function WolfSSL_Filetype_Pem return int with
839     Convention    => C,
840     External_Name => "get_wolfssl_filetype_pem",
841     Import        => True;
842
843   function WolfSSL_Filetype_Default return int with
844     Convention    => C,
845     External_Name => "get_wolfssl_filetype_default",
846     Import        => True;
847
848   pragma Warnings (Off, "pragma Restrictions (No_Exception_Propagation)");
849   --  The compiler may check for warnings related to no exception
850   --  propagation if this code is compiled with the Zero
851   --  Footprint run-time. The constants exposed here in the Ada binding
852   --  have valid values defined in the WolfSSL library but the compiler
853   --  cannot know this since the values become known during run-time.
854   Format_Asn1 : constant File_Format :=
855     File_Format (WolfSSL_Filetype_Asn1);
856
857   Format_Pem : constant File_Format :=
858     File_Format (WolfSSL_Filetype_Pem);
859
860   Format_Default : constant File_Format :=
861     File_Format (WolfSSL_Filetype_Default);
862   pragma Warnings (On, "pragma Restrictions (No_Exception_Propagation)");
863
864   function Get_WolfSSL_Success return int with
865     Convention    => C,
866     External_Name => "get_wolfssl_success",
867     Import        => True;
868
869   function Get_WolfSSL_Failure return int with
870     Convention    => C,
871     External_Name => "get_wolfssl_failure",
872     Import        => True;
873
874   Success : constant Subprogram_Result :=
875      Subprogram_Result (Get_WolfSSL_Success);
876   --  Indicates success for some functions.
877   --  Do not use, unless you know what you do.
878
879   Failure : constant Subprogram_Result :=
880     Subprogram_Result (Get_WolfSSL_Failure);
881
882   function Get_WolfSSL_Error_Want_Read return int with
883     Convention    => C,
884     External_Name => "get_wolfssl_error_want_read",
885     Import        => True;
886
887   function Get_WolfSSL_Error_Want_Write return int with
888     Convention    => C,
889     External_Name => "get_wolfssl_error_want_write",
890     Import        => True;
891
892   Error_Want_Read  : constant Error_Code :=
893      Error_Code (Get_WolfSSL_Error_Want_Read);
894
895   Error_Want_Write : constant Error_Code :=
896     Error_Code (Get_WolfSSL_Error_Want_Write);
897
898   type Opaque_RNG is limited null record;
899   type RNG_Type is access Opaque_RNG with Convention => C;
900
901   type Opaque_RSA is limited null record;
902   type RSA_Key_Type is access Opaque_RSA with Convention => C;
903
904   type Opaque_Sha256 is limited null record;
905   type SHA256_Type is access Opaque_Sha256 with Convention => C;
906
907   type Opaque_AES is limited null record;
908   type AES_Type is access Opaque_AES with Convention => C;
909
910end WolfSSL;