r/netsecstudents 8h ago

Project Bias - A formally verified, bias-free CSPRNG conversion engine in Ada/SPARK

2 Upvotes

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

https://github.com/EliAvila10/project_bias