Sicurezza basata sulla lingua - Language-based security

In informatica , la sicurezza basata sul linguaggio ( LBS ) è un insieme di tecniche che possono essere utilizzate per rafforzare la sicurezza delle applicazioni ad alto livello utilizzando le proprietà dei linguaggi di programmazione. Si ritiene che LBS applichi la sicurezza del computer a livello di applicazione, consentendo di prevenire le vulnerabilità che la sicurezza del sistema operativo tradizionale non è in grado di gestire.

Le applicazioni software sono in genere specificate e implementate in determinati linguaggi di programmazione e, al fine di proteggere da attacchi, difetti e bug, il codice sorgente di un'applicazione potrebbe essere vulnerabile, è necessaria la sicurezza a livello di applicazione; sicurezza valutando il comportamento delle applicazioni rispetto al linguaggio di programmazione. Quest'area è generalmente nota come sicurezza basata sulla lingua.

Motivazione

L'uso di grandi sistemi software, come SCADA , sta prendendo piede in tutto il mondo e i sistemi informatici costituiscono il cuore di molte infrastrutture. La società fa grande affidamento su infrastrutture come acqua, energia, comunicazioni e trasporti, che ancora una volta si basano su sistemi informatici perfettamente funzionanti. Ci sono molti esempi ben noti di quando i sistemi critici falliscono a causa di bug o errori nel software, come quando la mancanza di memoria del computer ha causato il crash dei computer LAX e il ritardo di centinaia di voli (30 aprile 2014).

Tradizionalmente, i meccanismi utilizzati per controllare il corretto comportamento del software sono implementati a livello di sistema operativo. Il sistema operativo gestisce diverse possibili violazioni della sicurezza come violazioni di accesso alla memoria, violazioni di overflow dello stack, violazioni del controllo di accesso e molte altre. Questa è una parte cruciale della sicurezza nei sistemi informatici, tuttavia proteggendo il comportamento del software a un livello più specifico, è possibile ottenere una sicurezza ancora maggiore. Poiché molte proprietà e comportamenti del software vengono persi durante la compilazione, è molto più difficile rilevare le vulnerabilità nel codice macchina. Valutando il codice sorgente, prima della compilazione, è possibile considerare anche la teoria e l'implementazione del linguaggio di programmazione e scoprire ulteriori vulnerabilità.

"Allora perché gli sviluppatori continuano a commettere gli stessi errori? Invece di fare affidamento sulla memoria dei programmatori, dovremmo sforzarci di produrre strumenti che codifichino ciò che è noto sulle vulnerabilità di sicurezza comuni e lo integrino direttamente nel processo di sviluppo".

— D. Evans e D. Larochelle, 2002

Obiettivo della sicurezza basata sulla lingua

Utilizzando LBS, la sicurezza del software può essere aumentata in diverse aree, a seconda delle tecniche utilizzate. Errori di programmazione comuni, come il verificarsi di buffer overflow e flussi di informazioni illegali, possono essere rilevati e non consentiti nel software utilizzato dal consumatore. È inoltre auspicabile fornire al consumatore alcune prove sulle proprietà di sicurezza del software, rendendolo in grado di fidarsi del software senza dover ricevere il codice sorgente e controllarlo da solo per eventuali errori.

Un compilatore, prendendo il codice sorgente come input, esegue diverse operazioni specifiche della lingua sul codice per tradurlo in codice leggibile dalla macchina. Analisi lessicale , preelaborazione , parsing , analisi semantica , generazione di codice e ottimizzazione del codice sono tutte operazioni comunemente utilizzate nei compilatori. Analizzando il codice sorgente e utilizzando la teoria e l'implementazione del linguaggio, il compilatore tenterà di tradurre correttamente il codice di alto livello in codice di basso livello, preservando il comportamento del programma.

Image
Illustrare un compilatore di certificazione

Durante la compilazione di programmi scritti in un linguaggio indipendente dai tipi , come Java , il codice sorgente deve eseguire correttamente il controllo del tipo prima della compilazione. Se il controllo del tipo fallisce, la compilazione non verrà eseguita e il codice sorgente dovrà essere modificato. Ciò significa che, dato un compilatore corretto, qualsiasi codice compilato da un programma sorgente verificato con successo dovrebbe essere privo di errori di assegnazione non validi. Si tratta di informazioni che possono essere utili per il consumatore di codice, in quanto forniscono un certo grado di garanzia che il programma non si arresterà in modo anomalo a causa di un errore specifico.

Un obiettivo di LBS è garantire la presenza di determinate proprietà nel codice sorgente corrispondenti alla politica di sicurezza del software. Le informazioni raccolte durante la compilazione possono essere utilizzate per creare un certificato che può essere fornito al consumatore come prova di sicurezza nel programma dato. Tale prova deve implicare che il consumatore può fidarsi del compilatore utilizzato dal fornitore e che il certificato, le informazioni sul codice sorgente, possono essere verificate.

La figura illustra come la certificazione e la verifica del codice di basso livello potrebbero essere stabilite mediante l'uso di un compilatore di certificazione. Il fornitore del software ha il vantaggio di non dover rivelare il codice sorgente, lasciando al consumatore il compito di verificare il certificato, compito facile rispetto alla valutazione e compilazione del codice sorgente stesso. La verifica del certificato richiede solo una base di codice attendibile limitata contenente il compilatore e il verificatore.

tecniche

Analisi del programma

Articolo principale: Analisi del programma

Le principali applicazioni dell'analisi del programma sono l' ottimizzazione del programma (tempo di esecuzione, requisiti di spazio, consumo energetico, ecc.) e la correttezza del programma (bug, vulnerabilità della sicurezza, ecc.). L'analisi del programma può essere applicata alla compilazione ( analisi statica ), al runtime ( analisi dinamica ) oa entrambe. Nella sicurezza basata sul linguaggio, l'analisi del programma può fornire diverse funzioni utili, come: controllo del tipo (statico e dinamico), monitoraggio , controllo delle contaminazioni e analisi del flusso di controllo .

Analisi del flusso di informazioni

Articolo principale: flusso di informazioni

L'analisi del flusso di informazioni può essere descritta come un insieme di strumenti utilizzati per analizzare il controllo del flusso di informazioni in un programma, al fine di preservare la riservatezza e l' integrità laddove i normali meccanismi di controllo dell'accesso vengono a mancare.

"Disaccoppiando il diritto di accesso alle informazioni dal diritto di diffonderle, il modello di flusso va oltre il modello a matrice di accesso nella sua capacità di specificare un flusso di informazioni sicuro. Un sistema pratico richiede sia l'accesso che il controllo del flusso per soddisfare tutti i requisiti di sicurezza".

— D. Denning, 1976

Il controllo degli accessi impone controlli sull'accesso alle informazioni, ma non si preoccupa di ciò che accade dopo. Un esempio: un sistema ha due utenti, Alice e Bob. Alice ha un file secret.txt , che può essere letto e modificato solo da lei, e preferisce tenere queste informazioni per sé. Nel sistema esiste anche un file public.txt , che è libero di leggere e modificare per tutti gli utenti del sistema. Supponiamo ora che Alice abbia scaricato accidentalmente un programma dannoso. Questo programma può accedere al sistema come Alice, aggirando il controllo di accesso su secret.txt . Il programma dannoso copia quindi il contenuto di secret.txt e lo inserisce in public.txt , consentendo a Bob e a tutti gli altri utenti di leggerlo. Ciò costituisce una violazione della politica di riservatezza prevista del sistema.

Non interferenza

La non interferenza è una proprietà dei programmi che non perde o rivela informazioni di variabili con una classificazione di sicurezza più elevata , a seconda dell'input di variabili con una classificazione di sicurezza inferiore . Un programma che soddisfa la non interferenza dovrebbe produrre lo stesso output ogni volta che viene utilizzato lo stesso input corrispondente sulle variabili inferiori . Questo deve valere per ogni possibile valore sull'input. Ciò implica che anche se le variabili superiori nel programma hanno valori diversi da un'esecuzione all'altra, ciò non dovrebbe essere visibile sulle variabili inferiori .

Un utente malintenzionato potrebbe tentare di eseguire un programma che non soddisfa la non interferenza ripetutamente e sistematicamente per cercare di mapparne il comportamento. Diverse iterazioni potrebbero portare alla divulgazione di variabili più elevate e consentire all'attaccante di apprendere informazioni sensibili, ad esempio, sullo stato del sistema.

Se un programma soddisfa o meno la non interferenza può essere valutato durante la compilazione assumendo la presenza di sistemi di tipo sicurezza .

Sistema di tipo di sicurezza

Articolo principale: sistema di tipo di sicurezza

Un sistema di tipi di sicurezza è un tipo di sistema di tipi che può essere utilizzato dagli sviluppatori di software per verificare le proprietà di sicurezza del loro codice. In un linguaggio con tipi di sicurezza, i tipi di variabili ed espressioni si riferiscono alla politica di sicurezza dell'applicazione e i programmatori possono essere in grado di specificare la politica di sicurezza dell'applicazione tramite dichiarazioni di tipo. I tipi possono essere utilizzati per ragionare su vari tipi di criteri di sicurezza, inclusi criteri di autorizzazione (come controllo dell'accesso o funzionalità) e sicurezza del flusso di informazioni. I sistemi di tipo di sicurezza possono essere formalmente correlati alla politica di sicurezza sottostante e un sistema di tipo di sicurezza è valido se tutti i programmi che effettuano il controllo di tipo soddisfano la politica in senso semantico. Ad esempio, un sistema di tipo di sicurezza per il flusso di informazioni potrebbe imporre la non interferenza, il che significa che il controllo del tipo rivela se c'è una violazione della riservatezza o dell'integrità nel programma.

Protezione del codice di basso livello

Le vulnerabilità nel codice di basso livello sono bug o difetti che porteranno il programma in uno stato in cui l'ulteriore comportamento del programma non è definito dal linguaggio di programmazione sorgente. Il comportamento del programma di basso livello dipenderà dal compilatore, dal sistema di runtime o dai dettagli del sistema operativo. Ciò consente a un utente malintenzionato di guidare il programma verso uno stato indefinito e sfruttare il comportamento del sistema.

Gli exploit comuni di codice di basso livello non sicuro consentono a un utente malintenzionato di eseguire letture o scritture non autorizzate su indirizzi di memoria. Gli indirizzi di memoria possono essere casuali o scelti dall'attaccante.

Utilizzo di lingue sicure

Un approccio per ottenere un codice di basso livello sicuro consiste nell'utilizzare linguaggi di alto livello sicuri. Un linguaggio sicuro è considerato completamente definito dal manuale dei suoi programmatori. Qualsiasi bug che potrebbe portare a un comportamento dipendente dall'implementazione in un linguaggio sicuro verrà rilevato in fase di compilazione o porterà a un comportamento di errore ben definito in fase di runtime. In Java , se si accede a un array fuori dai limiti, verrà generata un'eccezione. Esempi di altri linguaggi sicuri sono C# , Haskell e Scala .

Esecuzione difensiva di lingue non sicuresafe

Durante la compilazione di un linguaggio non sicuro, i controlli runtime vengono aggiunti al codice di basso livello per rilevare un comportamento non definito a livello di origine. Un esempio è l'uso di canaries , che può terminare un programma quando scopre violazioni dei limiti. Uno svantaggio dell'utilizzo dei controlli in fase di esecuzione come il controllo dei limiti è che impongono un notevole sovraccarico delle prestazioni.

La protezione della memoria , ad esempio l'utilizzo di stack e/o heap non eseguibili, può essere considerata anche come controlli aggiuntivi in ​​fase di esecuzione. Questo è utilizzato da molti sistemi operativi moderni.

Esecuzione isolata dei moduli

L'idea generale è identificare il codice sensibile dai dati dell'applicazione analizzando il codice sorgente. Fatto ciò, i diversi dati vengono separati e collocati in moduli differenti. Nell'assumere che ogni modulo abbia il controllo totale sulle informazioni sensibili che contiene, è possibile specificare quando e come dovrebbe lasciare il modulo. Un esempio è un modulo crittografico che può impedire alle chiavi di lasciare il modulo non crittografato.

Compilazione certificativa

Certificare la compilazione è l'idea di produrre un certificato durante la compilazione del codice sorgente, utilizzando le informazioni dalla semantica del linguaggio di programmazione di alto livello. Questo certificato dovrebbe essere allegato al codice compilato al fine di fornire una forma di prova al consumatore che il codice sorgente è stato compilato secondo un determinato insieme di regole. Il certificato può essere prodotto in diversi modi, ad esempio tramite codice di trasporto di prova (PCC) o linguaggio di assemblaggio tipizzato (TAL).

Codice di prova

Gli aspetti principali del PCC possono essere riassunti nei seguenti passaggi:

  1. Il fornitore fornisce un programma eseguibile con varie annotazioni prodotte da un compilatore di certificazione .
  2. Il consumatore fornisce una condizione di verifica, basata su una politica di sicurezza . Questo viene inviato al fornitore.
  3. Il fornitore esegue la condizione di verifica in un prover di teoremi per fornire una prova al consumatore che il programma soddisfa effettivamente la politica di sicurezza.
  4. Il consumatore esegue quindi la prova in un correttore di prove per verificare la validità della prova.

Un esempio di compilatore di certificazione è il compilatore Touchstone , che fornisce una prova formale PCC della sicurezza del tipo e della memoria per i programmi implementati in Java.

Linguaggio assembly digitato

TAL è applicabile ai linguaggi di programmazione che fanno uso di un sistema di tipi . Dopo la compilazione, il codice oggetto conterrà un'annotazione di tipo che può essere verificata da un normale controllore di tipo. L'annotazione qui prodotta è per molti versi simile alle annotazioni fornite da PCC, con alcune limitazioni. Tuttavia, TAL può gestire qualsiasi politica di sicurezza che può essere espressa dalle restrizioni del sistema di tipi, che possono includere la sicurezza della memoria e il flusso di controllo, tra gli altri.

seminari

Riferimenti

Libri

  • G. Barthe, B. Grégoire, T. Rezk, Raccolta di certificati , 2008
  • Brian Chess e Gary McGraw, Analisi statica per la sicurezza , 2004.

Ulteriori letture