Qualificare la libreria standard del linguaggio C per l’utilizzo in applicazioni di sicurezza critiche

• 
• Tweet
• Pin It
• Condividi per email

Marcel Beemster, CTO, Solid Sands

Introduzione

Le soluzioni software svolgono un ruolo sempre più importante nei sistemi di sicurezza, dove eventuali disfunzioni del software comportano attualmente sia rischi di responsabilità giuridica, sia minacce concrete in termini di lesioni, decessi, interruzione di servizi essenziali o danni ambientali.

Organizzazioni come ISO e Commissione Elettrotecnica Internazionale (IEC) hanno pubblicato standard adottati su larga scala per certificare la sicurezza dei software. Alcuni esempi sono ISO 26262 (Veicoli stradali – Sicurezza funzionale) per l’industria automobilistica, EN 50128 (Sistemi di comunicazione, segnalazione ed elaborazione. Software per sistemi di controllo e protezione ferroviari) per i trasporti ferroviari, e IEC 61508 (Sicurezza funzionale dei sistemi di sicurezza elettrici/elettronici/elettronici programmabili) per le applicazioni industriali.

Gli sviluppatori di applicazioni devono dimostrare che il software, così come i metodi, i processi e l’insieme di programmi (toolchain) utilizzati per svilupparlo, siano conformi agli standard vigenti. Tuttavia, gran parte della toolchain esula dal controllo dello sviluppatore e richiede quindi una convalida del compilatore. Pochi compilatori sono privi di difetti (bug); pertanto, sapendo che cosa non funziona, si possono evitare errori.

Gran parte del codice sorgente, che finisce tipicamente in un codice binario compilato, non passa mai attraverso il compilatore con una combinazione sempre identica di casi d’uso, opzioni di compilazione e ambiente hardware di destinazione. Parte di questo codice comprende funzioni di libreria precompilate, come ad esempio quelle nella Libreria Standard del C (libc) spesso fornite in formato binario all’interno di un kit di sviluppo software (SDK).

L’inclusione di macro rende in molti casi i componenti della libreria sensibili al tipo di utilizzo. Anche in una libreria prequalificata dal fornitore del SDK utilizzando lo stesso compilatore fornito con il SDK, non è detto che siano stati rispettati lo stesso caso di utilizzo, le stesse opzioni del compilatore e gli stessi requisiti dell’ambiente hardware di destinazione, rendendo così difficile dimostrare la conformità.

Per risolvere questo problema, la SuperGuard C Library Safety Qualification Suite offre piena tracciabilità per risalire dai risultati di singoli test ai requisiti derivati dalla specifica del linguaggio C a norma ISO. Può inoltre supportare la qualificazione delle implementazioni della Libreria Standard del C per applicazioni critiche di sicurezza, sia per librerie di terze parti non modificate, sia per implementazioni sviluppate o mantenute autonomamente.

Obiettivo della qualificazione

La qualificazione della libreria software è importante perché il codice della libreria viene integrato nell’applicazione e installato sul dispositivo target. Un componente difettoso della libreria metterebbe quindi a rischio la sicurezza funzionale dell’intera applicazione. Gli obiettivi di utilizzo della libreria software all’interno degli standard di sicurezza funzionale hanno solitamente uno scopo condiviso: verificare che l’implementazione della libreria sia conforme alle specifiche. Ad esempio, ISO 26262 prevede due percorsi di qualificazione della libreria, descritti nella ISO 26262 Parte 8 e nella ISO 26262 Parte 6. SuperGuard funziona in entrambi i casi.

Come vengono sviluppati i test con SuperGuard

Quando si effettuano test basati su requisiti così come raccomandato nella Parte 8 e nella Parte 6 della ISO 26262, il problema principale per le specifiche della Libreria Standard del C è che, pur fornendo una descrizione dettagliata del comportamento di ogni funzione, nessuna delle due parti definisce requisiti chiari. I requisiti devono quindi essere ricavati dalle descrizioni.

SuperGuard incorpora la suite collaudata per i test sulla Libreria Standard del C messa a disposizione dalla suite di collaudo e verifica del compilatore Super Test di Solid Sands.

I test di SuperGuard, idonei per un’ampia gamma di ambienti di sviluppo, verificano che il comportamento in fase di implementazione sia conforme alle specifiche della libreria. Ciascun test esegue il costrutto o la funzione sotto esame e confronta i risultati dell’esecuzione con i risultati attesi (“modello”) definiti nella specifica della libreria. Il test stesso comunica l’esito positivo o negativo al driver del test.

