- Algoritme hash dan HMAC bawaan Python kini digantikan oleh kode kriptografi terverifikasi dari HACL*
- Sekitar 15.000 baris kode C diintegrasikan secara otomatis dari HACL* ke basis kode Python
- API streaming dirancang dan diverifikasi secara generik agar dapat menangani berbagai algoritme blok
- Menangani isu rekayasa tingkat lanjut seperti penanganan kegagalan alokasi memori, penyelesaian masalah kompilasi AVX2, dan optimasi lingkungan CI
- Melalui kolaborasi antara Python dan komunitas kriptografi, proyek ini berhasil mengamankan keamanan nyata sekaligus kemudahan pemeliharaan
Adopsi Menyeluruh Kode Terverifikasi untuk Algoritme Kriptografi Python
- Setelah CVE-2022-37454 terkait implementasi SHA3 yang muncul pada 2022, muncul kebutuhan agar infrastruktur hash Python dialihkan ke kode yang telah terverifikasi
- Selama dua setengah tahun berikutnya, Python sepenuhnya mengganti implementasi hash bawaan dan algoritme HMAC dengan implementasi terverifikasi berbasis HACL*
- Pergantian ini dilakukan sepenuhnya transparan bagi pengguna, tanpa kehilangan fungsi apa pun
- HACL* juga menambahkan fitur yang dibutuhkan Python: berbagai mode Blake2, API dukungan varian Keccak pada SHA3, optimasi streaming untuk HMAC, dan lain-lain
- Penerapan versi baru diotomatisasi melalui skrip, sehingga mudah dipelihara
Memahami API Streaming
- Sebagian besar algoritme kriptografi adalah algoritme blok, sehingga input harus diproses per blok
- Dalam lingkungan penggunaan nyata, memberi input per blok sulit dilakukan, sehingga diperlukan API streaming
- API streaming bekerja tanpa bergantung pada panjang input dan juga memungkinkan ekstraksi hasil antara
- Implementasi streaming memerlukan pengelolaan status yang kompleks, dan implementasi SHA3 sebelumnya pernah memiliki cacat keamanan serius yang terkait dengan hal ini
- Setiap algoritme hash memiliki cara pemrosesan berbeda sehingga kompleksitas meningkat: misalnya Blake2 tidak mengizinkan blok kosong, HMAC dapat menghapus kunci setelah inisialisasi, dan sebagainya
Verifikasi Algoritme Streaming Generik
- Metode yang diperkenalkan dalam makalah tahun 2021 adalah dengan mengabstraksikan algoritme blok, lalu mendefinisikan algoritme streaming generik di atas abstraksi tersebut
- Setelah itu, metode tersebut dapat diterapkan seperti templat ke masing-masing algoritme sehingga bisa digunakan ulang
- Generalisasi dilakukan agar mencakup berbagai kondisi khusus:
- Apakah panjang output dapat ditentukan (SHA3 vs Shake)
- Apakah ada input yang dibutuhkan sebelum pemrosesan dimulai (contoh: blok kunci pada Blake2)
- Perbedaan cara menangani blok terakhir
- Informasi tambahan yang perlu disimpan dalam status internal
- Cara menyalin status untuk mengekstrak hasil antara (
stack vs heap)
- Strategi penggunaan API individual per algoritme vs API keluarga algoritme
Menjamin Stabilitas Build untuk Integrasi ke Python
- CI Python diverifikasi terhadap lebih dari 50 toolchain dan arsitektur, sehingga masalah kecil sekalipun dapat terungkap
- Dalam implementasi HMAC, muncul masalah dukungan instruksi AVX2:
- Beberapa kompiler tidak dapat menangani header
immintrin.h tanpa AVX2
- Untuk mengatasinya, digunakan pola struct abstrak dalam C
- Karena adanya perbedaan antara konsep abstraksi pada kode C yang dihasilkan dari F* dan struktur
struct di C, kompiler krml perlu ditambah fitur analisis visibilitas yang lebih presisi
Menangani Kegagalan Alokasi Memori
- Model F* yang ada sebelumnya secara teoretis dapat memodelkan kegagalan memori, tetapi ini adalah penerapan praktis pertamanya
- Sesuai kebutuhan Python, struktur status, definisi algoritme, dan struktur streaming semuanya ditingkatkan agar dapat meneruskan kegagalan alokasi
- Di F*, hal ini menggunakan tipe
option, dan di C dikompilasi menjadi tagged union
- Ke depannya, ada kemungkinan pendekatan ini diubah menjadi metode flag kegagalan runtime untuk mengurangi kompleksitas
Otomatisasi Pembaruan Kode HACL*
- PR Python awal menggunakan
sed untuk menghapus definisi header yang tidak diperlukan, memperbaiki path, dan sebagainya
- Setelah stabilitas kode HACL* terkonfirmasi,
sed yang kompleks dihapus dan digantikan dengan skrip sederhana
- Dengan skrip ini, siapa pun dapat dengan mudah memperbarui kode HACL* ke versi terbaru di source tree Python
Kesimpulan
- Kode kriptografi terverifikasi telah berhasil diintegrasikan ke Python sebagai lingkungan produksi yang representatif
- Ini membuktikan bahwa teknologi tersebut bukan sekadar hasil riset akademis, tetapi juga praktis dan dapat dipelihara dalam perangkat lunak nyata
- Ini juga menjadi contoh baik kolaborasi antara komunitas Python dan para pengembang HACL*, dan dapat memengaruhi proyek lain di masa depan
2 komentar
Seperti yang juga disebutkan dalam komentar di Hacker News, sulit memahami apa yang sebenarnya telah dicapai ekosistem Python sehingga bisa disebut telah "melampaui tahap riset akademis dan menjadi sesuatu yang praktis serta mudah dipelihara dalam perangkat lunak nyata".
Kalau yang ingin disampaikan adalah bahwa mereka telah mengerjakan abstraksi algoritma streaming terhadap infrastruktur hashing lama yang belum terverifikasi, maka ini juga hanya permainan kata-kata "Pythonic" lainnya.
Komentar Hacker News
Versi Python tidak disebutkan. Setelah ditelusuri, fitur ini dijadwalkan akan disertakan di versi 3.14. Kemungkinan tidak akan terlihat sampai Oktober
Mereka memasukkan library C terverifikasi yang dihasilkan dari F* milik Microsoft ke CPython dan menulis ekstensi C
Penasaran apakah dukungan output "streaming" untuk SHAKE juga akan dibawa
Kriptografi modern yang digunakan secara luas pada praktiknya tidak bisa dipecahkan, dan perang kripto tahun 90-an kini terasa agak usang. Penasaran apakah ada pemikiran tentang dampaknya pada masyarakat
Penasaran seberapa dapat digunakan ulang kerangka verifikasi streaming yang umum ini di luar hash kriptografis
Penasaran apakah semua yang mengimpor modul kriptografi perlu menyertakan G++ atau semacamnya, atau apakah ini dikompilasi ke dalam CPython itu sendiri
Tidak terlalu paham soal kriptografi. Penasaran apa arti ini bagi Python
Penasaran seberapa besar bagian dari pengembangannya yang sudah diverifikasi, dan apa saja yang tercakup di dalamnya
Jumlah baris kode adalah ukuran yang sangat tidak tepat. Terutama ketika membanggakan angka besar dalam konteks kode kriptografi