AxonOS è un progetto open source dedicato alla realizzazione di un’infrastruttura software per le brain-computer interface (BCI), ovvero sistemi capaci di elaborare segnali provenienti dal cervello e utilizzarli per interagire con dispositivi e applicazioni. L’obiettivo è fornire una base tecnica verificabile sulla quale laboratori di ricerca, gruppi di ingegneria clinica e aziende possano costruire applicazioni BCI con requisiti stringenti in termini di tempi di risposta, isolamento e gestione dei dati.
Il progetto utilizza un microkernel scritto in Rust #![no_std], con particolare attenzione ai sistemi embedded basati su microcontrollori Cortex-M4F e Cortex-M33. Il codice sorgente e le specifiche sono pubblici, mentre le decisioni architetturali vengono documentate attraverso RFC numerate e datate.
Uno degli aspetti più interessanti di AxonOS riguarda il modo in cui affronta la prevedibilità temporale. Il progetto non vuole limitarsi a pubblicare benchmark ottenuti durante l’esecuzione del software, ma utilizza tecniche di verifica formale per determinare limiti superiori sul comportamento delle operazioni considerate critiche.
Un’architettura BCI basata su Rust e verifica formale
La scelta di Rust è strettamente collegata agli obiettivi di sicurezza del progetto. AxonOS dichiara attualmente zero codice unsafe e utilizza una serie di harness Kani per la verifica mediante Bounded Model Checking. Complessivamente, il progetto indica 40 harness distribuiti lungo lo stack.
Questo approccio punta a rendere verificabili alcune proprietà che, in un’applicazione BCI, possono avere un’importanza particolare. Il progetto utilizza infatti analisi di schedulabilità e verifica formale per studiare il comportamento delle attività real-time.
Il preprint tecnico pubblicato da AxonOS descrive, tra gli altri elementi, una schedulabilità EDF secondo il modello Liu-Layland, una risposta R1 indicata in 972 microsecondi all’interno di una deadline di 4 millisecondi, la correttezza Release/Acquire di una coda SPSC verificata con Kani e un modello di isolamento basato sulle capability.
È importante distinguere queste proprietà dalle misurazioni fisiche. I numeri temporali pubblicati nella documentazione progettuale sono attualmente previsioni analitiche ottenute dai cycle count indicati nelle documentazioni hardware. Il progetto specifica infatti che la validazione con strumenti di laboratorio rappresenta uno dei passaggi ancora da completare.
Un altro elemento centrale riguarda la privacy. AxonOS cerca di spostare alcune garanzie dal livello applicativo alla struttura stessa del sistema. Tipi come RawEEG, EmotionState e CognitiveProfile non fanno parte delle capability disponibili nell’architettura descritta dal progetto. L’idea è impedire determinate forme di accesso ai dati direttamente attraverso il modello dei tipi, invece di affidarsi esclusivamente a controlli eseguiti durante l’esecuzione.
Anche il formato dei dati è documentato pubblicamente. Il progetto indica sei implementazioni del codec del wire format in linguaggi differenti, con l’obiettivo di ottenere una codifica byte-identica. Tra quelle già utilizzate vengono citati Python, C, JavaScript, Java, una libreria condivisa tramite C ABI e assembly x86-64.
Questa caratteristica è particolarmente importante per un progetto che vuole essere implementabile anche da soggetti indipendenti. La documentazione include infatti vettori pubblici di conformità e una sfida rivolta a chi desidera realizzare un’implementazione in un linguaggio non ancora incluso nell’elenco ufficiale.
Specifiche aperte, Community Radar e prossimi test hardware
AxonOS utilizza un modello di sviluppo fortemente orientato alla pubblicazione delle decisioni tecniche. Le specifiche architetturali vengono raccolte in RFC pubbliche e distribuite con licenza CC-BY-SA-4.0, mentre il codice principale utilizza Apache-2.0 oppure MIT.
Il progetto dichiara attualmente 23 repository pubblici su GitHub e nove RFC nell’apposito repository. Questa impostazione permette di seguire l’evoluzione dell’architettura senza dover dipendere da documentazione privata o da componenti proprietari.
Interessante anche il Community Radar, uno strumento che raccoglie periodicamente progetti pubblici GitHub legati a BCI, neurotech e real-time Rust. Il sistema effettua una scansione ogni tre ore e conserva i risultati attraverso commit Git. La funzione utilizzata per determinare la rilevanza dei repository è inoltre disponibile separatamente, così da poter essere analizzata e riprodotta.
Il progetto mette però in evidenza anche alcune questioni ancora aperte. Una riguarda il rilevamento dei replay nel formato di intent record definito da RFC-0006. Una precedente specifica prevedeva un sequence counter per individuare osservazioni perse o valori non monotoni, ma il record effettivamente distribuito non contiene quel campo. AxonOS considera quindi il problema ancora irrisolto e indica diverse possibili direzioni, tra cui l’utilizzo dei tre byte disponibili nel payload, una revisione del formato oppure lo spostamento della responsabilità al livello di trasporto.
L’altra verifica importante riguarda l’hardware. La prima fase del progetto prevede una prova indipendente attraverso una scheda STM32H573, una pipeline con GPIO strumentati e un logic analyzer capace di una risoluzione di 10 nanosecondi. Lo scopo è confrontare le previsioni analitiche con una misurazione effettuata direttamente sul dispositivo.
Il risultato dovrebbe essere pubblicato indipendentemente dall’esito. È proprio questo passaggio a rappresentare uno degli elementi tecnici più interessanti di AxonOS: trasformare le affermazioni sul comportamento real-time da semplici numeri ottenuti nei benchmark in ipotesi che possano essere sottoposte a una verifica hardware indipendente.
Il progetto prevede inoltre un percorso di governance nel quale un’eventuale fondazione non profit dovrebbe arrivare successivamente, dopo il raggiungimento di specifici requisiti di integrazione. Nel frattempo, codice, RFC, strumenti di verifica e documentazione rimangono pubblicamente consultabili, lasciando agli sviluppatori la possibilità di studiare, implementare e mettere alla prova l’architettura.