Алгебра витоку ентропії для криптографічних обчислень з плаваючою точкою IEEE 754
Анотація
Актуальність. Арифметика з плаваючою точкою вносить залежну від платформи невизначеність, яка ігнорується стандартними криптографічними моделями безпеки і створює неквантифікований ризик витоку ентропії в реальних реалізаціях на базі стандарту IEEE 754.
Мета. Розробити строгу композиційну алгебраїчну систему (ELA) для оцінки втрат мінімальної ентропії, спричинених арифметикою IEEE 754, у довільно складних криптографічних конвеєрах.
Методи дослідження. ELA є комутативним півкільцем, елементами якого є символічні вирази витоку. Дві операції — ⊕ для послідовної композиції та ⊗ для паралельного галуження — відображають структуру виконання конвеєра. Визначено чотири родини генераторів, що відповідають основним джерелам невизначеності IEEE 754.
Результати. Доведено аксіоми півкільця, встановлено унікальну нормальну форму суми максимумів (SMNF), що обчислюється за O(|e|²), і доведено, що порядок домінування вирішується за поліноміальний час. Три випадки — NTT ML-KEM (8.6 проти 8.3 біт емпірично), RSA Montgomery (12.7 біт точний збіг) та нейромережева функція виведення ключа (4.8 проти 4.75 біт) — підтверджують алгебраїчні межі з точністю до 4%.
Висновки. ELA надає механізований шлях до сертифікації ентропійної захищеності криптографічних реалізацій з плаваючою точкою. Аналіз SMNF виявляє обробку субнормальних чисел з записом у нуль (γz) як ключову вразливість в усіх досліджених конвеєрах.
Завантаження
Посилання
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/.
