An Entropy Leakage Algebra for IEEE 754 Floating-Point Cryptographic Computations
Abstract
Relevance. Floating-point arithmetic is not neutral ground for cryptography. The IEEE 754 standard leaves enough room for hardware and compilers to vary—in rounding, in FMA contraction, in subnormal handling—that the same program can produce measurably different intermediate distributions depending on where it runs. This nondeterminism is invisible to the programmer yet can shift probability mass in secret-dependent distributions, creating entropy leakage risks unaccounted for by conventional security models.
Objective. To develop a rigorous compositional framework—the Entropy Leakage Algebra (ELA)—for bounding the min-entropy loss induced by IEEE 754 floating-point arithmetic across arbitrarily complex cryptographic pipelines.
Methods. The ELA is a commutative semiring whose elements are symbolic leakage expressions. Two operations—⊕ for sequential composition and ⊗ for parallel branching—reflect the structure of floating-point pipeline execution. Four generator families grounded in IEEE 754 semantics (directed rounding γρ, FMA contraction γf, flush-to-zero γz, and expression reordering γr) are defined and proved sound via min-entropy bounds.
Results. The semiring axioms are proved. A unique Sum-of-Maxima Normal Form (SMNF) is established, computable in O(|e|²). The domination order on elements is shown to be decidable in polynomial time, enabling automated platform comparison. Three case studies—an ML-KEM NTT pipeline (8.6 vs. 8.3 bits empirical), an RSA Montgomery ladder (12.7 bits exact match), and a neural-network key-derivation function (4.8 vs. 4.75 bits)—validate algebraic bounds against empirical measurements with agreement within 4%.
Conclusions. The ELA provides a mechanizable certification path for entropy safety of floating-point cryptographic implementations. The SMNF analysis identifies flush-to-zero subnormal handling (γz) as the dominant vulnerability across all studied pipelines, a structural result that would otherwise require separate empirical measurement campaigns.
Downloads
References
IEEE Standard for Floating-Point Arithmetic, IEEE Std 754-2019, IEEE, 2019. DOI: 10.1109/IEEESTD.2019.8766229.
D. Brumley and D. Boneh, "Remote timing attacks are practical," in Proc. 12th USENIX Security Symp., 2003, pp. 1–14.
M. Andrysco, D. Kohlbrenner, K. Mowery, R. Jhala, S. Lerner, and H. Shacham, "On subnormal floating point and abnormal timing," in Proc. IEEE S&P 2015, pp. 623–639. DOI: 10.1109/SP.2015.44.
D. Monniaux, "The pitfalls of verifying floating-point computations," ACM Trans. Program. Lang. Syst., vol. 30, no. 3, 2008. DOI: 10.1145/1353445.1353446.
M. Abadi and C. Fournet, "Mobile values, new names, and secure communication," in Proc. POPL 2001, pp. 104–115. DOI: 10.1145/360204.360213.
B. Blanchet, "An efficient cryptographic protocol verifier based on Prolog rules," in Proc. CSFW 2001, pp. 82–96. DOI: 10.1109/CSFW.2001.930138.
R. Canetti, "Universally composable security," in Proc. FOCS 2001, pp. 136–145. DOI: 10.1109/SFCS.2001.959888.
U. Maurer and R. Renner, "Abstract cryptography," in Proc. ICS 2011, pp. 1–21.
G. Smith, "On the foundations of quantitative information flow," in Proc. FoSSaCS 2009, LNCS 5504, Springer, 2009, pp. 288–302. DOI: 10.1007/978-3-642-00596-1_21.
M. S. Alvim, K. Chatzikokolakis, A. McIver, C. Morgan, C. Palamidessi, and G. Smith, The Science of Quantitative Information Flow. Springer, 2020. DOI: 10.1007/978-3-319-96131-6.
L. Simon, D. Chisnall, and R. Anderson, "What you get is what you C," in Proc. EuroS&P 2018, pp. 1–15. DOI: 10.1109/EuroSP.2018.00011.
V. D'Silva, L. Haller, D. Kroening, and M. Tautschnig, "Numeric bounds analysis with conflict-driven learning," in Proc. TACAS 2012, LNCS 7214, pp. 48–63. DOI: 10.1007/978-3-642-28756-5_5.
R. E. Tarjan, "A unified approach to path problems," J. ACM, vol. 28, pp. 577–593, 1981. DOI: 10.1145/322261.322275.
D. Kozen, "Kleene algebra with tests," ACM Trans. Program. Lang. Syst., vol. 19, pp. 427–443, 1997. DOI: 10.1145/256167.256195.
R. Avanzi et al., CRYSTALS-Kyber Algorithm Specifications and Supporting Documentation, v3.02, NIST PQC Round 3, 2021. https://pq-crystals.org/kyber/.