Per verificare il comportamento in fase di implementazione, i test vengono compilati ed eseguiti in un ambiente di esecuzione, in modo tale che l’intera toolchain, compreso il processore target, sia coinvolta in ciascun test. SuperGuard risulta così idoneo per verificare la libreria coinvolgendo anche l’hardware (hardware-in-the-loop).

I test per la parte “freestanding” della libreria (tipicamente utilizzata nei sistemi a metallo nudo) richiedono risorse minime. La maggior parte dei test SuperGuard può girare su sistemi con meno di 4K di memoria: SuperGuard risulta quindi idonea per sistemi embedded molto piccoli.

Per implementare i test basati su requisiti, SuperGuard scompone le specifiche della Libreria Standard del C in requisiti di implementazione testabili, insieme a specifiche di collaudo che descrivono come viene testato ogni requisito. Ricollegando i risultati di esecuzione dei singoli test alla specifica di test, al requisito e alla funzione di libreria standard corrispondenti, SuperGuard offre piena tracciabilità dei test basati su requisiti. Per fornire evidenza di completezza, SuperGuard offre una copertura del codice strutturale quasi del 100% per oltre l’80% delle funzioni, con un livello elevato di Modified Condition/Decision Coverage (MC/DC).

All’interno di SuperGuard, i requisiti e le specifiche di test sono documentati per i test della libreria C, come era già possibile con la suite SuperTest.

Un esempio

Ogni test di libreria di SuperGuard viene sviluppato secondo una metodologia omogenea. Questa è la specifica nella Sezione 7.21.2.4 della definizione di linguaggio C99:

7.21.2.4 La funzione strncpy

Sinopsi

1 #include <string.h>
char * strncpy(char * restrict s1, const char * restrict s2, size_t n);

Descrizione

2 La funzione strncpy copia non più di n caratteri (i caratteri che seguono un carattere nullo non vengono copiati) dall’array puntato da s2 all’array puntato da s1. Se la copiatura avviene fra oggetti che si sovrappongono, il comportamento è indefinito.

3 Se l’array puntato da s2 è una stringa più corta di n caratteri, i caratteri nulli vengono aggiunti alla copia nell’array puntato da s1, fino a che non sono stati scritti n caratteri in tutto.

Ritorno

4 La funzione strncpy restituisce il valore di s1.

Il punto chiave è che il Paragrafo 2 specifica che cosa non fa strncpy().Come abbiamo letto in precedenza: “copia non più di n caratteri.” Non viene mai richiesto che vengano copiati caratteri da s2 a s1. Il Paragrafo 3 stabilisce un’azione, cioè che s1 venga completata con caratteri nulli. Un’implementazione letteralmente corretta secondo questa indicazione sarebbe scrivere n caratteri nulli in s1.

Tuttavia non è questo ciò che la funzione dovrebbe fare. Il principio generale è che la funzione copi il maggior numero di caratteri possibile da s2 a s1 fino a esaurimento della stringa s2 o di n. Ma, per definire requisiti, bisogna essere più precisi.

Il primo passo nello sviluppo di test è estrarre un set di requisiti (REQ) da questa descrizione, considerando ciò che la funzione dovrebbe realmente fare. Nel dettaglio:

REQ-copystring: Se s2 punta a una stringa con lunghezza ‘l2‘ (definita da strlen()) inferiore a n, strncpy() deve copiare l2 caratteri, in sequenza, dall’array s2 all’array s1.

REQ-copyn: Se s2 non punta a una stringa con lunghezza inferiore a n, strncpy() deve copiare i primi n caratteri, in sequenza, dall’array s2 all’array s1.

REQ-shorter: Se s2 punta a una stringa con lunghezza inferiore a n, strncpy() deve aggiungere caratteri nulli (‘\0’) dopo i caratteri copiati nell’array s1 finché non sono stati scritti n caratteri in totale.

REQ-nomore: strncpy() non deve scrivere nell’array di destinazione s1 oltre i primi n caratteri.

REQ-nochange: strncpy() non deve modificare l’array s2.

REQ-return: strncpy() deve restituire il valore di s1.

Il requisito REQ-nochange discende dalla dichiarazione di s2 come array costante, ma questo non garantisce che un’implementazione di strncpy() non scriva su s2.

Per ogni requisito viene quindi sviluppata una specifica di test, che definisce come un test verifica che il requisito sia vero. Una singola specifica di test si traduce solitamente in diversi casi di test che coprono le aree di input e output della funzione. I casi di test vengono implementati dal test. La specifica di test collega il requisito ai test.

