Security proof for Linux's random number generator

Four researchers have published a formal proof that Linux's new deterministic random bit generator (DRBG) is secure in a particular sense — specifically, that the number of queries that would need to be made to it to uncover its internal state depends on the quality of the entropy it can collect from different sources. As long as it can gather enough entropy, it produces secure random numbers.

Since the significant structural changes in Linux 4 and Linux 5.17, there has
been no research on the provable security of Linux-DRBG. For the first time (to
the best of our knowledge), we formally model the Linux-DRBG in Linux 6.4.8
and prove its security in the seedless robustness model

Thanks to Jason Donenfeld for bringing the paper to our attention.