Forse a questa risposta si può rispondere con una domanda più generale, ad esempio quali programmi possono essere provati sicuri .
Può essere (o è stato) dimostrato formalmente che una sandbox è sicura?
Forse a questa risposta si può rispondere con una domanda più generale, ad esempio quali programmi possono essere provati sicuri .
Può essere (o è stato) dimostrato formalmente che una sandbox è sicura?
Il termine "sandbox" è ampio, generico e spesso usato male e frainteso.
Consideriamo un tipo di sandbox, una macchina virtuale che funziona sotto il controllo di un hypervisor . Il sistema ospite è nominalmente isolato e non può "vedere" il sistema host. Tuttavia, questo è relativo all'implementazione dell'hypervisor, che è una combinazione di software e hardware, entrambi i quali sono suscettibili di bug (l'hardware è sempre coinvolto nel fatto che il tutto, in definitiva, funziona su una CPU, non sto parlando di utilizzare o non utilizzare gli opcode AMD-V / Intel-VT). Le fughe dagli hypervisor sono avvenute . "Dimostrare" che l'hypervisor sia corretto significherebbe dimostrare che è privo di errori. Dimostrare che il software è privo di bug è stato un obiettivo piuttosto elusivo per l'ultimo mezzo secolo ... e per l'hardware, ancora di più.
Inoltre, sandbox non equivalgono alla sicurezza . Perché una sandbox sia utile, deve avere poche porte aperte: si esegue un po 'di software nella sandbox, ma si vorrà vedere il risultato, che si tratti di qualcosa visualizzato, di file salvati da qualche parte o di alcune attività di rete. Quando le persone usano un browser Web in una sandbox, vogliono che il browser, ad esempio, cerchi il Web, in modo che le connessioni di rete esterne dalla sandbox debbano essere consentite; e il browser sandboxed deve anche avere la possibilità di visualizzare le cose, quindi ha accesso all'hardware grafico (probabilmente un accesso controllato, ma se si desidera l'accelerazione 3D, i controlli severi diventano difficili). Vuoi una sandbox perché sospetti che il browser possa essere sovvertito e dirottato da un utente malintenzionato. Ma, a quel punto, hai già perso (non tutta la guerra, ma comunque battaglie significative): il browser sovvertito, sandbox o no, è in grado di rete e può essere usato come relay per attaccare altri siti o inviare spam, apparentemente originario da il tuo indirizzo.
In più parole di successo, l'amputazione non è il tipo di medicina che si consiglia in ultima analisi.
Vediamo un altro tipo di sandbox, la Java Virtual Machine e il suo supporto per le applet. Ha due aspetti principali:
Il "codice" non è codice binario grezzo per la CPU locale, ma "bytecode": opcodes per una macchina concettuale e astratta, che vive in un mondo non hardware in cui non sono consentiti aritmetica generica del puntatore. I riferimenti hanno tipi non cancellabili e gli accessi agli array sono controllati dai limiti.
Le funzionalità di accesso esterno per il codice dell'applet sono limitate: le connessioni di rete possono essere effettuate solo al server di origine; i file locali non possono essere letti o scritti; e così via.
Quando il bytecode deve essere eseguito, è prima analizzato : l'implementazione JVM esegue un'analisi del flusso di controllo che dimostra formalmente (sì, nel senso di "sicurezza dimostrabile") che il codice è conforme a le regole di tipo per bytecode (vale a dire che non chiama mai un metodo su un oggetto che non presenta quel metodo). Ciò consente la traduzione di un codice nativo efficiente, senza la necessità di hardware di virtualizzazione specializzato. Inoltre, protegge da molti tipi di sovversione (i buffer overflow vengono rilevati in modo affidabile, non c'è un puntatore pendente o double-free a causa di Gestione della memoria basata su GC ...). Questo tipo di protezione non è sufficiente per "sicurezza" perché desideri comunque i controlli di accesso (ad esempio il blocco delle connessioni esterne eccetto il server di origine) che vengono applicate dalle classi di sistema. L'analisi bytecode serve a garantire che vengano utilizzate solo le classi di sistema e che vengano utilizzate correttamente; il resto è fino alle classi di sistema.
Ovviamente, oltre la storia di Java, sia l'analizzatore bytecode che le implementazioni delle classi di sistema hanno riscontrato difetti. Non sono intrinseci: ciò che cercano di ottenere non è matematicamente impossibile. Ma diciamocelo: gli errori capitano. La JVM è un software piuttosto complesso che è ben lungi dall'essere privo di errori. Inoltre, la JVM viene eseguita all'interno di un sistema operativo e su hardware tangibile, nessuno dei quali è privo di errori.
Questo illustra i miei punti:
Supponi di aver dimostrato che la tua sandbox è immune da tutti gli attacchi . Se questa dimostrazione fosse stata fatta circa 10 anni fa, non avrebbe preso in considerazione il puntatore pendente e padding oracle attacca perché questi metodi di sfruttamento erano sconosciuti al momento. Perciò non avresti potuto dimostrare che questa sandbox era totalmente sicura, in quanto sarebbe una contraddizione - > < -
La tua domanda sembra indicare un fraintendimento di cosa sia la sicurezza. La sicurezza provata è un ossimoro. Niente può mai essere completamente sicuro, o come fa il vecchio scherzo della sicurezza IT, l'unica memoria sufficientemente sicura sta scrivendo su dev / null (cioè, distruzione). La sicurezza è semplicemente un gioco di risorse e costi. Cerca di bilanciare la necessità che gli utenti legittimi ricevano le informazioni evitando che gli attaccanti facciano lo stesso, ma con qualsiasi accesso consentito, dati risorse e tempo sufficienti, sarà sempre possibile o almeno fattibile per rompere il sistema e ottenere l'accesso.
I sistemi autodistruttivi sono un tentativo di evitare questo problema limitando la quantità di accesso che può essere fatto, ma i mezzi inventivi possono eludere la maggior parte di questi e hanno risorse e sforzi abbastanza significativi (a volte fino al livello degli strati effettivamente in dissoluzione di chip, strato per strato).
La domanda ha davvero bisogno di ulteriori chiarimenti per poter rispondere. Vuoi forse dire che può essere provata la protezione contro un particolare tipo di attacco? Se sì, quali tipi di attacchi ti preoccupano?
Dipende dal tipo di sicurezza dimostrabile di cui parli (sia per il suo impossibile che per il non senso). Ma negli algoritmi di sicurezza la sicurezza dimostra che per rompere il tuo algoritmo qualcuno ha bisogno di interrompere la crittografia sottostante. Quindi se pensiamo al nostro cripto-alg come a uno sicuro, e scrivi una dimostrazione che solo rompendo la cripto sarai in grado di rompere il tuo algoritmo allora non significa niente, è solo qualcosa che può essere ricercato e pubblicato niente di più . E sono d'accordo con gli schemi di attacco di Rook che si stanno evolvendo, una prova per ora non sarà sicura entro un decennio o giù di lì.