diff --git a/repos/gems/include/aes_cbc_4k/aes_cbc_4k.h b/repos/gems/include/aes_cbc_4k/aes_cbc_4k.h
new file mode 100644
index 0000000000..cbc6dc477a
--- /dev/null
+++ b/repos/gems/include/aes_cbc_4k/aes_cbc_4k.h
@@ -0,0 +1,31 @@
+/*
+ * \brief Interface for AES CBC encryption/decrytion of 4KiB data blocks
+ * \author Norman Feske
+ * \date 2018-12-20
+ */
+
+/*
+ * Copyright (C) 2018 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU Affero General Public License version 3.
+ */
+
+#ifndef _AES_CBC_4K_H_
+#define _AES_CBC_4K_H_
+
+namespace Aes_cbc_4k {
+
+ struct Key { char values[32]; };
+ struct Block { char values[4096]; };
+
+ struct Plaintext : Block { };
+ struct Ciphertext : Block { };
+
+ struct Block_number { Genode::uint64_t value; };
+
+ void encrypt(Key const &, Block_number, Plaintext const &, Ciphertext &);
+ void decrypt(Key const &, Block_number, Ciphertext const &, Plaintext &);
+}
+
+#endif /* _AES_CBC_4K_H_ */
diff --git a/repos/gems/lib/mk/aes_cbc_4k.mk b/repos/gems/lib/mk/aes_cbc_4k.mk
new file mode 100644
index 0000000000..97fdfa630c
--- /dev/null
+++ b/repos/gems/lib/mk/aes_cbc_4k.mk
@@ -0,0 +1,10 @@
+SRC_ADB := aes_cbc_4k.adb
+LIBS += spark libsparkcrypto
+
+CC_ADA_OPT += -gnatec=$(REP_DIR)/src/lib/aes_cbc_4k/spark.adc
+
+INC_DIR += $(REP_DIR)/src/lib/aes_cbc_4k
+
+aes_cbc_4k.o : aes_cbc_4k.ads
+
+vpath % $(REP_DIR)/src/lib/aes_cbc_4k
diff --git a/repos/gems/run/aes_cbc_4k.run b/repos/gems/run/aes_cbc_4k.run
new file mode 100644
index 0000000000..cd57f83a69
--- /dev/null
+++ b/repos/gems/run/aes_cbc_4k.run
@@ -0,0 +1,28 @@
+build "core init test/aes_cbc_4k"
+
+create_boot_directory
+
+install_config {
+
+
+
+
+
+
+
+
+
+
+
+
+ }
+
+exec echo -n "Not for the public" > [run_dir]/genode/plaintext
+exec echo -n "Better kept private" > [run_dir]/genode/key
+
+build_boot_image "core ld.lib.so spark.lib.so libsparkcrypto.lib.so init test-aes_cbc_4k"
+
+append qemu_args "-nographic "
+
+run_genode_until "Test succeeded.*\n" 20
+
diff --git a/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb b/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb
new file mode 100644
index 0000000000..09fa3e53d3
--- /dev/null
+++ b/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;
diff --git a/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads b/repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads
new file mode 100644
index 0000000000..8bf8386bd0
--- /dev/null
+++ b/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;
diff --git a/repos/gems/src/lib/aes_cbc_4k/spark.adc b/repos/gems/src/lib/aes_cbc_4k/spark.adc
new file mode 100644
index 0000000000..c1f72d5b92
--- /dev/null
+++ b/repos/gems/src/lib/aes_cbc_4k/spark.adc
@@ -0,0 +1,2 @@
+pragma SPARK_Mode (On);
+pragma Check_Policy (Debug, Disable);
diff --git a/repos/gems/src/test/aes_cbc_4k/main.cc b/repos/gems/src/test/aes_cbc_4k/main.cc
new file mode 100644
index 0000000000..8fae71c7c9
--- /dev/null
+++ b/repos/gems/src/test/aes_cbc_4k/main.cc
@@ -0,0 +1,90 @@
+/*
+ * \brief Test for using libsparkcrypto
+ * \author Norman Feske
+ * \date 2018-12-20
+ */
+
+/*
+ * Copyright (C) 2018 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU Affero General Public License version 3.
+ */
+
+/* Genode includes */
+#include
+#include
+
+#include
+
+namespace Test {
+ struct Main;
+ using namespace Genode;
+}
+
+
+namespace Genode {
+
+ static inline void print(Output &out, Aes_cbc_4k::Ciphertext const &data)
+ {
+ constexpr unsigned NUM_LINES = 10;
+ constexpr unsigned BYTES_PER_LINE = 32;
+
+ for (unsigned line = 0; line < NUM_LINES; line++) {
+
+ for (unsigned i = 0; i < BYTES_PER_LINE; i++)
+ print(out, Genode::Hex(data.values[line*BYTES_PER_LINE + i],
+ Genode::Hex::OMIT_PREFIX,
+ Genode::Hex::PAD));
+ if (line + 1 < NUM_LINES)
+ print(out, "\n");
+ }
+ }
+}
+
+
+struct Test::Main
+{
+ Env &_env;
+
+ Attached_rom_dataspace _plaintext { _env, "plaintext" };
+ Attached_rom_dataspace _key { _env, "key" };
+
+ Aes_cbc_4k::Ciphertext _ciphertext { };
+ Aes_cbc_4k::Plaintext _decrypted_plaintext { };
+
+ Main(Env &env) : _env(env)
+ {
+ Aes_cbc_4k::Block_number const block_number { 0 };
+
+ Aes_cbc_4k::Key const &key = *_key.local_addr();
+ Aes_cbc_4k::Plaintext const &plaintext = *_plaintext.local_addr();
+
+ Aes_cbc_4k::encrypt(key, block_number, plaintext, _ciphertext);
+
+ log("ciphertext:\n", _ciphertext);
+
+ Aes_cbc_4k::decrypt(key, block_number, _ciphertext, _decrypted_plaintext);
+
+ /* compare decrypted ciphertext with original plaintext */
+ if (memcmp(plaintext.values, _decrypted_plaintext.values, sizeof(plaintext))) {
+ error("plaintext differs from decrypted ciphertext");
+ return;
+ }
+
+ log("Test succeeded");
+ }
+};
+
+
+Genode::Env *__genode_env;
+
+
+void Component::construct(Genode::Env &env)
+{
+ /* make ada-runtime happy */
+ __genode_env = &env;
+ env.exec_static_constructors();
+
+ static Test::Main inst(env);
+}
diff --git a/repos/gems/src/test/aes_cbc_4k/target.mk b/repos/gems/src/test/aes_cbc_4k/target.mk
new file mode 100644
index 0000000000..aabce7d4b6
--- /dev/null
+++ b/repos/gems/src/test/aes_cbc_4k/target.mk
@@ -0,0 +1,3 @@
+TARGET := test-aes_cbc_4k
+SRC_CC := main.cc
+LIBS += base aes_cbc_4k