Il prossimo Kernel Linux potrebbe essere capace di auto-verificare il proprio funzionamento con Runtime Verification

Che il Kernel Linux sia uno dei software più complessi al mondo lo abbiamo già evidenziato varie volte. E che sia anche fondamentale poter fare affidamento sul suo buon funzionamento è altrettanto evidente. Ovviamente, queste due caratteristiche sono in aperto contrasto: più un software è complesso, più è difficile garantirne il buon funzionamento.

Da qualche anno Daniel Bristot de Oliveria, manco a dirlo sviluppatore del Kernel, sta portando avanti una funzionalità che potrebbe essere di grande aiuto proprio per questo: Runtime Verification (RV – verifica in tempo reale). E, secondo lui, il lavoro è pronto per l’inclusione.
Semplificando molto, si tratta di una specie di debug automatico in tempo reale: si crea un modello di quali conseguenze debba avere una certa chiamata nel Kernel, e RV controllerà che ogni passaggio abbia il risultato aspettato.
In caso di discrepanza, potranno essere previste delle reazioni: un avvertimento all’utente per segnalare la cosa, azioni automatiche per rimediare al problema rilevato, il Kernel panic nei casi più gravi.

Normalmente questo tipo di approccio ha due grossi problemi:

1. la modellizzazione del risultato atteso è tanto più complessa quanto più è complesso il software da verificare;
2. i continui controlli creano un overhead tanto grande da relegarne l’uso solo in laboratorio, o comunque ambienti controllati.

Avrete capito che RV supera entrambi i limiti.
La modellizzazione utilizzata è modulare, permettendo di concatenare più verifiche puntuali (e quindi semplici) in un’unico modello complesso.
Ma soprattutto, grazie all’uso del sistema di tracing già integrato nel Kernel, l’overhead è limitato. tanto da poter essere usato in sistemi di produzione.

L’obbiettivo è quello di rendere Linux tanto affidabile da poter essere usato in condizioni critiche, dai sistemi di controllo degli aerei alla guida autonoma nelle macchine, o a sistemi medici salvavita. Non a caso, nelle prime patch proposte si faceva esplicito riferimento al progetto ELISA della Linux Foundation.

Vedremo quanto sarà davvero facile per gli sviluppatori usare queste funzioni, che hanno grandi potenzialità anche sotto il profilo della sicurezza. Insomma, potrebbe fare del bene anche a noi utenti desktop!