Library for the AES-CBC en/decryption of 4K blocks

The 'aes_cbc_4k' library is simple wrapper around libsparkcrypto to
serve as a backend for storage encryption. It operates on data chunks of
4 KiB and uses AES-CBC while incorporating the block number and the
private key as salt values.

repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb

@@ -0,0 +1,91 @@
+pragma Ada_2012;
+
+with LSC.AES_Generic.CBC;
+with LSC.SHA2_Generic;
+with Ada.Unchecked_Conversion;
+
+package body Aes_Cbc_4k with SPARK_Mode
+is
+   function Init_IV (Key : Key_Type; Block_Number : Block_Number_Type)
+      return Ciphertext_Base_Type
+      with post => Init_IV'Result'Length = 16;
+
+   function Init_IV (Key : Key_Type; Block_Number : Block_Number_Type)
+      return Ciphertext_Base_Type
+   is
+
+      type IV_Key_Base_Type is array (Natural range <>) of Byte;
+      subtype IV_Key_Index_Type is Natural range 1 .. 32;
+      subtype IV_Key_Type is IV_Key_Base_Type (IV_Key_Index_Type);
+
+      function Hash is new LSC.SHA2_Generic.Hash_SHA256
+         (Natural, Byte, Key_Base_Type, IV_Key_Index_Type, Byte, IV_Key_Type);
+
+      type Padding_Type is array (Natural range <>) of Byte;
+      type Block_Number_Text_Type is record
+         Block_Number : Block_Number_Type;
+         Padding      : Padding_Type(1 .. 8);
+      end record
+      with Size => 128;
+
+      Block_Number_Text : constant Block_Number_Text_Type :=
+         (Block_Number => Block_Number, Padding => (others => 0));
+
+      type Block_Number_Plaintext_Base_Type is array (Natural range <>) of Byte;
+      subtype Block_Number_Plaintext_Index_Type is Natural range 1 .. 16;
+      subtype Block_Number_Plaintext_Type is Block_Number_Plaintext_Base_Type (Block_Number_Plaintext_Index_Type);
+
+      function Convert is new Ada.Unchecked_Conversion
+         (Block_Number_Text_Type, Block_Number_Plaintext_Type);
+
+      function Enc_Key is new LSC.AES_Generic.Enc_Key
+         (Natural, Byte, IV_Key_Base_Type);
+
+      function Encrypt is new LSC.AES_Generic.Encrypt
+         (Natural, Byte, Block_Number_Plaintext_Base_Type, Natural, Byte, Ciphertext_Base_Type);
+
+  begin
+     return Encrypt (Plaintext => Convert(Block_Number_Text),
+                     Key       => Enc_Key(Hash(Key), LSC.AES_Generic.L256)) (Natural'First .. Natural'First + 15);
+   end Init_IV;
+
+   procedure Encrypt (Key          :     Key_Type;
+                      Block_Number :     Block_Number_Type;
+                      Plaintext    :     Plaintext_Type;
+                      Ciphertext   : out Ciphertext_Type)
+   is
+      function Enc_Key is new LSC.AES_Generic.Enc_Key
+         (Natural, Byte, Key_Base_Type);
+
+      procedure Encrypt is new LSC.AES_Generic.CBC.Encrypt
+         (Natural, Byte, Plaintext_Base_Type, Natural, Byte, Ciphertext_Base_Type);
+
+      IV : constant Ciphertext_Base_Type := Init_IV(Key, Block_Number);
+   begin
+
+      Encrypt (Plaintext  => Plaintext,
+               IV         => IV,
+               Key        => Enc_Key(Key, LSC.AES_Generic.L256),
+               Ciphertext => Ciphertext);
+   end Encrypt;
+
+
+   procedure Decrypt (Key          :     Key_Type;
+                      Block_Number :     Block_Number_Type;
+                      Ciphertext   :     Ciphertext_Type;
+                      Plaintext    : out Plaintext_Type)
+   is
+      function Dec_Key is new LSC.AES_Generic.Dec_Key
+         (Natural, Byte, Key_Base_Type);
+
+      procedure Decrypt is new LSC.AES_Generic.CBC.Decrypt
+         (Natural, Byte, Plaintext_Base_Type, Natural, Byte, Ciphertext_Base_Type);
+
+   begin
+      Decrypt (Ciphertext => Ciphertext,
+               IV         => Init_IV(Key, Block_Number),
+               Key        => Dec_Key(Key, LSC.AES_Generic.L256),
+               Plaintext  => Plaintext);
+   end Decrypt;
+
+end Aes_Cbc_4k;

repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads

@@ -0,0 +1,35 @@
+package Aes_Cbc_4k with SPARK_Mode
+is
+
+   -- pragma Pure; -- not possible because libsparkcrypto is not known as pure
+
+   type Byte              is mod 2**8 with Size => 8;
+   type Key_Base_type     is array (Natural range <>) of Byte;
+   subtype Key_Type       is Key_Base_type (1 .. 32);
+   type Block_Number_Type is mod 2**64 with Size => 64;
+
+   type Plaintext_Base_Type is array (Natural range <>) of Byte;
+   subtype Plaintext_Index_Type is Natural range 1 .. 4096;
+   subtype Plaintext_Type is Plaintext_Base_Type (Plaintext_Index_Type);
+
+   type Ciphertext_Base_Type is array (Natural range <>) of Byte;
+   subtype Ciphertext_Index_Type is Natural range 1 .. 4096;
+   subtype Ciphertext_Type is Ciphertext_Base_Type (Ciphertext_Index_Type);
+
+   procedure Encrypt (Key          :     Key_Type;
+                      Block_Number :     Block_Number_Type;
+                      Plaintext    :     Plaintext_Type;
+                      Ciphertext   : out Ciphertext_Type)
+   with Export,
+      Convention    => C,
+      External_Name => "_ZN10Aes_cbc_4k7encryptERKNS_3KeyENS_12Block_numberERKNS_9PlaintextERNS_10CiphertextE";
+
+   procedure Decrypt (Key          :     Key_Type;
+                      Block_Number :     Block_Number_Type;
+                      Ciphertext   :     Ciphertext_Type;
+                      Plaintext    : out Plaintext_Type)
+   with Export,
+      Convention    => C,
+      External_Name => "_ZN10Aes_cbc_4k7decryptERKNS_3KeyENS_12Block_numberERKNS_10CiphertextERNS_9PlaintextE";
+
+end Aes_Cbc_4k;

repos/gems/src/lib/aes_cbc_4k/spark.adc

@@ -0,0 +1,2 @@
+pragma SPARK_Mode (On);
+pragma Check_Policy (Debug, Disable);