hkdf_ada

SPARK-proved HKDF (RFC 5869) implementation in Ada/SPARK.

264/264 SPARK checks proved, 0 assumptions, 0 warnings, Level 2.

Proof scope

Package	SPARK status
HKDF_SHA256	100% proved at Level 2 (84 checks, 0 pragma Assume)
HKDF (generic)	SPARK_Mode (Off) -- unproved convenience layer

The generic HKDF package cannot be analyzed by gnatprove because generic formal subprograms have no contracts. Use the concrete HKDF_SHA256 package when formal verification is required. The generic is provided for use with other hash functions where SPARK proof is not needed.

Features

• HKDF Extract + Expand per RFC 5869
• HKDF-SHA-256 concrete instantiation, 100% SPARK Level 2 proved
• Generic HKDF package for other HMAC functions
• No heap allocation -- pragma Pure, all stack-bounded
• Passes all RFC 5869 Appendix A SHA-256 test vectors
• Boundary-tested: OKM lengths 1, 32, 33, and 8160 (max)

Installation

alr with hkdf_ada

Or add to your alire.toml:

[[depends-on]]
hkdf_ada = "~0.1.0"

Dependencies

• hmac_ada -- SPARK-proved HMAC-SHA-256

Usage

with System.Storage_Elements;  use System.Storage_Elements;
with HKDF_SHA256;

procedure Example is
   IKM  : constant Storage_Array := ...;  --  input keying material
   Salt : constant Storage_Array := ...;  --  optional salt
   Info : constant Storage_Array := ...;  --  context info

   PRK : HKDF_SHA256.PRK_Type;
   OKM : Storage_Array (1 .. 32);         --  desired output length
begin
   --  Extract: PRK = HMAC-SHA-256(salt, IKM)
   HKDF_SHA256.Extract (Salt, IKM, PRK);

   --  Expand: OKM = HKDF-Expand(PRK, info, L)
   HKDF_SHA256.Expand (PRK, Info, OKM);
end Example;

HKDF_SHA256.Byte_Array is provided as a library-level alias for System.Storage_Elements.Storage_Array if you prefer not to with System.Storage_Elements directly.

Build

alr build

Test

Tests live in the nested tests/ crate, which depends on the top-level crate via a local path pin. This keeps the published crate free of dev-only dependencies (gnatprove).

cd tests

# Linux
alr build
./obj/test_hkdf

# macOS
alr build -- -XSDK=macos -XSDK_LIB="$(xcrun --show-sdk-path)/usr/lib"
./obj/test_hkdf

SPARK proof

cd tests
alr exec -- gnatprove -P ../hkdf_ada.gpr -j0 --level=2 --timeout=120

Security notes

• This package inherits the security properties of hmac_ada (constant-time comparison, secure key wipe). See the hmac_ada documentation for details.
• HKDF is a key derivation function, not an encryption primitive. It assumes the input keying material has sufficient entropy.
• The generic HKDF package is not SPARK-proved. Do not use it in safety-critical paths without additional review.

License

Apache-2.0