Metodi Formali per la rilevazione di collusioni in ambiente Android
Introduzione
L’internet of things è ormai una realtà. Sul mercato si possono trovare centinaia di dispositivi intelligenti diversi, e le nostre case sono piene di elettrodomestici e sensori intelligenti.
Gli smartphone hanno fatto da apripista in questa rivoluzione delle connessioni, e tuttora mantengono la maggior parte di share del mercato per quanto riguarda i dispositivi elettronici. In questo contesto, da diversi anni, Android si è affermato come il sistema operativo più utilizzato al mondo con quasi il 39% del mercato [1], che supera addirittura il 70% se si considera solo l’ambiente mobile. Di conseguenza, Android risulta essere il sistema operativo più minacciato da malware.
I nostri smartphone sono assistenti di tantissime attività quotidiane, dal leggere le mail, navigare sul web e parlare con altre persone, fino al monitorare i nostri allenamenti, il traffico sulle strade che percorriamo e gli acquisti della spesa. La quantità di informazioni e dati che passano tramite i nostri smartphone è una risorsa di grande valore, ambita dalle grandi aziende informatiche, dai governi ma anche dai criminali.
La maggior parte di antimalware attuali fanno uso di tecniche ‘signature-based’ per il rilevamento di minacce, ossia comparano l’applicazione in analisi con un database di minacce conosciute. Chiaramente, questo tipo di approccio risulta inefficace nel rilevare nuove minacce non presenti nei database. Inoltre, gli sviluppatori di malware fanno largo uso di tecniche di offuscamento del codice per modificare parzialmente il malware mantenendo intatta la sua azione malevola ma rendendolo “nuovo” e quindi non rilevato dagli antimalware [2]. Per mantenere alto il livello di sicurezza dei dispositivi mobili c’è un continuo bisogno di sviluppo di tecniche di rilevamento di applicazioni malevole sempre più’ efficaci ed efficienti.
In questo contesto, gli scrittori di malware stanno sviluppando attacchi sempre più complessi per evadere i sistemi di rilevamento del malware, uno di questi recentemente apparso è il cosiddetto colluding attack (attacco tramite collusione): l’azione dannosa è suddivisa in più applicazioni che comunicano tra loro quando l’utente esegue una determinata azione o al verificarsi di uno specifico evento all’interno del sistema. In questo modo gli attuali antimalware, che analizzano un’applicazione alla volta, non sono in grado di identificare il payload dannoso in quanto suddiviso tra diverse applicazioni. Pertanto, negli attacchi tramite collusione, un payload dannoso viene suddiviso in parti più piccole e distribuito in più applicazioni. In questo tipo di attacco le applicazioni non destano sospetti per gli antimalware, perché richiedono i permessi minimi necessari per eseguire l’azione dannosa. Ad esempio, quando due applicazioni implementano questo tipo di attacco, la prima applicazione potrebbe avere il permesso di leggere dati sensibili e trasmetterli alla seconda applicazione, che col permesso di connessione ad una rete li trasmette al mondo esterno. In questo modo la prima non richiede il permesso per utilizzare la connessione Internet, ma solo il permesso per leggere i dati, eludendo così i controlli, poiché reputata innocua; dall’altra parte la seconda applicazione richiedendo solo il permesso di connessione ad Internet, non risulta essere sospetta se non può accedere direttamente a informazioni di tipo sensibile. A tal proposito si può affermare che se analizzate singolarmente, le applicazioni sono considerate benigne poiché non esiste un percorso diretto dai dati sensibili alla loro trasmissione.
Metodologia
Partendo dalla problematica dell’attacco tramite collusione in ambiente mobile, abbiamo sviluppato una metodologia basata sull’utilizzo di tecniche di model checking e su una nuova funzione euristica, il cui scopo è quello di ridurre il numero di applicazioni analizzate. La funzione è stata definita sulla base della Logica Temporale Mu-Calculus e del model checking [3].
La metodologia lavora sulle risorse condivise di tipo stringa, andando a sfruttare le SharedPreferences di Android, usate per salvare i settaggi delle impostazioni nelle applicazioni. Il nostro metodo, mostrato in Figura 1, prevede in input un insieme di applicazioni, che viene ridotto grazie ad una prima euristica, ottenendo così un sottoinsieme di candidati all’analisi. La prima euristica inoltre divide le applicazioni in base al diverso utilizzo delle shared resource, infatti in figura possiamo notare uno split tra le applicazioni che verificano la proprietà di GET (se leggono i dati) e quelle che verificano le proprietà di PUT (se scrivono dati). La seconda euristica entra in azione dopo la verifica della proprietà di PUT, visto che le applicazioni di questo tipo sono quelle che permettono una modifica attiva; e serve a ridurre ulteriormente lo spazio di ricerca tra le applicazioni colludenti andando ad analizzare l’esecuzione del flusso e quindi il tipo di informazione che viene inviata, per fare ciò si utilizza FlowDroid. Dopo ciò, con il model checker CWB-NC si verifica se tra le applicazioni è presente una proprietà di collusione che soddisfa la formula in mu-calculus [4].
Conclusioni
In conclusione, possiamo dire che l’attacco tramite collusione è una minaccia emergente in ambiente mobile che si basa sulla comunicazione tra due o più applicazioni. Per mitigare gli effetti dannosi di questa nuova minaccia in ambiente Android, proponiamo l’utilizzo di un metodo basato sul model checking. Il metodo proposto ottiene una accuracy pari a 0.99 nella valutazione di applicazioni che effettuano diversi tipi di attacchi tramite collusione, applicazioni malevole che non effettuano collusione ed applicazioni considerate legittime.
Referenze
[1] Statcounter Global Stats website. “Operating System Market Share Worldwide.” URL: https://gs.statcounter.com/os-market-share ACCESSED: 02/12/20
[2] Canfora, Gerardo, et al. “Obfuscation techniques against signature-based detection: a case study.” 2015 Mobile Systems Technologies Workshop (MST). IEEE, 2015.
[3] Iadarola, Giacomo, et al. “Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection.” Applied Sciences 10.22 (2020): 7975
[4] Casolare, Rosangela, et al. “Malicious Collusion Detection in Mobile Environment by means of Model Checking.” 2020 International Joint Conference on Neural Networks (IJCNN). IEEE, 2020
Articolo a cura di Giacomo Iadarola, Rosangela Casolare, Fabio Martinelli, Francesco Mercaldo, Antonella Santone
Giacomo Iadarola è assegnista di ricerca all’Istituto di Informatica e Telematica (IIT) del CNR di Pisa e dottorando al dipartimento di Informatica dell’Università di Pisa. Ha conseguito la laurea Magistrale in “Security & Privacy” studiando all’Università di Twente (Olanda) e alla Technische Universität Darmstadt (Germania).
Da sempre appassionato di cybersecurity, i suoi interessi nella ricerca riguardano la Software e Malware Analysis, specialmente in ambiente Mobile, i Metodi Formali ed il Machine Learning per risolvere problemi di Sicurezza Informatica, e l’Explainable AI.
Rosangela Casolare è una dottoranda presso l’Università degli Studi del Molise. È risultata vincitrice di una borsa di dottorato cofinanziata dall’Istituto di Informatica e Telematica del Consiglio Nazionale delle Ricerche (CNR) di Pisa.
Il 21 Febbraio 2019 ha conseguito la Laurea Magistrale in Sicurezza dei Sistemi Software presso la stessa università.
Le sue attività di ricerca rientrano nell’ambito della sicurezza dei sistemi mobili, con particolare enfasi sullo sviluppo di metodologie per la rilevazione di applicazioni colludenti attraverso tecniche di verifica formale in ambiente Android.
Fabio Martinelli è Dirigente di Ricerca presso l’Istituto di Informatica e Telematica (IIT) del Consiglio Nazionale delle Ricerche (CNR) ed il è referente per le attività di cyber security del CNR. I suoi interessi di ricerca riguardano la sicurezza dei sistemi distribuiti e pervasivi e gli aspetti di privacy e trust in sistemi dinamici e complessi. Fabio Martinelli e’ Direttore Scientifico della Scuola Internazionale in Foundations of Security Analysis and Design (FOSAD). Fabio Martinelli serve come co-chair della piattaforma tecnologica Italiana sulla ricerca in Sicurezza (SERIT) e del WG3 su Ricerca ed Innovazione della piattaforma tecnologica su “Network and Information Security (NIS)” promossa dalla Comunità Europea a supporto della direttiva NIS. Inoltre Fabio Martinelli è stato recentemente nominato First Director della European Cyber Security Organization (ECSO), la principale organizzazione in Europa per la ricerca ed innovazione del settore della cyber security.
Francesco Mercaldo ha conseguito presso l 'Università degli Studi del Sannio di Benevento la Laurea Specialistica in Ingegneria Informatica, con una tesi in software testing, ed il Dottorato in Ingegneria dell'Informazione nel 2015, con una tesi sull'analisi di malware mediante tecniche di machine learning. Successivamente è stato assegnista di ricerca post dottorale presso l'Istituto di Informatica e Telematica (IIT) del Consiglio Nazionale delle Ricerche (CNR) di Pisa ed attualmente è ricercatore presso l'Università degli Studi del Molise di Campobasso. Le aree di ricerca di Francesco sono nel campo della cyber security, in particolare sulla malware analysis, la verifica e la validazione del software, con l'enfasi sull'applicazione di metodi empirici. E' autore di diverse pubblicazioni su conferenze e riviste internazionali e fa parte di diversi comitati scientifici internazionali.
Antonella Santone è professore associato presso l ' Università degli Studi del Molise dal primo Settembre 2017. Il 23 Aprile 1993 ha conseguito la Laurea in Scienze dell’Informazione, presso l’Università degli Studi di Pisa. Il 16 Settembre 1997 ha conseguito il titolo di Dottore di Ricerca in Ingegneria Elettronica, Informatica e delle Telecomunicazioni presso il Dipartimento di Ingegneria dell’Informazione dell’Università di Pisa. Dal 27 Novembre 1998 al 31 Ottobre 2001 è stata in servizio, come ricercatore non confermato, presso il Dipartimento di Ingegneria dell’Informazione dell’Università di Pisa. Dal primo Novembre 2001 al 31 Agosto 2017 è stata in servizio in qualità di professore associato presso la Facoltà di Ingegneria dell’Università del Sannio. L’attività di ricerca di Antonella Santone si svolge principalmente nell'ambito dei metodi formali per l’analisi e la verifica di sistemi software, con particolare attenzione alle tecniche di model checking.
