Il kernel Ironclad

Ironclad è un kernel formalmente verificato, capace di calcolo in tempo reale, compatibile con UNIX e adatto a sistemi operativi generici o embedded. È scritto in SPARK e Ada ed è composto al 100% da software libero.

Ironclad include un'interfaccia POSIX, multiprocessing simmetrico, Controllo degli Accessi Obbligatorio (CAO), e la capacità di eseguire task in tempo reale rigoroso.

Perché scegliere Ironclad?

Libero

Ironclad è esclusivamente software libero ed è distribuito sotto la licenza GPLv3, garantendo che rimanga libero. Non è incluso né necessario alcun firmware proprietario, e lo stack di sviluppo è 100% software libero.

Verifica formale

Utilizziamo la verifica formale di SPARK per garantire l'assenza di errori e la correttezza di gran parte del kernel; esempi sono la crittografia, CAO e comunicazione tra processi.

Compatibilità

Portato a diverse piattaforme e schede, e progettato per essere facilmente portato a molte altre con relativa semplicità. La toolchain di GNU come unica dipendenza facilita la cross-compilazione.

Distribuzione ed ecosistema

La compatibilità con POSIX rende il porting e la creazione di software semplice e familiare. Diverse distribuzioni sono offerte pronte per essere scaricate e utilizzate per ciascuna delle piattaforme ufficialmente supportate. La distribuzione open source più prominente è Gloire.

Chi paga per Ironclad?

Ironclad sarà sempre gratuito per l'uso, lo studio e la modifica, quindi, per supportare il progetto, ci affidiamo all'uso di donazioni e sovvenzioni. Ogni contributo fa la differenza e ci consente di fare di più.

Grazie a:

Questo progetto è stato finanziato grazie all'iniziativa NGI Zero Core, un fondo istituito da NLnet con l'aiuto dell'iniziativa Next Generation Internet program della Commissione Europea. Più informazioni disponibili su la pagina del progetto NLnet.


Siamo inoltre grati per la collaborazione delle seguenti organizzazioni: