  The Linux pseudorandom number generator (PRNG) is a PRNG with entropy inputs
and is widely used in many security-related applications and protocols. This
PRNG is written as an open-source code which is subject to regular changes. It
has been analysed in the works of Gutterman et al., Lacharme et al., while in
the meantime, several changes have been applied to the code, to counter the
attacks presented since then. Our work describes the Linux PRNG of kernel
versions 5.3 and upwards. We discuss the PRNG architecture briefly and in
detail about the entropy mixing function.
  Our goal is to study the entropy mixing function and analyse it over two
properties, namely, injectivity and length of the longest chain. For this
purpose, we will be using SAT solving and model counting over targetted
formulas involving multiple states of the Linux entropy store.
