it-swarm-eu.dev

È possibile un software privo di exploit?

Ho sentito che ci saranno sempre vulnerabilità nei codici, nel software. Tuttavia, non capisco perché non sia possibile avere un software privo di exploit. Se le aziende continuano ad aggiornare il loro software, alla fine non ci saranno vulnerabilità, giusto?

139
Zheer

Il software è troppo complesso

Questo è di gran lunga il fattore più importante. Anche se si guarda a qualcosa come un'applicazione web, la quantità di ore lavorative inserite nella base di codice è immensa. Il codice funziona con le tecnologie, i cui standard sono pagine su pagine lunghe, scritte decenni fa, e che offre funzionalità di cui la maggior parte degli sviluppatori non ha mai nemmeno sentito parlare.

Combinalo con il fatto che il software moderno è basato su librerie, che sono costruite su librerie, che astraggono alcune librerie di basso livello basate su alcune funzionalità del sistema operativo, che di nuovo è solo un wrapper per alcune altre funzioni del sistema operativo scritte negli anni '90.

Il moderno stack tecnologico è semplicemente troppo grande per essere completamente grokato da una persona, anche se si esclude il lato OS delle cose, il che porta al punto successivo:

La conoscenza si perde nel tempo

Le iniezioni SQL hanno ora 20 anni. Sono ancora in giro. In che modo? Un fattore da considerare è che la conoscenza all'interno di un'azienda si perde nel tempo. Potresti avere uno o due sviluppatori senior, che conoscono e si preoccupano della sicurezza, che si assicurano che il loro codice non sia vulnerabile alle iniezioni di SQL, ma questi anziani alla fine assumeranno posizioni diverse, cambieranno aziende o andranno in pensione. Le nuove persone prenderanno il loro posto e potrebbero essere altrettanto bravi sviluppatori, ma non sanno né si preoccupano della sicurezza. Di conseguenza, potrebbero non conoscere o preoccuparsi del problema e quindi non cercarli.

Alle persone viene insegnato nel modo sbagliato

Un altro punto è che la sicurezza non è davvero qualcosa che interessa alle scuole. Ricordo la prima lezione sull'uso di SQL in Java e il mio insegnante ha usato la concatenazione di stringhe per inserire parametri in una query. Gli ho detto che era insicuro e sono stato urlato per aver disturbato la lezione. Tutti gli studenti di questa classe hanno visto che la concatenazione delle stringhe è la strada da percorrere - dopo tutto, è così che ha fatto l'insegnante, e l'insegnante non avrebbe mai insegnato nulla di male, giusto?

Tutti quegli studenti ora andrebbero nel mondo dello sviluppo e scriverebbero felicemente codice SQL facilmente iniettabile, solo perché a nessuno importa. Perché a nessuno importa? Perché

Le aziende non sono interessate al "codice perfetto"

