Che ne direste se fosse possibile ingannare i compilatori affinché producano dei file binari differenti dalla logica visibile agli occhi umani nel codice sorgente? Vi dimostriamo che fare ciò non solo è possibile, ma facilmente sfruttabile...
Questo si legge nell'introduzione del paper "Trojan source: Invisible Vulnerabilities", recentemente pubblicato dal Prof. Ross Anderson della Cambridge University, autore del testo “Security Engineering”, e da Nicholas Boucher, suo studente di dottorato.
Incuriositi, come spesso capita nel mondo cyber, abbiamo deciso di approfondire.
Per iniziare, ricordiamo che i programmi scritti con i moderni linguaggi di programmazione hanno necessità di un compilatore, cioè di un altro programma che analizza il testo del nostro programma, ne verifica la correttezza sintattica, e lo traduce in un programma ottimizzato nel linguaggio eseguibile dal calcolatore. Già da questo si comprende la criticità nello sviluppo di un compilatore che potrebbe inserire involontariamente delle vulnerabilità nel programma. Negli anni ’80 già Ken Thomson, uno dei padri di Unix, metteva in guarda da questi rischi nella sua famosa lezione tenuta in occasione del conferimento del “Turing award” (l’equivalente del Premio Nobel per l’informatica) dal titolo evocativo “Reflections on trusting trust”. Il compilatore del linguaggio C è a sua volta un programma scritto in linguaggio C, per cui per potersi fidare del programma eseguibile prodotto dal compilatore occorre non solo fidarsi di chi ha scritto il programma, ma anche fidarsi del compilatore.
Ora, tornando all’articolo di Boucher e Anderson, ripartiamo dal considerare un compilatore come un analizzatore di testo che conosce i termini e la sintassi del linguaggio di programmazione. I caratteri utilizzati per formare il testo hanno necessità di essere codificati in un computer.
Per capire in cosa consiste questo nuovo genere di attacco presentato da Boucher e Anderson, in primo luogo occorre parlare di codifica e degli standard utilizzati per la codifica.
Con lo sviluppo dei sistemi informatici cambiarono le esigenze e fu necessario estendere lo standard ASCII per consentire la codifica di caratteri provenienti da lingue diverse o necessari per specifici ambienti.
Si passò così, gradatamente, allo standard conosciuto come UNICODE. Questo standard consente di codificare 144.697 tra caratteri e simboli vari. Tra questi vi sono alfabeti cosiddetti Left-to-Right (da sinistra a destra, come Italiano, Russo, Inglese...) e Right-to-Left (da destra a sinistra, come Arabo, Ebraico...). Nel caso di Unicode, che è uno degli standard di codifica oggi più largamente utilizzato, per stabilire l’ordine secondo il quale un testo debba essere visualizzato, viene utilizzato un algoritmo chiamato Bidirectional Algorithm (BiDi).
L'algoritmo BiDi è pensato per gestire automaticamente la visualizzazione del testo attraverso dei caratteri cosiddetti di controllo (override characters) che consentono di specificare esplicitamente come debba essere trattata una specifica porzione di testo (ad esempio Right To Left Override, RLO, specifica di trattare il testo a cui si applica come right-to-left). I caratteri di controllo sono dei caratteri invisibili a schermo che permettono di controllare la visualizzazione di porzioni di testo. Eccone alcuni tra i più usati.
Inoltre i caratteri di controllo possono essere "nidificati", consentendo in questo modo di riordinare la visualizzazione di un testo in modo anche molto complesso.
Ora, se il testo che viene visualizzato a schermo è un codice di un programma, occorre tener presente che in linea di massima la sintassi della maggior parte dei linguaggi di programmazione non consente tipicamente di inserire questi caratteri controllo direttamente all’interno del codice sorgente in quanto altererebbero evidentemente la logica di controllo del programma. Tuttavia, dato che molti linguaggi consentono l’utilizzo di commenti e stringhe, è possibile inserire i caratteri di controllo all’interno dei commenti o delle stringhe e fare si che abbiano un impatto sul codice sorgente in quanto i BiDi ovverrides non rispettano i delimitatori delle stringhe e dei commenti.
Proprio su questa caratteristica tipica delle codifiche odierne si basa il tipo di attacco descritto da Boucher e Anderson. In effetti grazie ai caratteri di controllo è possibile sfruttare la differenza tra quanto visualizzato e quanto realmente codificato e passato a compiler e interpreter per condurre il tipo di attacco "Trojan Source Attack" descritto da Boucher e Anderson.
Boucher e Anderson hanno inoltre dimostrato che tale tipo di attacco è possibile con i più usati linguaggi di programmazione tra cui C, C++, C#, JavaScript, Java, Rust, Go, and Python.
L’esempio di seguito, in codice Python, mostra che il codice codificato (e dunque eseguito sulla macchina) a sinistra è differente dal codice sorgente (a destra) visualizzato.
In base a quest’ultimo ci si aspetterebbe di trovare un valore pari a 50 in bank [‘alice’] al termine dell’esecuzione, mentre nella pratica il valore presente sarà ancora pari a 100.
Il fatto che fino ad ora non si abbiano evidenze di questo genere di attacco non ci tranquillizza per il futuro dato che, come noi, anche altri possono aver letto il paper e, magari, preso la decisione di testarne i concetti.
Davide Ariu, Giorgio Giacinto e Alessandro Rugolo,
Per approfondire:
- Trojan Source: Invisible Vulnerabilities;
- 'Trojan Source' bug a novel way to attack program encodings (techxplore.com);
- Trojan Source attack is dangerous for compilers of program languages (gridinsoft.com);
- GitHub - nickboucher/trojan-source: Trojan Source: Invisible Vulnerabilities;
- The Unicode Bidirectional Text Algorithm - Developer guides | MDN (mozilla.org);
Nessun commento:
Posta un commento