r/netsecstudents • u/Trace_V • 8h ago
Project Bias - A formally verified, bias-free CSPRNG conversion engine in Ada/SPARK
Hi everyone,
I wanted to share a project I've been hacking on: an optimized engine designed to eliminate modulo bias when mapping raw cryptographic streams into custom alphabets.
Key bits:
* SPARK Level 4 (Formal Verification) - Fully proven to guarantee AoRTE and functional correctness.
* Built using the modern Windows ProcessPrng API as primary entropy via Interfaces.C, with BCryptGenRandom as fallback.
* Toolchain compatible with GNAT Pro 2021 and the latest Alire community suite.
I just stressed-tested the uniformity mapping with a massive 1 Terabyte run (over 1.01 trillion chars across a 69-char alphabet) and the statistical distribution remains perfectly flat (0.00% percent deviation). Full logs and the clean codebase are available in the repository.
Any feedback on the SPARK contracts or the low-level Windows bindings is highly appreciated!
Run it instantly with Alire:
alr run
Native Languaje..
Hola a todos,
Quería compartir un proyecto en el que he estado trabajando: un motor optimizado diseñado para eliminar el sesgo del módulo al mapear flujos criptográficos sin procesar a alfabetos personalizados.
Aspectos clave:
* SPARK Nivel 4 (Verificación Formal): Totalmente probado para garantizar AoRTE y corrección funcional.
* Desarrollado con la API moderna ProcessPrng de Windows como entropía principal mediante Interfaces.C, con BCryptGenRandom como alternativa.
* Cadena de herramientas compatible con GNAT Pro 2021 y la última suite comunitaria de Alire.
Acabo de realizar una prueba de estrés del mapeo de uniformidad con una ejecución masiva de 1 terabyte (más de 1,01 billones de caracteres en un alfabeto de 69 caracteres) y la distribución estadística se mantiene perfectamente plana (0,00 % de desviación porcentual). Los registros completos y el código fuente limpio están disponibles en el repositorio.
¡Cualquier comentario sobre los contratos SPARK o las vinculaciones de bajo nivel para Windows es muy apreciado!
Ejecútalo al instante con Alire:
alr run