È un'affermazione audace, ma è vera. Per un'azienda, si preoccupano degli investimenti e dei rendimenti. "Investono" il tempo dei loro sviluppatori (che costa all'azienda una specifica quantità di denaro) e si aspettano in cambio funzionalità che possono vendere ai clienti. Le caratteristiche da vendere includono:

  • Il software ora può funzionare con più formati di file
  • Il software ora include gli acquisti in-app
  • Il software sembra migliore
  • Il software ti fa sembrare migliore
  • Il software funziona più velocemente
  • Il software si integra perfettamente nel flusso di lavoro

Ciò che le aziende non possono venderti è l'assenza di bug. "Il software non è vulnerabile contro XSS" non è qualcosa che puoi vendere, e quindi non è qualcosa in cui le aziende vogliono investire denaro. Risolvere i problemi di sicurezza è molto simile a fare il bucato: nessuno ti paga per farlo, nessuno ti loda per averlo fatto, e probabilmente non hai voglia di farlo comunque, ma devi comunque farlo.

E un altro punto finale:

Non è possibile verificare l'assenza di bug

Ciò significa che non si può mai essere certi che il codice contenga bug. Non puoi provare che alcuni software siano sicuri, perché non riesci a vedere quanti bug rimangono. Lasciami dimostrare questo:

function Compare(string a, string b)
{
    if (a.Length != b.Length)
    {
        // If the length is not equal, we know the strings will not be equal
        return -1;
    }
    else
    {
        for(int i = 0; i < a.Length; i++)
        {
            if(a[i] != b[i])
            {
                // If one character mismatches, the string is not equal
                return -1;
            }
        }

        // Since no characters mismatched, the strings are equal
        return 0;
    }
}

Questo codice ti sembra sicuro? Potresti pensarlo. Restituisce 0 se le stringhe sono uguali e -1 se non lo sono. Allora, qual'è il problema? Il problema è che se viene usato un segreto costante per una parte e input controllato dall'attaccante per l'altra, un utente malintenzionato può misurare il tempo necessario per il completamento della funzione. Se i primi 3 caratteri corrispondono, ci vorrà più tempo che se nessun personaggio corrisponde.

Ciò significa che un utente malintenzionato può provare vari input e misurare il tempo necessario per il completamento. Più tempo impiega, più caratteri consecutivi sono identici. Con abbastanza tempo, un utente malintenzionato può infine scoprire qual è la stringa segreta. Questo si chiama attacco del canale laterale .

Questo bug potrebbe essere corretto? Sì, naturalmente. Qualsiasi bug può essere corretto. Ma il punto di questa dimostrazione è mostrare che i bug non sono necessariamente chiaramente visibili e correggerli richiede che tu ne sia consapevole, sappia come correggerli e abbia l'incentivo a farlo.

In sintesi...

So che questo è un post lungo, quindi non ti biasimo per aver saltato fino alla fine. La versione rapida è che scrivere codice senza exploit è davvero difficile e diventa esponenzialmente più difficile quanto più il tuo software diventa complesso. Ogni tecnologia utilizzata dal tuo software, sia esso web, XML o qualcos'altro, fornisce alla tua base di codice migliaia di vettori di sfruttamento aggiuntivi. Inoltre, al tuo datore di lavoro potrebbe non interessare nemmeno la produzione di codice privo di exploit: si preoccupano delle funzionalità che possono vendere. E infine, puoi mai davvero essere sicuro che sia privo di exploit? O stai solo aspettando che il prossimo grande exploit colpisca il pubblico?

266
MechMK1

Le risposte esistenti, al momento della stesura di questo, si sono concentrate sulle difficoltà di creare codice privo di bug e sul perché non è possibile.

Ma immagina se fosse possibile. Quanto potrebbe essere difficile. C'è un software là fuori che si è guadagnato il titolo di "bug free:" il microkernel L4. Possiamo usarlo per vedere fino a che punto arriva la tana del coniglio.

seL4 è un microkernel. È unico perché, nel 2009, ha dimostrato di non avere bug. Ciò significa che hanno usato un sistema di prova automatizzato per dimostrare matematicamente che se il codice è compilato da un compilatore conforme agli standard, il binario risultante farà esattamente ciò che la documentazione del linguaggio dice che farà. Questo è stato rafforzato in seguito per rendere asserzioni simili del binario ARM del microkernel:

Il codice binario del ARM del microkernel seL4 implementa correttamente il comportamento descritto nella sua specifica astratta e nient'altro. Inoltre, la specifica e il binario seL4 soddisfano le classiche proprietà di sicurezza chiamate integrità e riservatezza .

Eccezionale! Abbiamo un software non banale che è provato per essere corretti. Qual è il prossimo?

Bene, le persone seL4 non ci stanno mentendo. Indicano quindi immediatamente che questa prova ha dei limiti ed enumera alcuni di questi limiti

Assembly: il kernel seL4, come tutti i kernel del sistema operativo, contiene del codice Assembly, circa 340 righe di ARM Assembly nel nostro caso. Per seL4, ciò riguarda principalmente l'entrata e l'uscita dal kernel, nonché gli accessi diretti all'hardware. Per la prova, supponiamo che questo codice sia corretto.
Hardware: supponiamo che l'hardware funzioni correttamente. In pratica, ciò significa che si presume che l'hardware non sia manomesso e funzioni secondo le specifiche. Significa anche che deve essere eseguito nelle sue condizioni operative.
Gestione dell'hardware: la prova fa solo le ipotesi più minime sull'hardware sottostante. Si sottrae dalla coerenza della cache, colorazione della cache e gestione TLB (translation lookaside buffer). La dimostrazione presuppone che queste funzioni siano implementate correttamente nel livello Assembly sopra menzionato e che l'hardware funzioni come pubblicizzato. La dimostrazione presuppone anche che soprattutto queste tre funzioni di gestione dell'hardware non abbiano alcun effetto sul comportamento del kernel. Questo è vero se vengono utilizzati correttamente.
Codice di avvio: la prova al momento riguarda il funzionamento del kernel dopo che è stato caricato correttamente in memoria e portato in modo coerente, stato iniziale minimo. Questo esclude circa 1.200 righe della base di codice che un programmatore del kernel normalmente considererebbe parte del kernel.
Memoria virtuale: secondo lo standard dei progetti di verifica formale "normali", la memoria virtuale non deve essere considerata un presupposto di questa prova . Tuttavia, il grado di affidabilità è inferiore rispetto ad altre parti della nostra prova in cui ragioniamo dal primo principio. Più in dettaglio, la memoria virtuale è il meccanismo hardware che il kernel utilizza per proteggersi da programmi utente e programmi utente l'uno dall'altro. Questa parte è completamente verificata. Tuttavia, la memoria virtuale introduce una complicazione, poiché può influire sul modo in cui il kernel stesso accede alla memoria. Il nostro modello di esecuzione assume un certo comportamento standard della memoria mentre il kernel viene eseguito e giustificiamo questo presupposto dimostrando le condizioni necessarie sul comportamento del kernel. Il fatto è: devi fidarti di noi che abbiamo ottenuto tutte le condizioni necessarie e che le abbiamo fatte bene. La nostra prova controllata dalla macchina non ci obbliga a essere completi a questo punto. In breve, in questa parte della dimostrazione, a differenza delle altre parti, esiste un potenziale errore umano.
...

L'elenco continua. Tutti questi avvertimenti devono essere attentamente considerati quando si richiede la prova della correttezza.

Ora dobbiamo dare credito al team seL4. Una tale prova è un'incredibile dichiarazione di fiducia. Ma mostra dove va la tana del coniglio quando inizi ad avvicinarti all'idea di "bug free". Non ottieni mai "bug free". Inizi a dover considerare seriamente classi più grandi di bug.

Alla fine ti imbatterai nel problema più interessante e umano di tutti: stai usando il software giusto per il lavoro? seL4 offre diverse grandi garanzie. Sono quelli di cui avevi davvero bisogno? La risposta di MechMK1 evidenzia un attacco temporale a un certo codice. Le prove di seL4 non includono esplicitamente la difesa contro quelle. Se sei preoccupato per tali attacchi di temporizzazione, seL4 non garantisce nulla al riguardo. Hai usato lo strumento sbagliato.

E, se guardi alla storia degli exploit, è pieno di squadre che hanno usato lo strumento sbagliato e sono state bruciate per questo.

†. In risposta ai commenti: le risposte parlano in realtà per sfruttare il codice libero. Tuttavia, direi che una prova del fatto che il codice è privo di bug è necessaria per provare che è privo di exploit.

92
Cort Ammon

Puoi avere un codice di alta qualità, ma diventa enormemente più costoso svilupparlo. Il software Space Shuttle era sviluppato , con grande cura e test rigorosi, risultante in un software molto affidabile - ma molto più costoso di uno PHP.

Alcune cose quotidiane sono anche molto ben codificate. Ad esempio, lo stack TCP/IP di Linux è piuttosto solido e ha avuto pochi problemi di sicurezza (anche se sfortunatamente, uno recentemente ) Altri software ad alto rischio di attacco includono OpenSSH, Desktop remoto, endpoint VPN. Gli sviluppatori sono generalmente consapevoli dell'importanza del loro software in quanto spesso forniscono un "limite di sicurezza", in particolare con attacchi pre-autenticazione, e in generale fanno meglio e hanno meno problemi di sicurezza.

Sfortunatamente, alcuni software chiave non sono così ben sviluppati. Un esempio notevole è OpenSSL che è molto usato, ma ha interni disordinati in cui è facile introdurre difetti di sicurezza come Heart Bleed. Sono stati presi provvedimenti per affrontare questo problema, ad es. LibreSSL.

Un effetto simile si verifica nel software CMS. Ad esempio, il core di Word Press è generalmente ben progettato e presenta pochi problemi. Ma i plug-in sono molto più variabili, e spesso plug-in obsoleti è il modo in cui tali siti vengono hackerati.

I browser Web sono in prima linea in questo. Miliardi di utenti desktop si affidano al proprio browser Web per essere sicuri, tenere lontano il malware dai loro sistemi. Ma devono anche essere veloci, supportare tutte le funzionalità più recenti e gestire ancora milioni di siti legacy. Quindi, sebbene tutti desideriamo davvero che i browser Web siano limiti di sicurezza affidabili, al momento non lo sono.

Quando si tratta di software su misura - che spesso sono applicazioni Web - gli sviluppatori che ci lavorano sono in genere meno esperti e attenti alla sicurezza rispetto agli sviluppatori di infrastrutture di base. E i tempi commerciali impediscono loro di adottare un approccio molto dettagliato e attento. Ma questo può essere aiutato con architetture che contengono codice critico per la sicurezza in una piccola area, che è accuratamente codificato e testato. Il codice non critico per la sicurezza può essere sviluppato più rapidamente.

Tutto lo sviluppo può essere aiutato con strumenti e test di sicurezza, inclusi analizzatori statici, fuzzer e test con penna. Alcuni possono essere integrati in una pipeline di elementi della configurazione automatizzati e già dipartimenti di sicurezza più esperti lo fanno.

Quindi abbiamo ancora molta strada da fare, in futuro c'è sicuramente speranza che ci saranno molti meno bug di sicurezza. E molte opportunità per la tecnologia innovativa che ci porta lì.

24
paj28

Sì...

Come altri hanno sottolineato, è possibile provare il codice e in tal modo dimostrare che il codice funzionerà esattamente come previsto. La difficoltà con i tempi di correzione e modelli non deterministici (come le interazioni di rete) è una difficoltà, non l'impossibilità. Le patch per Meltdown e Spectre mostrano che anche gli attacchi di temporizzazione del canale laterale possono essere contabilizzati e indirizzati.

L'approccio principale alla costruzione di codice come questo è quello di trattare il codice come matematica. Se non riesci a provare il tuo codice, non trattarlo come privo di bug. Se puoi, allora hai ... solo un colpo a bug-free.

... ma ...

Anche se puoi provare che il tuo codice è incontaminato, non puoi rilasciare dati se non come previsto, non può essere messo in uno stato errato o aberrante, ecc., Ricorda che il codice da solo non ha valore. Se uno sviluppatore scrive codice che ha una tale prova, ma esegue quel codice su hardware che a sua volta contiene vulnerabilità hardware, la sicurezza del software diventa discutibile.

Si consideri una semplice funzione per recuperare alcuni dati crittografati dalla memoria, archiviarli in un registro CPU, effettuare una trasformazione appropriata sul registro per decrittografare, elaborare e ricrittografare i dati. Si noti che ad un certo punto, i dati non crittografati si trovano in un registro. Se i codici operativi disponibili per quell'hardware della CPU offrono la possibilità di un programma che non ostruisce quel registro della CPU, eseguendo parallelamente al codice comprovato, allora c'è un attacco basato sull'hardware.

Ciò significa, in definitiva, che per avere un software così privo di exploit, dovresti prima provare che hai un hardware privo di exploit. Come hanno dimostrato Meltdown e Spectre (tra molti altri), l'hardware comunemente disponibile non supera questo marchio.

Anche l'hardware delle specifiche militari e delle specifiche spaziali non riesce in questa metrica. LEON line of processors , che vedono l'uso in schieramenti militari e spaziali, sono solo rinforzati contro Single Event Upset (SEUs) e Single Event Transients (SETs) . Questo è fantastico, ma significa che c'è sempre la possibilità che un utente malintenzionato collochi il sistema in un ambiente con radiazioni sufficienti a indurre abbastanza disturbi e transitori a porre l'hardware in uno stato aberrante.

... e altri ma ...

Quindi la correzione di software e hardware non è sufficiente. Dobbiamo considerare anche gli effetti ambientali nella prova del nostro hardware. Se esponiamo un LEON4 a una quantità di radiazione sufficiente a sopraffare l'involucro OR causa abbastanza radiazione indotta nell'involucro per sopraffare il processore, possiamo ancora causare aberrazione. A questo punto, il sistema totale somma ( software, hardware, ambiente) sarebbe follemente complicato da definire pienamente e correttamente per provare tale prova.

... quindi no, non proprio ...

Supponiamo di aver ideato un RDBMS di aver verificato il codice, di aver verificato l'hardware e di aver verificato l'ambiente. Ad un certo punto, abbiamo finalmente raggiunto il punto debole di qualsiasi catena di sicurezza:

Idio ... er, Utenti.

Il nostro glorioso database e il nostro illustre PFY creano un sistema insicuro. Il PFY - cerchiamo di essere più caritatevoli e conferiamo loro il titolo "JrOp" ... Il JrOp accede al database e riceve solo quei dati che JrOp deve conoscere e niente di più, niente di meno. In un momento di brillantezza solo JrOps può raccogliere, il nostro JrOp si sporge verso un collega e mormora: "Hai visto cosa User12358W ha appena caricato? Guarda questo!"

Tanto per la nostra sicurezza ...

... un'ultima speranza (e sconfiggendolo con assurdità) ...

Diciamo, tuttavia, immaginiamo il futuro ipotetico in cui abbiamo finalmente capito coscienza umana . L'umanità ha finalmente raggiunto una contabilità scientifica e tecnologica di tutto il funzionamento mentale umano. Supponiamo inoltre che ciò ci permetta di provare il nostro sistema anche contro i nostri utenti: i sistemi di feedback appropriati sono integrati nel sistema per garantire che il nostro JrOp non PENSI nemmeno di rivelare ciò che è stato rivelato al JrOp. Possiamo lasciare la questione della metaetica e della manipolazione ai filosofi - parlando di filosofi ...

Si noti che ad ogni singolo passaggio, abbiamo utilizzato prove.

"Ah-ah," esclama scettico pirronico con gioia. "Hai supposto che qualche sistema formale, come ZF/ZFC, Peano, teoria del Set non ingenuo, logica proposizionale classica, sia sano. Perché?"

Quale risposta può essere data? Tra Godel e Tarski, non possiamo nemmeno definire formalmente la verità (vedi Godel's Incompleteness Theorum e Tarski's Undefinability Theorum ), quindi anche l'asserzione ", beh, la prendiamo perché sembra è utile utilizzare un sistema in linea con la realtà ", in sostanza è solo un'ipotesi infondata - il che significa che qualsiasi prova che il nostro sistema sia privo di exploit è in definitiva stessa.

... quindi no, non lo è.

Mentre può essere possibile scrivere codice privo di bug, scrivendolo come prove matematiche e conseguendo tecnicamente l'obiettivo di "codice privo di exploit" di livello superiore, ciò richiede di esaminare il codice nel vuoto. C'è un certo valore in questo - è un obiettivo utile ("Ma questo presuppone wor--" "La maggior parte delle persone lo fa, affrontalo Pyrrho"). Tuttavia, non concederti mai la comodità di pensare di essere mai riuscito a raggiungere quell'obiettivo e, se lo fai, abbi l'umiltà di intitolare il tuo codice "HMS Titanic".

11
LRWerewolf

Voglio rispondere lateralmente alle domande precedenti. Non credo che il software privo di bug sia teoricamente impossibile o che il software sia troppo complesso. Abbiamo altri sistemi complessi con tassi di errore molto più bassi.

Ci sono due ragioni per cui il codice privo di exploit non accadrà in un futuro prevedibile:

Prestazioni e altre ottimizzazioni

Molti problemi, compresi quelli sfruttabili, non sono casi in cui non sappiamo come scrivere correttamente il codice, è solo che il codice corretto sarebbe più lento. O usa più memoria. O essere più costoso da scrivere. Nel software sono presenti molte scorciatoie per aumentare la velocità o ottenere altri guadagni. Alcune di queste scorciatoie sono la fonte di exploit

Problemi fondamentali

I sistemi che utilizziamo per creare software oggi presentano difetti fondamentali che portano a exploit, ma non sono in linea di principio inevitabili. I nostri compilatori non hanno dimostrato di essere al sicuro. Il sistema di libreria, in particolare l'ecosistema Node (ora copiato da compositore, cargo e altri) di integrazione dinamica di centinaia o migliaia di piccoli pacchetti attraverso dipendenze automatizzate è una sicurezza enorme incubo. Dovrei usare i caratteri a 72pt per mostrare quanto siano enormi. Quasi tutte le nostre lingue contengono costruzioni fondamentalmente insicure (il pensiero behing Rust ne illustra alcune). I nostri sistemi operativi sono costruiti su sistemi ancora più vecchi con ancora più difetti.

In breve: in questo momento, il meglio che possiamo fare è fondamentalmente "cercare di non sbagliare" e questo non è abbastanza per un sistema complesso.

Conclusione

Quindi, in sintesi, con il mondo del software come è oggi, no. Il codice senza exploit è impossibile con quegli strumenti, mentalità e ambienti di sviluppo a meno che non stiamo parlando di codice banale o estremamente autonomo (il kernel L4 che è già stato menzionato).

In teoria, tuttavia, nulla ci impedisce di creare software da piccoli moduli, ognuno dei quali può essere formalmente dimostrato di essere corretto. Niente ci impedisce di modellare le relazioni, le interazioni e le interfacce di tali modelli e di dimostrare formalmente la loro correttezza.

In effetti, oggi potremmo farlo, ma senza i fondamentali progressi nella progettazione del software, quel codice dovrebbe strisciare, non funzionare.

8
Tom

È possibile? Sì. Ma non per il software che stai cercando.

"Bug/Exploit Free" significa sostanzialmente che un programma avrà una risposta ragionevole e sicura a qualsiasi input. Questo può includere ignorare quell'input.

L'unico software in cui questo può essere ottenuto è programmi piccoli e banali appena oltre un mondo Hello. Non ci sono exploit in questo:

print("Hello World")

Perché questo codice ignora tutti gli input e restituisce solo una stringa codificata.

Tuttavia, questo codice esegue anche esattamente 0 lavori utili per te.

Non appena si desidera, ad esempio, connettersi a Internet e scaricare qualcosa, verranno scaricati dati sui quali non si ha alcun controllo e potrebbero essere dannosi. Naturalmente, ci sono molte restrizioni che il nostro software di download applica a quei dati per difenderti, ma è impossibile difenderti da un angolo di minaccia di cui non sei a conoscenza.

7
Gloweye

Sì, se la sicurezza del sistema è matematicamente provata. Non è una nuova idea, il Trusted Computer System Assessment Criteria , in breve "Orange Book" ha origine dal 1985.

enter image description here

In essi, il massimo livello di sicurezza, denominato A1, è quando abbiamo verificato il design . Significa che è matematicamente dimostrato che non c'è modo di rompere il sistema.

In pratica, dimostrare la correttezza matematica (compresa la sicurezza) di qualsiasi software è molto difficile e un lavoro davvero strabiliante. Per quanto ne so, nessun sistema informatico completo ha una tale prova, ma alcuni sistemi (almeno il kernel VM/ESA ) sono stati parzialmente provati.

Si noti inoltre che la sicurezza IT si occupa intrinsecamente di possibili attacchi da cui non sappiamo, da dove provengono. Ad esempio, un tale modello matematico andrebbe bene e funzionerebbe per un sistema che - direttamente o indirettamente - presume che non ci sia modo di intercettare le sue comunicazioni interne TCP. Pertanto, sarebbe idoneo a ottenere il certificato A1. In pratica, un tale sistema potrebbe essere facilmente fragile su un router compromesso.

In generale, test di correttezza automatizzati (o parzialmente automatizzati) dei programmi, incl. i loro test di sicurezza, è un campo informatico ben funzionante da alcuni decenni fa. Ne sono risultate molte pubblicazioni e titoli di dottorato di riferimento. Ma è ancora così lontano dall'ampio uso pratico, come lo era 25 anni fa.

Sono sorpreso che nessuno abbia menzionato verifica formale con il suo nome (sebbene la risposta di Cort menzioni il microkernel L4, che è stato formalmente verificato).

Personalmente non ho molta familiarità con la verifica formale, quindi indicherò alcune parti rilevanti della pagina di Wikipedia sull'argomento; si prega di fare riferimento ad esso per ulteriori informazioni.

Nel contesto dei sistemi hardware e software, la verifica formale è l'atto di provare o smentire la correttezza degli algoritmi previsti alla base di un sistema rispetto a una specifica specifica o proprietà formale, usando metodi formali di matematica. [1]

La verifica formale dei programmi software implica la prova che un programma soddisfa una specifica formale del suo comportamento. [...]

La crescita della complessità dei progetti aumenta l'importanza delle tecniche di verifica formale nel settore hardware. [6] [7] Allo stato attuale, la verifica formale è utilizzata dalla maggior parte o da tutte le principali società di hardware , [8] ma il suo utilizzo nel settore del software è ancora languente.[citazione necessaria] Ciò potrebbe essere attribuito alla maggiore necessità nel settore dell'hardware, in cui gli errori hanno un maggiore significato commerciale.[citazione necessaria] [...]

A partire dal 2011 , diversi sistemi operativi sono stati verificati formalmente: il microkernel Secure Embedded L4 di NICTA, venduto commercialmente come seL4 da OK Labs; [10] OSEK/VDX basato sul sistema operativo in tempo reale ORIENTAIS della East China Normal University;[citazione necessaria] Sistema operativo Integrity di Green Hills Software;[citazione necessaria] e PikeOS di SYSGO. [11] [12]

A partire dal 2016, i professori di Yale e Columbia Zhong Shao e Ronghui Gu hanno sviluppato un protocollo di verifica formale per la blockchain chiamato CertiKOS. [13] Il programma è il primo esempio di verifica formale nel mondo blockchain e un esempio di verifica formale utilizzato esplicitamente come programma di sicurezza. [14]

A partire dal 2017, la verifica formale è stata applicata alla progettazione di grandi reti informatiche [15] attraverso un modello matematico della rete [16] e come parte di una nuova categoria di tecnologia di rete, reti basate su intenti [17]. I fornitori di software di rete che offrono soluzioni di verifica formale includono Cisco [18], Forward Networks [19] [20] e Veriflow Systems. [21]

Il compilatore C CompCert è un compilatore C formalmente verificato che implementa la maggior parte di ISO C.

6
Dan Dascalescu

Nella sicurezza, ci piace credere che nulla possa essere protetto, solo indurito.

Questo perché non importa quanto si tenta di aggiornare il software e le applicazioni, Zero Day's esiste. Soprattutto se vale la pena hackerare il tuo software. Ciò significa che, sebbene il team di ingegneri della sicurezza sia in grado di correggere il problema, il software può essere sfruttato prima che la vulnerabilità diventi pubblica.

E più applicazioni crei nel tuo software, maggiore è la possibilità di zero giorni.

5
s h a a n

È possibile, ma non economico senza regolamenti che attualmente non esistono.

La risposta sul kernel dimostrato seL4 è corretta nel fornire un esempio di codice privo di bug, nel senso che funzionerà esattamente come descritto - e se la loro descrizione è sbagliata, beh, potrebbe essere chiamato un exploit. Ma i bug nella descrizione/specifica sono comparativamente estremamente rari ed è discutibile se in realtà sono anche bug.

I limiti citati anche nell'altra risposta si riducono tutti a "ci siamo limitati al kernel, perché avevamo risorse limitate". Tutti potrebbero essere risolti sviluppando l'hardware e il software circostante e il software client allo stesso modo del kernel seL4.

Se lo facessero tutti, quindi scrivere, per esempio, un sito Web dimostrabilmente corretto diventerebbe banale, perché tutti gli strumenti che useresti sarebbero dimostrati corretti e scriveresti solo un piccolo codice di colla. Quindi la quantità di codice che dovrebbe essere dimostrata corretta per un piccolo progetto sarebbe piccola. In questo momento, la quantità di codice che deve essere dimostrata corretta se si desidera scrivere un piccolo programma dimostrabilmente corretto è enorme perché sarebbe praticamente necessario ricominciare da zero senza avere a disposizione nessuno degli strumenti sviluppati dall'inizio dei computer .

Alcune persone oggi richiedono strumenti oppressivi come sorveglianza e censura e blocchi commerciali e contrattacchi in risposta alla digitalizzazione. Se invece passassero a incentivare il software sicuro, ad esempio richiedendo una certa quantità di responsabilità (chiamata anche responsabilità) dai produttori di software e hardware, presto avremmo solo un software sicuro. Ci vorrebbe molto meno tempo per ricostruire il nostro ecosistema software in modo totalmente sicuro di quanto non fosse necessario per crearlo in primo luogo.

5
Nobody

Attualmente è molto costoso scrivere codice privo di bug abbastanza complicato. È ancora più costoso verificare che sia effettivamente privo di bug o che il programma di verifica sia privo di bug, all'infinitum. Non credo che qualcuno avesse già una soluzione per le dimensioni della maggior parte dei software commerciali.

Ma direi che alcuni programmi, che potrebbero avere dei bug, sarebbero almeno privi di vulnerabilità. Ad esempio, un programma che dovrebbe essere eseguito in una sandbox perfetta come un browser e non tenta di interagire con nulla tranne l'utente, o almeno non ha alcuna promessa documentata che altri programmi dovrebbero fidarsi. Se c'è qualcosa che non va, è una vulnerabilità della sandbox e non del programma stesso.

Abbiamo modi per progettare sistemi che accettano un risultato solo se più versioni di un programma diversamente progettate concordano. E abbiamo modi per rendere apolidi le parti di un programma. Potremmo ricreare le promesse usando questi metodi. Dato che un programma sandboxing avrebbe una complessità limitata, direi che, in un futuro lontano, c'è qualche speranza di rendere finalmente possibile la scrittura di codice privo di exploit fintanto che tutti gli algoritmi utilizzati saranno provabili. Tuttavia, non so se diventerà mai economicamente sostenibile.

3
user23013

La maggior parte delle risposte si è concentrata su bug che consentono exploit. Questo è molto vero Tuttavia esiste una strada più fondamentale per gli exploit.

Se può essere programmato, può essere hackerato.

A qualsiasi sistema che può essere programmato può essere detto di fare cose stupide, anche cose maligne.
La programmabilità può assumere molte forme, alcune delle quali non sono molto ovvie. Ad esempio è un elaboratore di testi o un foglio di calcolo ha una funzione macro. Questa funzione fornisce sequenze all'utente. Se in aggiunta, ci sono funzionalità che forniscono selezione e reiterazione, improvvisamente è molto programmabile.

Se non può essere programmato, gli utenti richiederanno maggiore flessibilità.

Quasi ogni pacchetto applicativo complesso alla fine creerà un ambiente in cui gli utenti vogliono automatizzare il loro comportamento di routine. Questa automazione a volte assume la forma di script, come Powershell o Python, ma a volte si verifica attraverso qualcosa come una funzione macro con qualche campana e fischietti extra per l'automazione. Quando i costruttori accolgono gli utenti, improvvisamente è un sistema programmabile.

2
Walter Mitty

Basti pensare in termini di "sviluppo" di un edificio impenetrabile ... e pensare a pochi possibili scenari e ipotesi:

  • il budget è limitato? Lo è sempre! Un cattivo attore con un budget maggiore potrebbe acquistare i mezzi per entrare (come negli strumenti di acquisto, corrompendo i costruttori, ...)
  • c'è sempre una scala ambientale oltre la quale non hai alcun controllo: una regione in rotta, una meteora che colpisce un'infrastruttura di sicurezza cruciale, i progressi tecnologici più in basso lungo la linea che non avevi modo di pianificare, ...

Potresti scatenare la tua immaginazione con questo esempio.

E ora accetta il fatto che gli edifici sono spesso più semplici da difendere come oggetti fisici, molto probabilmente più semplici e raramente costruiti da componenti con catene di dipendenze così lunghe o difficili da stabilire come le librerie di software di terze parti.

2
diginoise

Teoricamente, sì.

Sebbene sia possibile un software privo di exploit, è estremamente difficile da ottenere, se si potesse programmare un software da programmare per te, tecnicamente, questo è possibile. Ho sentito parlare di persone che tentano di creare qualcosa del genere, anche se è più difficile di quanto sembri, creare un robot in grado di programmare per te, è più difficile di quanto sembri. Un altro modo in cui un programma può essere sfruttato gratuitamente è se il software è provato matematicamente. Sebbene, il codice creato dall'uomo non possa ottenere qualcosa del genere, altri tipi della programmazione può essere sfruttato gratuitamente se non ha richiesto input umani.

1
yosh

Scrivere un codice perfetto è come costruire un'auto perfetta. Potremmo essere in grado di costruire un'auto perfetta ma solo per l'età in cui viviamo. Man mano che la tecnologia cresce, le idee vengono condivise e più cervelli si riuniscono per risolvere i problemi, quindi potresti avere qualcosa di molto meglio.

Hai ragione nel dire che se un'azienda continua a lavorare su un software, a un certo momento saranno privi di bug. È vero, ma con il tempo si evolvono diverse tecnologie e fai la scelta di rimanere aggiornato con la tecnologia o semplicemente tenere il passo con la stessa vecchia base di codice perfetta.

Facciamo un esempio di Facebook perché sono un gruppo numeroso e sono focalizzati su un singolo prodotto. Facebook usava la libreria jquery per tutte le cose dinamiche qualche anno fa. Era una tecnologia all'avanguardia e tutto andava alla grande e non ho mai pensato di sostituirla. Ma per coinvolgere gli utenti dovevano diventare molto più dinamici. Quindi, man mano che Facebook cresceva e aveva bisogno di funzionalità sempre più dinamiche e si rendeva conto che jquery non soddisfaceva le loro esigenze.

Poiché nessun altro sito Web aveva così tanti utenti, nessun organismo ha effettivamente compreso la necessità di nuove librerie. Quindi hanno iniziato a lavorare sulla propria biblioteca chiamata React. Col passare del tempo sempre più persone hanno iniziato a utilizzare Internet a causa di Facebook e quindi ovviamente sono stati introdotti anche in altri siti. Ora anche altri siti web hanno iniziato ad avere i problemi che Facebook stava affrontando, ma fortunatamente ora avevano React Libreria per soddisfare le loro esigenze invece di costruirne uno nuovo.

Google stava riscontrando un problema simile e invece di utilizzare Facebook React hanno pensato di costruirne uno per soddisfare le loro esigenze specifiche. Ciò continuerà ad andare avanti e non ci sarà mai un unico codice base perfetto.

È la legge della natura ogni volta che arriva qualcosa di più grande che spinge più persone a pensare più in grande e fare meglio di così, Simile a come sempre più personaggi più potenti continuano ad arrivare in Avengers.

Perché il tempo è l'unica entità unica e non c'è mai un tempo illimitato. I proprietari di aziende e gli sviluppatori fanno triadi. Le triadi nel codice possono essere qualcosa del tipo:

  • Essere più ottimizzati/più veloci o più gestibili?
  • Concentrarsi maggiormente sulla sicurezza o avere un'esperienza utente migliore?
  • Le nuove funzionalità dovrebbero essere più testate o per spedire nuove funzionalità in tempo?

Rendiamo questa triade fuori tutti i giorni ...

1
omer Farooq

Per casi specifici (programmi), quasi . In generale, NO

  1. Per casi specifici:

È possibile affinare ripetutamente un determinato programma fino a quando la maggior parte o tutte le forme note di vulnerabilità (es. Buffer overflow) sono state eliminate, ma molte forme di vulnerabilità si verificano al di fuori del codice sorgente. Ad esempio, supponiamo di compilare in modo tale che il programma quasi o perfetto. Ciò produce un oggetto o un programma eseguibile distribuito. Nel computer di destinazione è esposto a malware che può modificare in modo tale che il codice binario, ovvero l'inserimento di salti nel codice dannoso che, naturalmente, non siano nel programma originale.

  1. In generale

È possibile avere un programma, ora o in futuro, essere in grado di convalidare il codice sorgente di any programma per le vulnerabilità?

Un po 'di teoria. Essere un programma privo di vulnerabilità è una proprietà semantica dei programmi, non sintattica. Una proprietà sintattica può essere formalizzata (e quindi può essere rilevata con metodi formali), ma una semantica non può:

Una proprietà semantica non è una proprietà semantica banale. una banale proprietà semantica è sempre presente o sempre assente in tutti i programmi. Una proprietà semantica ben nota dei programmi è " Questo programma funzionerà per sempre" (il famoso Turing's problema di arresto ) perché alcuni programmi funzioneranno per sempre, mentre altri vincono ' t. Torino provato che il problema dell'arresto è indecidibile , quindi non può esistere un metodo formale per testare la natura dell'arresto di alcun programma.

Il teorema di Rice afferma che anche tutte le proprietà semantiche non banali dei programmi sono indecidibili. In realtà, la dimostrazione si basa sul fatto che se una proprietà semantica non banale dei programmi fosse decidibile, potrebbe essere utilizzata per risolvere il programma di interruzione, il che è impossibile.

Come altro esempio di proprietà semantiche, considera la proprietà " Questo programma è dannoso". Naturalmente è una proprietà semantica e quindi, a causa del teorema di Rice, non è possibile creare un programma di rilevamento malware formale e deterministico; la maggior parte di essi utilizza l'euristica per le proprie procedure di rilevamento.

Naturalmente, poiché viene utilizzato nel rilevamento di malware, è possibile utilizzare l'euristica, l'intelligenza artificiale, l'apprendimento automatico, ecc. Per avvicinarsi a un metodo per la ricerca di vulnerabilità nel codice, ma non può esistere uno formale, perfetto e deterministico.

1

La prima regola del test del software (QA):

'Non è possibile confermare che l'ultimo bug è stato trovato'.

Ho codificato dal 1980 (anche un ingegnere elettronico) e nessuno del mio software è stato sfruttato, questo non significa che non potrebbe essere, solo che nessuno lo ha fatto. I sistemi bancari (e i sistemi simili a "Snowden") dispongono di avvisi/audit che attivano automaticamente la registrazione di accessi non autorizzati (ho lavorato su sistemi simili).

Quindi, sì, è possibile sfruttare il software libero, ma come lo quantificereste/verifichereste?

Infine, consulta le regole FCC (USA):

La parte 15 delle norme FCC, che disciplina i dispositivi senza licenza, incorpora un principio fondamentale della politica dello spettro degli Stati Uniti: un dispositivo senza licenza deve accettare interferenze da qualsiasi fonte e non può causare interferenze dannose a qualsiasi servizio concesso in licenza

Ciò significa che il segnale Wi-Fi è "sfruttabile", il che a sua volta significa che il software su di esso è "sfruttabile".

0
Mr. de Silva