crypto: Implement RFC8439-compatible variant of ChaCha20

sipa · dhruv · sipa · commit 511a8d406e31 · 2023-07-07T17:16:27.000-04:00
There are two variants of ChaCha20 in use. The original one uses a 64-bit
nonce and a 64-bit block counter, while the one used in RFC8439 uses a
96-bit nonce and 32-bit block counter. This commit changes the interface
to use the 96/32 split (but automatically incrementing the first 32-bit
part of the nonce when the 32-bit block counter overflows, so to retain
compatibility with &gt;256 GiB output).

Simultaneously, also merge the SetIV and Seek64 functions, as we almost
always call both anyway.

Co-authored-by: dhruv &lt;856960+dhruv@users.noreply.github.com&gt;
diff --git a/src/bench/chacha20.cpp b/src/bench/chacha20.cpp
@@ -15,8 +15,7 @@ static void CHACHA20(benchmark::Bench& bench, size_t buffersize)
 {
     std::vector<uint8_t> key(32,0);
     ChaCha20 ctx(key.data());
-    ctx.SetIV(0);
-    ctx.Seek64(0);
+    ctx.Seek64({0, 0}, 0);
     std::vector<uint8_t> in(buffersize,0);
     std::vector<uint8_t> out(buffersize,0);
     bench.batch(in.size()).unit("byte").run([&] {
diff --git a/src/crypto/chacha20.cpp b/src/crypto/chacha20.cpp
@@ -47,16 +47,12 @@ ChaCha20Aligned::ChaCha20Aligned(const unsigned char* key32)
     SetKey32(key32);
 }
 
-void ChaCha20Aligned::SetIV(uint64_t iv)
+void ChaCha20Aligned::Seek64(Nonce96 nonce, uint32_t block_counter)
 {
-    input[10] = iv;
-    input[11] = iv >> 32;
-}
-
-void ChaCha20Aligned::Seek64(uint64_t pos)
-{
-    input[8] = pos;
-    input[9] = pos >> 32;
+    input[8] = block_counter;
+    input[9] = nonce.first;
+    input[10] = nonce.second;
+    input[11] = nonce.second >> 32;
 }
 
 inline void ChaCha20Aligned::Keystream64(unsigned char* c, size_t blocks)
diff --git a/src/crypto/chacha20.h b/src/crypto/chacha20.h
@@ -7,9 +7,15 @@
 
 #include <cstdlib>
 #include <stdint.h>
+#include <utility>
 
 // classes for ChaCha20 256-bit stream cipher developed by Daniel J. Bernstein
-// https://cr.yp.to/chacha/chacha-20080128.pdf */
+// https://cr.yp.to/chacha/chacha-20080128.pdf.
+//
+// The 128-bit input is here implemented as a 96-bit nonce and a 32-bit block
+// counter, as in RFC8439 Section 2.3. When the 32-bit block counter overflows
+// the first 32-bit part of the nonce is automatically incremented, making it
+// conceptually compatible with variants that use a 64/64 split instead.
 
 /** ChaCha20 cipher that only operates on multiples of 64 bytes. */
 class ChaCha20Aligned
@@ -26,11 +32,22 @@ class ChaCha20Aligned
     /** set 32-byte key. */
     void SetKey32(const unsigned char* key32);
 
-    /** set the 64-bit nonce. */
-    void SetIV(uint64_t iv);
+    /** Type for 96-bit nonces used by the Set function below.
+     *
+     * The first field corresponds to the LE32-encoded first 4 bytes of the nonce, also referred
+     * to as the '32-bit fixed-common part' in Example 2.8.2 of RFC8439.
+     *
+     * The second field corresponds to the LE64-encoded last 8 bytes of the nonce.
+     *
+     */
+    using Nonce96 = std::pair<uint32_t, uint64_t>;
 
-    /** set the 64bit block counter (pos seeks to byte position 64*pos). */
-    void Seek64(uint64_t pos);
+    /** Set the 96-bit nonce and 32-bit block counter.
+     *
+     * Block_counter selects a position to seek to (to byte 64*block_counter). After 256 GiB, the
+     * block counter overflows, and nonce.first is incremented.
+     */
+    void Seek64(Nonce96 nonce, uint32_t block_counter);
 
     /** outputs the keystream of size <64*blocks> into <c> */
     void Keystream64(unsigned char* c, size_t blocks);
@@ -62,13 +79,13 @@ class ChaCha20
         m_bufleft = 0;
     }
 
-    /** set the 64-bit nonce. */
-    void SetIV(uint64_t iv) { m_aligned.SetIV(iv); }
+    /** 96-bit nonce type. */
+    using Nonce96 = ChaCha20Aligned::Nonce96;
 
-    /** set the 64bit block counter (pos seeks to byte position 64*pos). */
-    void Seek64(uint64_t pos)
+    /** Set the 96-bit nonce and 32-bit block counter. */
+    void Seek64(Nonce96 nonce, uint32_t block_counter)
     {
-        m_aligned.Seek64(pos);
+        m_aligned.Seek64(nonce, block_counter);
         m_bufleft = 0;
     }
 
diff --git a/src/crypto/chacha_poly_aead.cpp b/src/crypto/chacha_poly_aead.cpp
@@ -58,12 +58,11 @@ bool ChaCha20Poly1305AEAD::Crypt(uint64_t seqnr_payload, uint64_t seqnr_aad, int
 
     unsigned char expected_tag[POLY1305_TAGLEN], poly_key[POLY1305_KEYLEN];
     memset(poly_key, 0, sizeof(poly_key));
-    m_chacha_main.SetIV(seqnr_payload);
 
     // block counter 0 for the poly1305 key
     // use lower 32bytes for the poly1305 key
     // (throws away 32 unused bytes (upper 32) from this ChaCha20 round)
-    m_chacha_main.Seek64(0);
+    m_chacha_main.Seek64({0, seqnr_payload}, 0);
     m_chacha_main.Crypt(poly_key, poly_key, sizeof(poly_key));
 
     // if decrypting, verify the tag prior to decryption
@@ -85,8 +84,7 @@ bool ChaCha20Poly1305AEAD::Crypt(uint64_t seqnr_payload, uint64_t seqnr_aad, int
     // calculate and cache the next 64byte keystream block if requested sequence number is not yet the cache
     if (m_cached_aad_seqnr != seqnr_aad) {
         m_cached_aad_seqnr = seqnr_aad;
-        m_chacha_header.SetIV(seqnr_aad);
-        m_chacha_header.Seek64(0);
+        m_chacha_header.Seek64({0, seqnr_aad}, 0);
         m_chacha_header.Keystream(m_aad_keystream_buffer, CHACHA20_ROUND_OUTPUT);
     }
     // crypt the AAD (3 bytes message length) with given position in AAD cipher instance keystream
@@ -95,7 +93,7 @@ bool ChaCha20Poly1305AEAD::Crypt(uint64_t seqnr_payload, uint64_t seqnr_aad, int
     dest[2] = src[2] ^ m_aad_keystream_buffer[aad_pos + 2];
 
     // Set the playload ChaCha instance block counter to 1 and crypt the payload
-    m_chacha_main.Seek64(1);
+    m_chacha_main.Seek64({0, seqnr_payload}, 1);
     m_chacha_main.Crypt(src + CHACHA20_POLY1305_AEAD_AAD_LEN, dest + CHACHA20_POLY1305_AEAD_AAD_LEN, src_len - CHACHA20_POLY1305_AEAD_AAD_LEN);
 
     // If encrypting, calculate and append tag
@@ -117,8 +115,7 @@ bool ChaCha20Poly1305AEAD::GetLength(uint32_t* len24_out, uint64_t seqnr_aad, in
     if (m_cached_aad_seqnr != seqnr_aad) {
         // we need to calculate the 64 keystream bytes since we reached a new aad sequence number
         m_cached_aad_seqnr = seqnr_aad;
-        m_chacha_header.SetIV(seqnr_aad);                                         // use LE for the nonce
-        m_chacha_header.Seek64(0);                                               // block counter 0
+        m_chacha_header.Seek64({0, seqnr_aad}, 0);                                // use LE for the nonce
         m_chacha_header.Keystream(m_aad_keystream_buffer, CHACHA20_ROUND_OUTPUT); // write keystream to the cache
     }
 
diff --git a/src/test/crypto_tests.cpp b/src/test/crypto_tests.cpp
@@ -131,14 +131,13 @@ static void TestAES256CBC(const std::string &hexkey, const std::string &hexiv, b
     }
 }
 
-static void TestChaCha20(const std::string &hex_message, const std::string &hexkey, uint64_t nonce, uint64_t seek, const std::string& hexout)
+static void TestChaCha20(const std::string &hex_message, const std::string &hexkey, ChaCha20::Nonce96 nonce, uint32_t seek, const std::string& hexout)
 {
     std::vector<unsigned char> key = ParseHex(hexkey);
     assert(key.size() == 32);
     std::vector<unsigned char> m = ParseHex(hex_message);
     ChaCha20 rng(key.data());
-    rng.SetIV(nonce);
-    rng.Seek64(seek);
+    rng.Seek64(nonce, seek);
     std::vector<unsigned char> outres;
     outres.resize(hexout.size() / 2);
     assert(hex_message.empty() || m.size() * 2 == hexout.size());
@@ -152,8 +151,7 @@ static void TestChaCha20(const std::string &hex_message, const std::string &hexk
     BOOST_CHECK_EQUAL(hexout, HexStr(outres));
     if (!hex_message.empty()) {
         // Manually XOR with the keystream and compare the output
-        rng.SetIV(nonce);
-        rng.Seek64(seek);
+        rng.Seek64(nonce, seek);
         std::vector<unsigned char> only_keystream(outres.size());
         rng.Keystream(only_keystream.data(), only_keystream.size());
         for (size_t i = 0; i != m.size(); i++) {
@@ -169,7 +167,7 @@ static void TestChaCha20(const std::string &hex_message, const std::string &hexk
         lens[1] = InsecureRandRange(hexout.size() / 2U + 1U - lens[0]);
         lens[2] = hexout.size() / 2U - lens[0] - lens[1];
 
-        rng.Seek64(seek);
+        rng.Seek64(nonce, seek);
         outres.assign(hexout.size() / 2U, 0);
         size_t pos = 0;
         for (int j = 0; j < 3; ++j) {
@@ -485,43 +483,43 @@ BOOST_AUTO_TEST_CASE(chacha20_testvector)
     // RFC 7539/8439 A.1 Test Vector #1:
     TestChaCha20("",
                  "0000000000000000000000000000000000000000000000000000000000000000",
-                 0, 0,
+                 {0, 0}, 0,
                  "76b8e0ada0f13d90405d6ae55386bd28bdd219b8a08ded1aa836efcc8b770dc7"
                  "da41597c5157488d7724e03fb8d84a376a43b8f41518a11cc387b669b2ee6586");
 
     // RFC 7539/8439 A.1 Test Vector #2:
     TestChaCha20("",
                  "0000000000000000000000000000000000000000000000000000000000000000",
-                 0, 1,
+                 {0, 0}, 1,
                  "9f07e7be5551387a98ba977c732d080dcb0f29a048e3656912c6533e32ee7aed"
                  "29b721769ce64e43d57133b074d839d531ed1f28510afb45ace10a1f4b794d6f");
 
     // RFC 7539/8439 A.1 Test Vector #3:
     TestChaCha20("",
                  "0000000000000000000000000000000000000000000000000000000000000001",
-                 0, 1,
+                 {0, 0}, 1,
                  "3aeb5224ecf849929b9d828db1ced4dd832025e8018b8160b82284f3c949aa5a"
                  "8eca00bbb4a73bdad192b5c42f73f2fd4e273644c8b36125a64addeb006c13a0");
 
     // RFC 7539/8439 A.1 Test Vector #4:
     TestChaCha20("",
                  "00ff000000000000000000000000000000000000000000000000000000000000",
-                 0, 2,
+                 {0, 0}, 2,
                  "72d54dfbf12ec44b362692df94137f328fea8da73990265ec1bbbea1ae9af0ca"
                  "13b25aa26cb4a648cb9b9d1be65b2c0924a66c54d545ec1b7374f4872e99f096");
 
     // RFC 7539/8439 A.1 Test Vector #5:
     TestChaCha20("",
                  "0000000000000000000000000000000000000000000000000000000000000000",
-                 0x200000000000000, 0,
+                 {0, 0x200000000000000}, 0,
                  "c2c64d378cd536374ae204b9ef933fcd1a8b2288b3dfa49672ab765b54ee27c7"
                  "8a970e0e955c14f3a88e741b97c286f75f8fc299e8148362fa198a39531bed6d");
 
     // RFC 7539/8439 A.2 Test Vector #1:
     TestChaCha20("0000000000000000000000000000000000000000000000000000000000000000"
                  "0000000000000000000000000000000000000000000000000000000000000000",
                  "0000000000000000000000000000000000000000000000000000000000000000",
-                 0, 0,
+                 {0, 0}, 0,
                  "76b8e0ada0f13d90405d6ae55386bd28bdd219b8a08ded1aa836efcc8b770dc7"
                  "da41597c5157488d7724e03fb8d84a376a43b8f41518a11cc387b669b2ee6586");
 
@@ -539,7 +537,7 @@ BOOST_AUTO_TEST_CASE(chacha20_testvector)
                  "74696f6e73206d61646520617420616e792074696d65206f7220706c6163652c"
                  "207768696368206172652061646472657373656420746f",
                  "0000000000000000000000000000000000000000000000000000000000000001",
-                 0x200000000000000, 1,
+                 {0, 0x200000000000000}, 1,
                  "a3fbf07df3fa2fde4f376ca23e82737041605d9f4f4f57bd8cff2c1d4b7955ec"
                  "2a97948bd3722915c8f3d337f7d370050e9e96d647b7c39f56e031ca5eb6250d"
                  "4042e02785ececfa4b4bb5e8ead0440e20b6e8db09d881a7c6132f420e527950"
@@ -559,7 +557,7 @@ BOOST_AUTO_TEST_CASE(chacha20_testvector)
                  "6162653a0a416c6c206d696d737920776572652074686520626f726f676f7665"
                  "732c0a416e6420746865206d6f6d65207261746873206f757467726162652e",
                  "1c9240a5eb55d38af333888604f6b5f0473917c1402b80099dca5cbc207075c0",
-                 0x200000000000000, 42,
+                 {0, 0x200000000000000}, 42,
                  "62e6347f95ed87a45ffae7426f27a1df5fb69110044c0d73118effa95b01e5cf"
                  "166d3df2d721caf9b21e5fb14c616871fd84c54f9d65b283196c7fe4f60553eb"
                  "f39c6402c42234e32a356b3e764312a61a5532055716ead6962568f87d3f3f77"
@@ -569,14 +567,14 @@ BOOST_AUTO_TEST_CASE(chacha20_testvector)
     TestChaCha20("4c616469657320616e642047656e746c656d656e206f662074686520636c617373206f66202739393a204966204920636f756"
                  "c64206f6666657220796f75206f6e6c79206f6e652074697020666f7220746865206675747572652c2073756e73637265656e"
                  "20776f756c642062652069742e",
-                 "000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f", 0x4a000000UL, 1,
+                 "000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f", {0, 0x4a000000UL}, 1,
                  "6e2e359a2568f98041ba0728dd0d6981e97e7aec1d4360c20a27afccfd9fae0bf91b65c5524733ab8f593dabcd62b3571639d"
                  "624e65152ab8f530c359f0861d807ca0dbf500d6a6156a38e088a22b65e52bc514d16ccf806818ce91ab77937365af90bbf74"
                  "a35be6b40b8eedf2785e42874d"
                  );
 
     // test keystream output
-    TestChaCha20("", "000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f", 0x4a000000UL, 1,
+    TestChaCha20("", "000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f", {0, 0x4a000000UL}, 1,
                  "224f51f3401bd9e12fde276fb8631ded8c131f823d2c06e27e4fcaec9ef3cf788a3b0aa372600a92b57974cded2b9334794cb"
                  "a40c63e34cdea212c4cf07d41b769a6749f3f630f4122cafe28ec4dc47e26d4346d70b98c73f3e9c53ac40c5945398b6eda1a"
                  "832c89c167eacd901d7e2bf363");
@@ -730,8 +728,7 @@ static void TestChaCha20Poly1305AEAD(bool must_succeed, unsigned int expected_aa
     BOOST_CHECK(memcmp(ciphertext_buf.data(), expected_ciphertext_and_mac.data(), ciphertext_buf.size()) == 0);
 
     // manually construct the AAD keystream
-    cmp_ctx.SetIV(seqnr_aad);
-    cmp_ctx.Seek64(0);
+    cmp_ctx.Seek64({0, seqnr_aad}, 0);
     cmp_ctx.Keystream(cmp_ctx_buffer.data(), 64);
     BOOST_CHECK(memcmp(expected_aad_keystream.data(), cmp_ctx_buffer.data(), expected_aad_keystream.size()) == 0);
     // crypt the 3 length bytes and compare the length
@@ -758,8 +755,7 @@ static void TestChaCha20Poly1305AEAD(bool must_succeed, unsigned int expected_aa
             BOOST_CHECK(memcmp(ciphertext_buf.data(), expected_ciphertext_and_mac_sequence999.data(), expected_ciphertext_and_mac_sequence999.size()) == 0);
         }
         // set nonce and block counter, output the keystream
-        cmp_ctx.SetIV(seqnr_aad);
-        cmp_ctx.Seek64(0);
+        cmp_ctx.Seek64({0, seqnr_aad}, 0);
         cmp_ctx.Keystream(cmp_ctx_buffer.data(), 64);
 
         // crypt the 3 length bytes and compare the length
diff --git a/src/test/fuzz/crypto_chacha20.cpp b/src/test/fuzz/crypto_chacha20.cpp
@@ -28,10 +28,11 @@ FUZZ_TARGET(crypto_chacha20)
                 chacha20.SetKey32(key.data());
             },
             [&] {
-                chacha20.SetIV(fuzzed_data_provider.ConsumeIntegral<uint64_t>());
-            },
-            [&] {
-                chacha20.Seek64(fuzzed_data_provider.ConsumeIntegral<uint64_t>());
+                chacha20.Seek64(
+                    {
+                        fuzzed_data_provider.ConsumeIntegral<uint32_t>(),
+                        fuzzed_data_provider.ConsumeIntegral<uint64_t>()
+                    }, fuzzed_data_provider.ConsumeIntegral<uint32_t>());
             },
             [&] {
                 std::vector<uint8_t> output(fuzzed_data_provider.ConsumeIntegralInRange<size_t>(0, 4096));
@@ -63,17 +64,16 @@ void ChaCha20SplitFuzz(FuzzedDataProvider& provider)
     auto key_bytes = provider.ConsumeBytes<unsigned char>(32);
     std::copy(key_bytes.begin(), key_bytes.end(), key);
     uint64_t iv = provider.ConsumeIntegral<uint64_t>();
+    uint32_t iv_prefix = provider.ConsumeIntegral<uint32_t>();
     uint64_t total_bytes = provider.ConsumeIntegralInRange<uint64_t>(0, 1000000);
-    /* ~x = 2^64 - 1 - x, so ~(total_bytes >> 6) is the maximal seek position. */
-    uint64_t seek = provider.ConsumeIntegralInRange<uint64_t>(0, ~(total_bytes >> 6));
+    /* ~x = 2^BITS - 1 - x, so ~(total_bytes >> 6) is the maximal seek position. */
+    uint32_t seek = provider.ConsumeIntegralInRange<uint32_t>(0, ~(uint32_t)(total_bytes >> 6));
 
     // Initialize two ChaCha20 ciphers, with the same key/iv/position.
     ChaCha20 crypt1(key);
     ChaCha20 crypt2(key);
-    crypt1.SetIV(iv);
-    crypt1.Seek64(seek);
-    crypt2.SetIV(iv);
-    crypt2.Seek64(seek);
+    crypt1.Seek64({iv_prefix, iv}, seek);
+    crypt2.Seek64({iv_prefix, iv}, seek);
 
     // Construct vectors with data.
     std::vector<unsigned char> data1, data2;
diff --git a/src/test/fuzz/crypto_diff_fuzz_chacha20.cpp b/src/test/fuzz/crypto_diff_fuzz_chacha20.cpp
@@ -284,6 +284,8 @@ FUZZ_TARGET(crypto_diff_fuzz_chacha20)
 
     // ECRYPT_keysetup() doesn't set the counter and nonce to 0 while SetKey32() does
     static const uint8_t iv[8] = {0, 0, 0, 0, 0, 0, 0, 0};
+    ChaCha20::Nonce96 nonce{0, 0};
+    uint32_t counter{0};
     ECRYPT_ivsetup(&ctx, iv);
 
     LIMITED_WHILE (fuzzed_data_provider.ConsumeBool(), 3000) {
@@ -292,45 +294,56 @@ FUZZ_TARGET(crypto_diff_fuzz_chacha20)
             [&] {
                 const std::vector<unsigned char> key = ConsumeFixedLengthByteVector(fuzzed_data_provider, 32);
                 chacha20.SetKey32(key.data());
+                nonce = {0, 0};
+                counter = 0;
                 ECRYPT_keysetup(&ctx, key.data(), key.size() * 8, 0);
                 // ECRYPT_keysetup() doesn't set the counter and nonce to 0 while SetKey32() does
                 uint8_t iv[8] = {0, 0, 0, 0, 0, 0, 0, 0};
                 ECRYPT_ivsetup(&ctx, iv);
             },
             [&] {
+                uint32_t iv_prefix = fuzzed_data_provider.ConsumeIntegral<uint32_t>();
                 uint64_t iv = fuzzed_data_provider.ConsumeIntegral<uint64_t>();
-                chacha20.SetIV(iv);
+                nonce = {iv_prefix, iv};
+                counter = fuzzed_data_provider.ConsumeIntegral<uint32_t>();
+                chacha20.Seek64(nonce, counter);
+                ctx.input[12] = counter;
+                ctx.input[13] = iv_prefix;
                 ctx.input[14] = iv;
                 ctx.input[15] = iv >> 32;
             },
-            [&] {
-                uint64_t counter = fuzzed_data_provider.ConsumeIntegral<uint64_t>();
-                chacha20.Seek64(counter);
-                ctx.input[12] = counter;
-                ctx.input[13] = counter >> 32;
-            },
             [&] {
                 uint32_t integralInRange = fuzzed_data_provider.ConsumeIntegralInRange<size_t>(0, 4096);
-                // DJB's version seeks forward to a multiple of 64 bytes after every operation. Correct for that.
-                uint64_t pos = ctx.input[12] + (((uint64_t)ctx.input[13]) << 32) + ((integralInRange + 63) >> 6);
                 std::vector<uint8_t> output(integralInRange);
                 chacha20.Keystream(output.data(), output.size());
                 std::vector<uint8_t> djb_output(integralInRange);
                 ECRYPT_keystream_bytes(&ctx, djb_output.data(), djb_output.size());
                 assert(output == djb_output);
-                chacha20.Seek64(pos);
+                // DJB's version seeks forward to a multiple of 64 bytes after every operation. Correct for that.
+                uint32_t old_counter = counter;
+                counter += (integralInRange + 63) >> 6;
+                if (counter < old_counter) ++nonce.first;
+                if (integralInRange & 63) {
+                    chacha20.Seek64(nonce, counter);
+                }
+                assert(counter == ctx.input[12]);
             },
             [&] {
                 uint32_t integralInRange = fuzzed_data_provider.ConsumeIntegralInRange<size_t>(0, 4096);
-                // DJB's version seeks forward to a multiple of 64 bytes after every operation. Correct for that.
-                uint64_t pos = ctx.input[12] + (((uint64_t)ctx.input[13]) << 32) + ((integralInRange + 63) >> 6);
                 std::vector<uint8_t> output(integralInRange);
                 const std::vector<uint8_t> input = ConsumeFixedLengthByteVector(fuzzed_data_provider, output.size());
                 chacha20.Crypt(input.data(), output.data(), input.size());
                 std::vector<uint8_t> djb_output(integralInRange);
                 ECRYPT_encrypt_bytes(&ctx, input.data(), djb_output.data(), input.size());
                 assert(output == djb_output);
-                chacha20.Seek64(pos);
+                // DJB's version seeks forward to a multiple of 64 bytes after every operation. Correct for that.
+                uint32_t old_counter = counter;
+                counter += (integralInRange + 63) >> 6;
+                if (counter < old_counter) ++nonce.first;
+                if (integralInRange & 63) {
+                    chacha20.Seek64(nonce, counter);
+                }
+                assert(counter == ctx.input[12]);
             });
     }
 }
