From a2743dcaeba024d201a0b85a81d89a068f941639 Mon Sep 17 00:00:00 2001 From: Norman Feske Date: Thu, 20 Dec 2018 16:49:14 +0100 Subject: [PATCH] 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/include/aes_cbc_4k/aes_cbc_4k.h | 31 +++++++ repos/gems/lib/mk/aes_cbc_4k.mk | 10 +++ repos/gems/run/aes_cbc_4k.run | 28 ++++++ repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb | 91 ++++++++++++++++++++ repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads | 35 ++++++++ repos/gems/src/lib/aes_cbc_4k/spark.adc | 2 + repos/gems/src/test/aes_cbc_4k/main.cc | 90 +++++++++++++++++++ repos/gems/src/test/aes_cbc_4k/target.mk | 3 + 8 files changed, 290 insertions(+) create mode 100644 repos/gems/include/aes_cbc_4k/aes_cbc_4k.h create mode 100644 repos/gems/lib/mk/aes_cbc_4k.mk create mode 100644 repos/gems/run/aes_cbc_4k.run create mode 100644 repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.adb create mode 100644 repos/gems/src/lib/aes_cbc_4k/aes_cbc_4k.ads create mode 100644 repos/gems/src/lib/aes_cbc_4k/spark.adc create mode 100644 repos/gems/src/test/aes_cbc_4k/main.cc create mode 100644 repos/gems/src/test/aes_cbc_4k/target.mk 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