Ad esempio, le specifiche di test per i requisiti REQ-copystring e REQ-nomore sono le seguenti:

Specifica di test per REQ-copystring: Chiama la funzione strncpy() con diversi valori per il parametro n (incluso n==0) uguale alla e maggiore della lunghezza della stringa di origine. Verificare che la stringa di origine venga copiata nell’array di destinazione fino al carattere nullo di terminazione.

Specifica di test per REQ-nomore: Per tutti i casi di test, verificare che il carattere con indice n nell’array di destinazione s1 non sia modificato. Se coincide con il test, verificare anche che nessun carattere oltre n sia modificato.

Qui, la specifica di test REQ-nomore viene implementata nello stesso file di test come gli altri casi di test per strncpy().Poiché il requisito deve reggere incondizionatamente per ogni chiamata a strncpy(), invece di creare nuovi test per questa specifica di test, essa viene implementata semplicemente aggiungendo un controllo ulteriore su ogni test di caso per gli altri requisiti, invece di creare nuovi test.

Gestire file di intestazione e funzioni come macro

Non tutte le funzioni nella Libreria Standard del C vengono implementate solo come codici binari precompilati. Molte dipendono anche dalle informazioni contenute nei file di intestazione sorgente. Questi definiscono tipi, variabili globali e macro, e fanno parte della libreria tanto quanto le funzioni (precompilate) della libreria. Molte funzioni vengono implementate sia come funzioni reali, sia come macro. Ai fini della velocità e dell’efficienza, è abitudine comune utilizzare le implementazioni macro. SuperGuard testa entrambe.

Diversamente dai codici binari corrispondenti, funzioni come le macro non sono precompilate, ma generate dal compilatore del SDK con il codice sorgente dell’applicazione. Pertanto è vitale che, insieme ad altri contenuti del file di intestazione, esse vengano verificate per il caso d’uso specifico di una data applicazione.

SuperGuard dispone di ampie funzionalità di report

Analisi della copertura del codice

In SuperGuard, particolare attenzione viene prestata alla copertura del codice ottenuta per un’implementazione open-source matura e popolare della Libreria Standard del C, per soddisfare il requisito ASIL D del comma 12.4.2.3. Per molte funzioni presenti in quella libreria, SuperGuard raggiunge una copertura del 100%, oltre a un’elevata copertura MC/DC.

Ogni implementazione di libreria è diversa, ma tutte gestiscono un’analisi dei casi simile. L’elevata copertura del codice di Standard Library offre benefici per tutte le implementazioni della Libreria Standard del C.

Casi anomali

I test di SuperGuard gestiscono i casi anomali in due modi. Il primo riguarda un comportamento definito derivante da un input anomalo; ad esempio, passare un numero negativo alla funzione sqrt() deve restituire il valore NaN (presumendo IEC 60559 aritmetica). Per quanto anomalo, il comportamento della funzione è pienamente definito e può essere verificato.

Il secondo modo riguarda i requisiti che il compilatore può verificare. Ad esempio, se una funzione deve avere un tipo di ritorno vuoto, un test può provare a utilizzare il valore di ritorno attendendosi che generi un errore del compilatore. SuperGuard definisce queste prove X-Test. Gli X-Test VENGONO SUPERATI se il compilatore rileva un errore in compilazione, mentre FALLISCONO in caso contrario. Gli X-Test non vengono mai eseguiti.

Riepilogo

Gli sviluppatori software non devono dare per scontato che strumenti e componenti di terze parti e/o commerciali da scaffale (COTS), come compilatori e librerie standard, siano privi di errori, o che la prequalificazione dia questa certezza.

SuperGuard offre la tracciabilità necessaria per ricollegare i risultati dei test basati su requisiti alla specifica della Libreria Standard del C. La piena tracciabilità viene garantita scomponendo le specifiche funzionali della Libreria Standard ISO C in requisiti chiaramente definiti, sviluppando specifiche di test idonee e implementandole secondo lo standard richiesto. Inoltre, consente agli sviluppatori di eseguire test nello stesso ambiente di sviluppo, alle stesse condizioni di caso d’uso e sullo stesso hardware di destinazione utilizzato nella loro applicazione, con una copertura del codice strutturale vicina al 100%. Generando un report di qualificazione completo ritagliato sulle esigenze degli enti di certificazione, SuperGuard aiuta a dimostrare l’integrità dei componenti della libreria utilizzati in applicazioni safety-critical.

Maggiori informazioni sui prodotti e sui servizi dell’azienda sono disponibili al sito www.solidsands.nl.  

• 
• Tweet
• Pin It
• Condividi per email