wolfSSL/wolfssl
1
0
Fork 1
mirror of https://github.com/wolfSSL/wolfssl.git synced 2026-07-06 00:30:49 +02:00
Code Issues Packages Projects Releases Wiki Activity
Files
2c030ddb0dd7b40904bd571a052d64a18d32df4e
wolfssl/wrapper/Ada/wolfssl.ads
T
JacobBarthelmeh a156ed7bc7 update Copyright year
2026-02-18 09:52:21 -07:00

911 lines
41 KiB
Ada
Raw Blame History

-- wolfssl.ads
--
-- Copyright (C) 2006-2026 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 3 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;
-- This package is annotated "with SPARK_Mode" that SPARK can verify
-- the API of this package is used correctly.
package WolfSSL with SPARK_Mode is
type Subprogram_Result is new Integer;
Success : constant Subprogram_Result;
-- Indicates success for some functions.
-- Do not use, unless you know what you do.
Failure : constant Subprogram_Result;
-- Indicates failure for some functions.
-- Do not use, unless you know what you do.
Exception_Error : constant := -1234567;
-- Indicates an exception was raised during a subprogram call.
function Initialize return Subprogram_Result;
-- Initializes the wolfSSL library for use. Must be called once per
-- application and before any other call to the library.
function Finalize return Subprogram_Result;
-- Un-initializes the wolfSSL library from further use.
-- Doesn't have to be called, though it will free any resources
-- used by the library.
subtype unsigned is Interfaces.C.unsigned;
subtype Byte_Type is Interfaces.C.char;
subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000;
subtype Byte_Array is Interfaces.C.char_array;
use type Interfaces.C.size_t;
type Context_Type is limited private with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Instances of this type are called SSL Contexts.
function Is_Valid (Context : Context_Type) return Boolean with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Indicates if the SSL Context has successfully been initialized.
-- If initialized, the SSL Context has allocated resources
-- that needs to be deallocated before application exit.
-- Annotation added for GNATprove ownership analysis.
-- https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
type Method_Type is limited private with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
function Is_Valid (Method : Method_Type) return Boolean with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Annotation added for GNATprove ownership analysis.
-- https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
function TLSv1_2_Server_Method return Method_Type;
-- This function is used to indicate that the application is a server
-- and will only support the TLS 1.2 protocol.
function TLSv1_2_Client_Method return Method_Type;
-- This function is used to indicate that the application is a client
-- and will only support the TLS 1.2 protocol.
function TLSv1_3_Server_Method return Method_Type;
-- This function is used to indicate that the application is a server
-- and will only support the TLS 1.3 protocol.
function TLSv1_3_Client_Method return Method_Type;
-- This function is used to indicate that the application is a client
-- and will only support the TLS 1.3 protocol.
function DTLSv1_2_Server_Method return Method_Type;
-- This function is used to indicate that the application is a server
-- and will only support the DTLS 1.2 protocol.
function DTLSv1_2_Client_Method return Method_Type;
-- This function is used to indicate that the application is a client
-- and will only support the DTLS 1.2 protocol.
function DTLSv1_3_Server_Method return Method_Type;
-- This function is used to indicate that the application is a server
-- and will only support the DTLS 1.3 protocol.
function DTLSv1_3_Client_Method return Method_Type;
-- This function is used to indicate that the application is a client
-- and will only support the DTLS 1.3 protocol.
procedure Create_Context (Method : in out Method_Type;
Context : out Context_Type) with
Post => not Is_Valid (Method);
-- This function creates a new SSL context, taking a desired SSL/TLS
-- protocol method for input.
-- If successful Is_Valid (Context) = True, otherwise False.
-- The Method is consumed by this operation and set to null.
procedure Free (Context : in out Context_Type) with
Post => not Is_Valid (Context);
-- This function frees an allocated SSL Context object.
-- If Context is not valid, this is a no-op.
type Mode_Type is private;
function "or" (Left, Right : Mode_Type) return Mode_Type;
Verify_None : constant Mode_Type;
-- Client mode: the client will not verify the certificate received
-- from the server and the handshake will continue as normal.
--
-- Server mode: the server will not send a certificate request to
-- the client. As such, client verification will not be enabled.
Verify_Peer : constant Mode_Type;
-- Client mode: the client will verify the certificate received from
-- the server during the handshake. This is turned on by default
-- in wolfSSL, therefore, using this option has no effect.
--
-- Server mode: the server will send a certificate request to
-- the client and verify the client certificate received.
Verify_Fail_If_No_Peer_Cert : constant Mode_Type;
-- Client mode: no effect when used on the client side.
--
-- Server mode: the verification will fail on the server side if
-- the client fails to send a certificate when requested to do so
-- (when using Verify_Peer on the SSL server).
Verify_Client_Once : constant Mode_Type;
Verify_Post_Handshake : constant Mode_Type;
Verify_Fail_Except_Psk : constant Mode_Type;
-- Client mode: no effect when used on the client side.
--
-- Server mode: the verification is the same as
-- Verify_Fail_If_No_Peer_Cert except in the case of a PSK connection.
-- If a PSK connection is being made then the connection
-- will go through without a peer cert.
Verify_Default : constant Mode_Type;
procedure Set_Verify (Context : Context_Type;
Mode : Mode_Type) with
Pre => Is_Valid (Context);
-- This function sets the verification method for remote peers
function Get_Verify (Context : Context_Type) return Mode_Type;
type File_Format is private;
Format_Asn1 : constant File_Format;
Format_Pem : constant File_Format;
Format_Default : constant File_Format;
function Use_Certificate_File (Context : Context_Type;
File : String;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Context);
-- This function loads a certificate file into the SSL context.
-- The file is provided by the file argument. The format argument
-- specifies the format type of the file, either ASN1 or
-- PEM file types. Please see the examples for proper usage.
function Use_Certificate_Buffer (Context : Context_Type;
Input : Byte_Array;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Context);
-- This function loads a certificate buffer into the SSL Context.
-- It behaves like the non-buffered version (Use_Certificate_File),
-- only differing in its ability to be called with a buffer as input
-- instead of a file. The buffer is provided by the Input argument.
-- Format specifies the format type of the buffer; ASN1 or PEM.
-- Please see the examples for proper usage.
function Use_Private_Key_File (Context : Context_Type;
File : String;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Context);
-- This function loads a private key file into the SSL context.
-- The file is provided by the File argument. The Format argument
-- specifies the format type of the file - ASN1 or PEM.
-- Please see the examples for proper usage.
function Use_Private_Key_Buffer (Context : Context_Type;
Input : Byte_Array;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Context);
-- This function loads a private key buffer into the SSL Context.
-- It behaves like the non-buffered version (Use_Private_Key_File),
-- only differing in its ability to be called with a buffer as input
-- instead of a file. The buffer is provided by the Input argument.
-- Format specifies the format type of the buffer; ASN1 or PEM.
-- Please see the examples for proper usage.
function Load_Verify_Locations (Context : Context_Type;
File : String;
Path : String)
return Subprogram_Result with
Pre => Is_Valid (Context);
-- This function loads PEM-formatted CA certificate files into
-- the SSL context. These certificates will be treated as trusted
-- root certificates and used to verify certs received from peers
-- during the SSL handshake. The root certificate file,
-- provided by the File argument, may be a single certificate or
-- a file containing multiple certificates. If multiple CA certs
-- are included in the same file, wolfSSL will load them in the same
-- order they are presented in the file. The path argument is
-- a pointer to the name of a directory that contains certificates
-- of trusted root CAs. If the value of File is not empty "",
-- path may be specified as "" if not needed. If path is specified
-- and NO_WOLFSSL_DIR was not defined when building the library,
-- wolfSSL will load all CA certificates located in the given
-- directory. This function will attempt to load all files in
-- the directory. This function expects PEM formatted CERT_TYPE file
-- with header "--BEGIN CERTIFICATE--".
function Load_Verify_Buffer (Context : Context_Type;
Input : Byte_Array;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Context);
-- This function loads a CA certificate buffer into the SSL
-- Context. It behaves like the non-buffered version, only differing
-- in its ability to be called with a buffer as input instead of
-- a file. The buffer is provided by the Input argument.
-- Format specifies the format type of the buffer; ASN1 or PEM.
-- More than one CA certificate may be loaded
-- per buffer as long as the format is in PEM.
-- Please see the examples for proper usage.
type WolfSSL_Type is limited private with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Instances of this type are called SSL Sessions.
function Is_Valid (Ssl : WolfSSL_Type) return Boolean with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Indicates if the SSL Session has successfully been initialized.
-- If initialized, the SSL Session has allocated resources
-- that needs to be deallocated before application exit.
-- Annotation added for GNATprove ownership analysis.
-- https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
procedure Create_WolfSSL (Context : Context_Type;
Ssl : out WolfSSL_Type) with
Pre => Is_Valid (Context);
-- This function creates a new SSL session, taking an already created
-- SSL context as input.
-- If successful Is_Valid (Ssl) = True, otherwise False.
function Use_Certificate_File (Ssl : WolfSSL_Type;
File : String;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- This function loads a certificate file into the SSL session.
-- The certificate file is provided by the file argument.
-- The format argument specifies the format type of the file
-- either ASN1 or PEM.
function Use_Certificate_Buffer (Ssl : WolfSSL_Type;
Input : Byte_Array;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- This function loads a certificate buffer into the SSL session
-- object. It behaves like the non-buffered version, only differing
-- in its ability to be called with a buffer as input instead
-- of a file. The buffer is provided by the Input argument.
-- Format specifies the format type of the buffer; ASN1 or PEM.
-- Please see the examples for proper usage.
function Use_Private_Key_File (Ssl : WolfSSL_Type;
File : String;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- This function loads a private key file into the SSL session.
-- The key file is provided by the File argument. The Format argument
-- specifies the format type of the file - ASN1 or PEM.
function Use_Private_Key_Buffer (Ssl : WolfSSL_Type;
Input : Byte_Array;
Format : File_Format)
return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- This function loads a private key buffer into the SSL session
-- object. It behaves like the non-buffered version, only differing
-- in its ability to be called with a buffer as input instead
-- of a file. The buffer is provided by the Input argument.
-- Format specifies the format type of the buffer; ASN1 or PEM.
-- Please see the examples for proper usage.
function Attach (Ssl : WolfSSL_Type;
Socket : Integer)
return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- Attach wolfSSL to the socket.
--
-- This function assigns a file descriptor (Socket) as
-- the input/output facility for the SSL connection.
-- Typically this will be a socket file descriptor.
procedure Keep_Arrays (Ssl : WolfSSL_Type) with
Pre => Is_Valid (Ssl);
-- Normally, at the end of the SSL handshake, wolfSSL frees
-- temporary arrays. Calling this function before the handshake
-- begins will prevent wolfSSL from freeing temporary arrays.
-- Temporary arrays may be needed for things such as
-- wolfSSL_get_keys() or PSK hints. When the user is done with
-- temporary arrays, either Free_Arrays(..) may be called to free
-- the resources immediately, or alternatively the resources will
-- be freed when the associated SSL object is freed.
procedure Free_Arrays (Ssl : WolfSSL_Type) with
Pre => Is_Valid (Ssl);
-- Normally, at the end of the SSL handshake, wolfSSL frees temporary
-- arrays. If Keep_Arrays(..) has been called before the handshake,
-- wolfSSL will not free temporary arrays. This function explicitly
-- frees temporary arrays and should be called when the user is done
-- with temporary arrays and does not want to wait for the SSL object
-- to be freed to free these resources.
function Accept_Connection (Ssl : WolfSSL_Type)
return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- The name of this function is not Accept (..) because the word
-- "accept" is a reserved keyword in the Ada language.
--
-- This function is called on the server side and waits for an
-- SSL client to initiate the SSL/TLS handshake. When this function
-- is called, the underlying communication channel has already been
-- set up. This function works with both blocking and
-- non-blocking I/O. When the underlying I/O is non-blocking,
-- Accept_Connection (..) will return when the underlying I/O could
-- not satisfy the needs of Accept_Connection (..) to continue
-- the handshake. In this case, a call to Get_Error(..) will
-- yield either Error_Want_Read or Error_Want_Write.
-- The calling process must then repeat the call to
-- Accept_Connection (..) when data is available to read and
-- wolfSSL will pick up where it left off. When using a
-- non_blocking socket, nothing needs to be done, but select() can
-- be used to check for the required condition.
-- If the underlying I/O is blocking, Accept_Connection (..) will
-- only return once the handshake has been finished or
-- an error occurred.
-- This record type has discriminants with default values to be able
-- to compile this code under the restriction No Secondary Stack.
type Read_Result (Success : Boolean := False;
Last : Byte_Index := Byte_Index'Last) is record
case Success is
when True => Buffer : Byte_Array (1 .. Last);
when False => Code : Subprogram_Result; -- Error code
end case;
end record;
procedure Read (Ssl : WolfSSL_Type;
Result : out Read_Result) with
Pre => Is_Valid (Ssl);
-- This function reads a number of bytes from the SSL session (ssl)
-- internal read buffer into the buffer data. The bytes read are
-- removed from the internal receive buffer.
-- If necessary Read(..) will negotiate an SSL/TLS session
-- if the handshake has not already
-- been performed yet by Connect(..) or Accept_Connection (..).
-- The SSL/TLS protocol uses SSL records which have a maximum size
-- of 16kB (the max record size can be controlled by the
-- MAX_RECORD_SIZE define in /wolfssl/internal.h). As such, wolfSSL
-- needs to read an entire SSL record internally before it is able
-- to process and decrypt the record. Because of this, a call to
-- Read(..) will only be able to return the maximum buffer
-- size which has been decrypted at the time of calling. There may
-- be additional not-yet-decrypted data waiting in the internal
-- wolfSSL receive buffer which will be retrieved and decrypted with
-- the next call to Read(..).
-- This record type has discriminants with default values to be able
-- to compile this code under the restriction No Secondary Stack.
type Write_Result (Success : Boolean := False) is record
case Success is
when True => Bytes_Written : Byte_Index;
when False => Code : Subprogram_Result; -- Error code
end case;
end record;
procedure Write (Ssl : WolfSSL_Type;
Data : Byte_Array;
Result : out Write_Result) with
Pre => Is_Valid (Ssl);
-- The number of bytes written is returned.
-- This function writes bytes from the buffer, Data,
-- to the SSL connection, ssl. If necessary, Write(..) will
-- negotiate an SSL/TLS session if the handshake has not already
-- been performed yet by Connect(..) or Accept_Connection(..).
-- Write(..) works with both blocking and non-blocking I/O.
-- When the underlying I/O is non-blocking, Write(..) will return
-- when the underlying I/O could not satisfy the needs of Write(..)
-- to continue. In this case, a call to Get_Error(..) will
-- yield either Error_Want_Read or Error_Want_Write.
-- The calling process must then repeat the call to Write(..)
-- when the underlying I/O is ready. If the underlying I/O is
-- blocking, Write(..) will only return once the buffer data
-- has been completely written or an error occurred.
function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- This function shuts down an active SSL/TLS connection using
-- the SSL session, ssl. This function will try to send a
-- "close notify" alert to the peer. The calling application can
-- choose to wait for the peer to send its "close notify" alert
-- in response or just go ahead and shut down the underlying
-- connection after directly calling wolfSSL_shutdown (to save
-- resources). Either option is allowed by the TLS specification.
-- If the underlying connection will be used again in the future,
-- the complete two_directional shutdown procedure must be performed
-- to keep synchronization intact between the peers.
-- Shutdown(..) works with both blocking and non_blocking I/O.
-- When the underlying I/O is non_blocking, Shutdown(..) will
-- return an error if the underlying I/O could not satisfy the needs
-- of Shutdown(..) to continue. In this case, a call to
-- Get_Error(..) will yield either Error_Want_Read or
-- Error_Want_Write. The calling process must then repeat
-- the call to Shutdown() when the underlying I/O is ready.
procedure Free (Ssl : in out WolfSSL_Type) with
Post => not Is_Valid (Ssl);
-- Frees the resources allocated by the SSL session object.
-- If Ssl is not valid, this is a no-op.
function Connect (Ssl : WolfSSL_Type) return Subprogram_Result with
Pre => Is_Valid (Ssl);
-- This function is called on the client side and initiates
-- an SSL/TLS handshake with a server. When this function is called,
-- the underlying communication channel has already been set up.
-- Connect(..) works with both blocking and non_blocking I/O.
-- When the underlying I/O is non_blocking, Connect(..) will
-- return when the underlying I/O could not satisfy the needs
-- of wolfSSL_connect to continue the handshake. In this case,
-- a call to Get_Error(..) will yield either
-- Error_Want_Read or SSL_ERROR_WANT_WRITE. The calling process
-- must then repeat the call to Connect(..) when
-- the underlying I/O is ready and wolfSSL will pick up where
-- it left off. When using a non_blocking socket, nothing needs
-- to be done, but select() can be used to check for the required
-- condition. If the underlying I/O is blocking, Connect(..)
-- will only return once the handshake has been finished or an error
-- occurred. wolfSSL takes a different approach to certificate
-- verification than OpenSSL does. The default policy for the client
-- is to verify the server, this means that if you don't load CAs
-- to verify the server you'll get a connect error,
-- unable to verify. It you want to mimic OpenSSL behavior
-- of having SSL_connect succeed even if verifying the server fails
-- and reducing security you can do this by calling:
-- Set_Verify (Ctx, Verify_None, 0); before calling
-- Create_WolfSSL(...); Though it's not recommended.
type Error_Code is new Integer;
Error_Want_Read : constant Error_Code;
Error_Want_Write : constant Error_Code;
function Get_Error (Ssl : WolfSSL_Type;
Result : Subprogram_Result) return Error_Code;
-- This function returns a unique error code describing why
-- the previous API function call (Connect, Accept_Connection,
-- Read, Write, etc.) resulted in an error return code.
-- After Get_Error is called and returns the unique error code,
-- wolfSSL_ERR_error_string() may be called to get a human readable
-- error string.
subtype Error_Message_Index is Natural range 0 .. 80;
-- The default error message length is 80 in WolfSSL unless
-- configured to another value. See the result
-- of the Max_Error_Size function.
type Error_Message (Last : Error_Message_Index := 0) is record
Text : String (1 .. Last);
end record;
procedure Error (Code : in Error_Code;
Message : in out Error_Message);
-- This function converts an error code returned by Get_Error(..)
-- into a more human readable error string. Code is the error code
-- returned by Get_error(). The maximum length of error strings is
-- 80 characters by default, as defined by MAX_ERROR_SZ
-- is wolfssl/wolfcrypt/error.h.
--
-- If Message has not been updated with a text, it may be because
-- an exception was raised during the execution of the subprogram.
function Max_Error_Size return Natural;
-- Returns the value of the defined MAX_ERROR_SZ integer
-- in wolfssl/wolfcrypt/error.h.
type RNG_Type is limited private with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
function Is_Valid (Key : RNG_Type) return Boolean with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Indicates if the RNG has successfully been initialized.
-- Annotation added for GNATprove ownership analysis.
-- https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
procedure Create_RNG (Key : in out RNG_Type;
Result : out Integer) with
Pre => not Is_Valid (Key),
Post => (if Result = 0 then Is_Valid (Key));
-- If successful Result = 0.
procedure Free_RNG (Key : in out RNG_Type) with
Pre => Is_Valid (Key),
Post => not Is_Valid (Key);
-- Frees resources associated with RNG and releases the underlying C object.
procedure RNG_Generate_Block (RNG : RNG_Type;
Output : out Byte_Array;
Result : out Integer) with
Pre => Is_Valid (RNG);
type HMAC_Hash is (MD5, SHA, SHA256, SHA384, SHA512, SHA3_224,
SHA3_256, SHA3_384, SHA3_512);
procedure PBKDF2 (Output : out Byte_Array;
Password : Byte_Array;
Salt : Byte_Array;
Iterations : Positive;
Key_Length : Positive;
HMAC : HMAC_Hash;
Result : out Integer);
type RSA_Key_Type is limited private with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
function Is_Valid (Key : RSA_Key_Type) return Boolean with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Indicates if the RSA has successfully been initialized.
-- Annotation added for GNATprove ownership analysis.
-- https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
procedure Create_RSA (Key : in out RSA_Key_Type;
Result : out Integer) with
Pre => not Is_Valid (Key),
Post => (if Result = 0 then Is_Valid (Key));
-- If successful Result = 0.
procedure Free_RSA (Key : in out RSA_Key_Type) with
Pre => Is_Valid (Key),
Post => not Is_Valid (Key);
-- Frees resources associated with RSA and releases the underlying C object.
procedure Rsa_Public_Key_Decode (Input : Byte_Array;
Index : in out Byte_Index;
Key : in out RSA_Key_Type;
Size : Integer;
Result : out Integer) with
Pre => Is_Valid (Key);
-- This function parses a DER-formatted RSA public key,
-- extracts the public key and stores it in the RsaKey structure
-- specified by the Key input argument. It also sets the distance
-- parsed in Index.
-- Note: A RsaKey structure contains two parts,
-- one public and one private key.
procedure Rsa_Private_Key_Decode (Input : Byte_Array;
Index : in out Byte_Index;
Key : in out RSA_Key_Type;
Size : Integer;
Result : out Integer) with
Pre => Is_Valid (Key);
-- This function parses a DER-formatted RSA private key,
-- extracts the private key and stores it in the RsaKey structure
-- specified by the Key input argument. It also sets the distance
-- parsed in Index.
-- Note: A RsaKey structure contains two parts,
-- one public and one private key.
procedure Rsa_Set_RNG (Key : in out Rsa_Key_Type;
RNG : in out RNG_Type;
Result : out Integer);
procedure Rsa_SSL_Sign (Input : Byte_Array;
Output : in out Byte_Array;
RSA : in out RSA_Key_Type;
RNG : in out RNG_Type;
Result : out Integer) with
Pre => Is_Valid (RSA) and Is_Valid (RNG);
-- The Output buffer must have the same size as the RSA key.
-- If successful Result = 0.
-- If Result < 0, then failure.
-- If Result > 0, then Success and is the size of the RSA key in bytes.
procedure Rsa_SSL_Verify (Input : Byte_Array;
Output : in out Byte_Array;
RSA : in out RSA_Key_Type;
Result : out Integer) with
Pre => Is_Valid (RSA);
-- If Result < 0, then failure.
-- If Result > 0, then digital signature in Input
-- successfully verified.
procedure RSA_Public_Encrypt (Input : Byte_Array;
Output : in out Byte_Array;
Index : out Byte_Index;
RSA : in out RSA_Key_Type;
RNG : in out RNG_Type;
Result : out Integer) with
Pre => Is_Valid (RSA);
-- This function encrypts a message from Input and stores the result
-- in Output. It requires an initialized public key and a random
-- number generator. As a side effect, this function will return
-- the bytes written to Output in Index.
procedure RSA_Private_Decrypt (Input : Byte_Array;
Output : in out Byte_Array;
Index : out Byte_Index;
RSA : in out RSA_Key_Type;
Result : out Integer) with
Pre => Is_Valid (RSA);
-- This functions provides private RSA decryption.
type SHA256_Type is limited private with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
function Is_Valid (SHA256 : SHA256_Type) return Boolean with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Indicates if the SHA256 has successfully been initialized.
-- Annotation added for GNATprove ownership analysis.
-- https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
procedure Create_SHA256 (SHA256 : in out SHA256_Type;
Result : out Integer) with
Pre => not Is_Valid (SHA256),
Post => (if Result = 0 then Is_Valid (SHA256));
-- If successful Result = 0.
procedure Free_SHA256 (SHA256 : in out SHA256_Type) with
Pre => Is_Valid (SHA256),
Post => not Is_Valid (SHA256);
-- Frees resources associated with SHA256 and releases the underlying C object.
-- If successful Result = 0.
procedure Update_SHA256 (SHA256 : in out SHA256_Type;
Byte : Byte_Array;
Result : out Integer) with
Pre => Is_Valid (SHA256);
-- If successful Result = 0.
subtype SHA256_As_String is String (1 .. 64);
subtype SHA256_Hash is Byte_Array (1 .. 32);
procedure Finalize_SHA256 (SHA256 : in out SHA256_Type;
Hash : out SHA256_Hash;
Result : out Integer) with
Pre => Is_Valid (SHA256);
-- If successful Result = 0.
type Device_Identifier is new Integer;
function Invalid_Device return Device_Identifier;
type AES_Type is limited private with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
function Is_Valid (AES : AES_Type) return Boolean with
Annotate => (GNATprove, Ownership, "Needs_Reclamation");
-- Indicates if the AES has successfully been initialized.
-- Annotation added for GNATprove ownership analysis.
-- https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/additional_annotate_pragmas.html#annotation-for-enforcing-ownership-checking-on-a-private-type
procedure Create_AES (Device : Device_Identifier;
AES : in out AES_Type;
Result : out Integer) with
Pre => not Is_Valid (AES),
Post => (if Result = 0 then Is_Valid (AES));
-- If successful Is_Valid (AES) = True, and Result = 0.
procedure AES_Free (AES : in out AES_Type;
Result : out Integer) with
Pre => Is_Valid (AES),
Post => (if Result = 0 then not Is_Valid (AES));
-- Frees resources associated with AES and releases the underlying C object.
procedure AES_Set_Key (AES : AES_Type;
Key : Byte_Array;
Length : Integer;
IV : Byte_Array;
Dir : Integer;
Result : out Integer) with
Pre => Is_Valid (AES);
procedure AES_Set_IV (AES : AES_Type;
IV : Byte_Array;
Result : out Integer) with
Pre => Is_Valid (AES);
procedure AES_Set_Cbc_Encrypt (AES : AES_Type;
Output : out Byte_Array;
Input : Byte_Array;
Size : Integer;
Result : out Integer) with
Pre => Is_Valid (AES);
procedure AES_Set_Cbc_Decrypt (AES : AES_Type;
Output : out Byte_Array;
Input : Byte_Array;
Size : Integer;
Result : out Integer) with
Pre => Is_Valid (AES);
-- (Removed duplicate AES_Free declaration)
private
pragma SPARK_Mode (Off);
type chars_ptr is access all Character;
pragma Convention (C, chars_ptr);
pragma No_Strict_Aliasing (chars_ptr);
-- Since this type is used for external interfacing, with the pointer
-- coming from who knows where, it seems a good idea to turn off any
-- strict aliasing assumptions for this type.
subtype int is Interfaces.C.int; use type int;
type Opaque_Method is limited null record;
type Opaque_Context is limited null record;
type Opaque_WolfSSL is limited null record;
-- Access-to-object types with convention C uses the same amount of
-- memory for storing pointers as is done in the C programming
-- language. The following access type definitions are used in
-- the Ada binding to the WolfSSL library:
type Context_Type is access Opaque_Context with Convention => C;
type Method_Type is access Opaque_Method with Convention => C;
type WolfSSL_Type is access Opaque_WolfSSL with Convention => C;
subtype Unsigned_32 is Interfaces.Unsigned_32; use type Unsigned_32;
type Mode_Type is new Unsigned_32;
-- The following imported subprograms are used to initialize
-- the constants defined in the public part of this package
-- specification. They cannot therefore be moved to the body
-- of this package.
function WolfSSL_Verify_None return int with
Convention => C,
External_Name => "get_wolfssl_verify_none",
Import => True;
function WolfSSL_Verify_Peer return int with
Convention => C,
External_Name => "get_wolfssl_verify_peer",
Import => True;
function WolfSSL_Verify_Fail_If_No_Peer_Cert return int with
Convention => C,
External_Name => "get_wolfssl_verify_fail_if_no_peer_cert",
Import => True;
function WolfSSL_Verify_Client_Once return int with
Convention => C,
External_Name => "get_wolfssl_verify_client_once",
Import => True;
function WolfSSL_Verify_Post_Handshake return int with
Convention => C,
External_Name => "get_wolfssl_verify_post_handshake",
Import => True;
function WolfSSL_Verify_Fail_Except_Psk return int with
Convention => C,
External_Name => "get_wolfssl_verify_fail_except_psk",
Import => True;
function WolfSSL_Verify_Default return int with
Convention => C,
External_Name => "get_wolfssl_verify_default",
Import => True;
pragma Warnings (Off, "pragma Restrictions (No_Exception_Propagation)");
-- The compiler may check for warnings related to no exception
-- propagation if this code is compiled with the Zero
-- Footprint run-time. The constants exposed here in the Ada binding
-- have valid values defined in the WolfSSL library but the compiler
-- cannot know this since the values become known during run-time.
Verify_None : constant Mode_Type := Mode_Type (WolfSSL_Verify_None);
Verify_Peer : constant Mode_Type := Mode_Type (WolfSSL_Verify_Peer);
Verify_Fail_If_No_Peer_Cert : constant Mode_Type :=
Mode_Type (WolfSSL_Verify_Fail_If_No_Peer_Cert);
Verify_Client_Once : constant Mode_Type :=
Mode_Type (WolfSSL_Verify_Client_Once);
Verify_Post_Handshake : constant Mode_Type :=
Mode_Type (WolfSSL_Verify_Post_Handshake);
Verify_Fail_Except_Psk : constant Mode_Type :=
Mode_Type (WolfSSL_Verify_Fail_Except_Psk);
Verify_Default : constant Mode_Type :=
Mode_Type (WolfSSL_Verify_Default);
pragma Warnings (On, "pragma Restrictions (No_Exception_Propagation)");
type File_Format is new Unsigned_32;
function WolfSSL_Filetype_Asn1 return int with
Convention => C,
External_Name => "get_wolfssl_filetype_asn1",
Import => True;
function WolfSSL_Filetype_Pem return int with
Convention => C,
External_Name => "get_wolfssl_filetype_pem",
Import => True;
function WolfSSL_Filetype_Default return int with
Convention => C,
External_Name => "get_wolfssl_filetype_default",
Import => True;
pragma Warnings (Off, "pragma Restrictions (No_Exception_Propagation)");
-- The compiler may check for warnings related to no exception
-- propagation if this code is compiled with the Zero
-- Footprint run-time. The constants exposed here in the Ada binding
-- have valid values defined in the WolfSSL library but the compiler
-- cannot know this since the values become known during run-time.
Format_Asn1 : constant File_Format :=
File_Format (WolfSSL_Filetype_Asn1);
Format_Pem : constant File_Format :=
File_Format (WolfSSL_Filetype_Pem);
Format_Default : constant File_Format :=
File_Format (WolfSSL_Filetype_Default);
pragma Warnings (On, "pragma Restrictions (No_Exception_Propagation)");
function Get_WolfSSL_Success return int with
Convention => C,
External_Name => "get_wolfssl_success",
Import => True;
function Get_WolfSSL_Failure return int with
Convention => C,
External_Name => "get_wolfssl_failure",
Import => True;
Success : constant Subprogram_Result :=
Subprogram_Result (Get_WolfSSL_Success);
-- Indicates success for some functions.
-- Do not use, unless you know what you do.
Failure : constant Subprogram_Result :=
Subprogram_Result (Get_WolfSSL_Failure);
function Get_WolfSSL_Error_Want_Read return int with
Convention => C,
External_Name => "get_wolfssl_error_want_read",
Import => True;
function Get_WolfSSL_Error_Want_Write return int with
Convention => C,
External_Name => "get_wolfssl_error_want_write",
Import => True;
Error_Want_Read : constant Error_Code :=
Error_Code (Get_WolfSSL_Error_Want_Read);
Error_Want_Write : constant Error_Code :=
Error_Code (Get_WolfSSL_Error_Want_Write);
type Opaque_RNG is limited null record;
type RNG_Type is access Opaque_RNG with Convention => C;
type Opaque_RSA is limited null record;
type RSA_Key_Type is access Opaque_RSA with Convention => C;
type Opaque_Sha256 is limited null record;
type SHA256_Type is access Opaque_Sha256 with Convention => C;
type Opaque_AES is limited null record;
type AES_Type is access Opaque_AES with Convention => C;
end WolfSSL;
Reference in New Issue View Git Blame Copy Permalink