Progetti e tesi

Sono possibili tesi e progetti inerenti i seguenti temi: Analisi di vulnerabilita', Analisi statica di linguaggi dinamici, Codice automodificante.
 Click here to return to: Isabella Mastroeni's Home Page; Mila Dalla Preda's Home Page.

 Analisi di vulnerabilita'

 Al giorno d'oggi la difesa dei sistemi informatici e' una grande sfida non solo dal punto di vista scientifico e tecnologico ma anche dal punto di vista sociale. La criminalita' informatica puo' essere vista come un sistema complesso vivace, dinamico e in continuo adattamento al fine di sfruttare nuove vulnerabilita' e nuovi strumenti. I criminali informatici sono sempre stati un passo avanti rispetto alla difesa. Per poter spezzare questo circolo vizioso dovuto alla natura asimmetrica della minaccia e' necessario non lavorare sugli attacchi del passato, ma prevedere le minaccie di domani. Nella pratica corrente della cyber security, la maggior parte delle difese sono reattive mentre gli attaccanti sono proattivi. Il solo modo per costruire difese effettive e' quello di cambiare le regole del gioco, anticipando le mosse degli attaccanti, identificando vulnerabilita' emergenti, e lavorando per rispondere a possibili attacchi prima che questi si verifichino.
Guardiamo al problema della difesa analizzando come il sistema interagisce con l'attacco. Questo concetto di interferenza viene modellato nel contesto dell'interpretazione astratta. Il framework della non interfernza astratta [GM04,M13] si basa sull'idea di modellare come diversi componenti di un sistema interferiscono tra loro in modo parametrico su cosa puo' variare e su cosa vogliamo osservare. Questa parametricita' e misurata e modellata mediante interpretazione astratta [CC77]. Con questi strumenti, vogliamo analizzare il problema a diversi livelli di astrazione e con tre obiettivi principali:

  Analisi di interferenza tra dati: A questo livello vogliamo capire le vulnerabilita' di flusso di informazione che compromettono la protezione dei dati sensibili o personali, ad esempio i meccanismi di sicurezza per Android si basano fortemente su meccanismi di controllo degli accessi, non offrendo controlli sui possibili flussi di informazione sensibile;

  Analisi di interferenza tra programmi: A questo livello vogliamo studiare come l'ambiente interagisce con l'ambiente in modo da capire cosa puo' attivare o inibire un attacco. Quindi vogliamo studiare le vulnerabilita' anche in funzione di come gli attacchi e l'ambiente interagiscono. Quindi vogliamo studiare le tecniche di anti-emulation ma anche le vulnerabilita' che possono essere non solo sfruttate ma anche attivate da agenti malevoli.

  Analisi di interferenza tra dati e programmi: A questo livello vogliamo capire come programmi di analisi possono interferire con i dati analizzati. Questo tipo di analisi potrebbe offrire basi tecnologiche per l'uso delle prove dgitali nel contesto legale. In particolare, un primo aspetto importante e' l'integrita' dei dati. L'integrita' riguarda la protezione dallla accidentale o intenzionale manipolazione dei dati. Questo garantirebbe la possibilita' di usare i dati come prove in ambito processuale. Quindi possiamo usare proprieta'di non interferenza astratta per assicurare affidabilita' ed accuratezza di processi automatici di estrazione di prove digitali.

[CC77] P. Cousot, R. Cousot. Abstract Interpretation: A unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL77, ACM Press 1977.

[GM04] R. Giacobazzi, I. Mastroeni: Abstract non-interference: parameterizing non-interference by abstract interpretation. POPL 2004. ACM Press, 2004.

[M13] I. Mastroeni: Abstract interpretation-based approaches to Security - A Survey on Abstract Non-Interference and its Challenging Applications. Festschrift for Dave Schmidt 2013: 41-65.

 Analisi statica di linguaggi dinamici

I linguaggi dinamici, come Ruby, Pyton, PHP e Javascript diventano sempre piu'popolari grazie alla rapidita' con cui si progettano producono prototipi dall'idea al prodotto finale. Questi linguaggi sono caratterizzati da una strutture altamente dinamica, che supera il varifica statica dei tipi. Questa caratteristica ha delle ragioni profonde nel modo e nell'area in cui questi linguaggi sono usati, che consiste principalmente nella progettazione di interfacce web e nella manipolazione di stringhe. Infatti, i linguaggi fortemente tipati non sono adeguati allo sviluppo di applicazioni orientate ai dati, come l'estrazione e il processo di big data. Inoltre, i linguaggi dinamici permettono la scrittura di codice automodificante, ovvero di programmi che possono cambiare la loro struttura interna a tempo di esecuzione. Questo e' possibile grazie alla presenza di primitive string-to-code come eval().
Tale natura fortemente dinamica dei linguaggi di scripting rompe l'assunzione standard che sta alla base dell'analisi di programmi, ovvero la staticita' della struttura del codice analizzato. Quindi per tali linguaggi emerge la necessita' non solo di predire l'evoluzione dei dati ma anche del codice.
La semantica di questi linguaggi e' stata recentemente studiata e formalizzata per Javascript in [GMS12,MMT08,BCF14]. Tutti questi linguaggi non considerano la possibilita' di Javascript di cambiare dinamicamente il proprio codice. Anche il problema dell'analisi statica di Javascript e' stato recentemente affrontato, ma anche in questo caso supponendo che il condice non utilizza la primitiva eval() [KDK14].Questo necessiterebbe di nuove metodologie per approssimare il comportamento del codice come una struttura dati mutevole. Inoltre PHP rappresenta ancora un problema aperto nel contesto della analisi statica di programmi, sia al livello semantico che di analisi.
Quindi le problematiche che si dovrebbero affrontare in questo contesto sono le seguenti:

  Studiare problematiche di sicurezza in termini di proprieta' analizzabili e vulnerabilita' comuni nel contesto di apllicazioni web scritte in JavaScript o PHP. In questo contesto e' importante sia capire che tipo di informazioni estraggono analisi esistenti (ad esempio analisi di flusso e di dipendenze), sia capire quali analisi nuove si possono progettare ed implementare per estrarre informazioni di flusso importanti per individuare vulnerabilita' specifiche dei contesti applicativi di questi linguaggi (come ad esempio code injection e XXS attacks). In particolare l'idea e' quella di studiare problemi di confinamento e flusso di informazione mediante taint analisi e noninterferenza mediante interpretazione astratta [GM04,M13];

  Studiare il funzionamento di eval(), capire come e' possibile estendere la semantica esistente di JavaScript per coprire anche primitive di automodifica come eval() e capire come adattare tale semantica al linguaggio PHP. In questo caso e' anche fondamentale capire come JavaScript, PHP e altri linguaggi interagiscono tra di loro nel contesto web.

[GMS12] P. Gardner, S. Maffeis, G. D. Smith: Towards a program logic for JavaScript . POPL 2012: 31-44 ACM Prss, 2012.

[MMT08] S. Maffeis, J. C. Mitchell, A. Taly: An Operational Semantics for JavaScript. APLAS 2008: 307-325.

[BCF14] M Bodin, A. Chargueraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith: A trusted mechanised JavaScript specification. POPL 2014: 87-100. ACM Press 2014.

[KDK14] V. Kashyap, K. Dewey, E. A. Kuefner, J. Wagner, K. Gibbons, J. Sarracino, B. Wiedermann, B. Harkdekopf: JSAI: Designing a Sound, Configurable, and Efficient Static Analyzer for JavaScript. CoRR 2014.

 Codice automodificante

Un problema centrale nell'ambito della sicurezza informatica e' quello dell'analisi di codice che si auto-modifica. Moderni linguaggi di programmazione come PHP e JavaScript sono dinamici, ovvero ammettono la possibilita' di generare a tempo di esecuzione il codice da eseguire. Inoltre gli hacker utilizzano ampiamente tecniche di metamorfismo per raggirare gli anti-virus, ovvero modificano il codice dei malware (programmi malevoli) in modo che questo non venga riconosciuto dagli anti-virus. In questi contesti diventa sempre piu' importante essere in grado di analizzare caratteristiche di programmi che si auto-modificano. Come primi passi in questa direzione sono stati sviluppati dei modelli comportamentali per programmi auto-modificanti che sono in grado di esprimere l'evoluzione del codice durante l'esecuzione. Questi modelli sono: - la semantica delle fasi [DGDCT10] che estrae staticamente il grafo di evoluzione del codice - waves [GMR09] che estrae dinamicamente il grafo di evoluzione del codice La semantica delle fasi sembra essere il corrispondente statico del modello estratto con le waves e viceversa le waves sembrano essere il corrispondente dinamico del modello estratto con la semantica delle fasi. Quindi i due modelli presentano vantaggi e limiti tipici delle analisi statiche e dinamiche. Ad esempio, la semantica delle fasi fornisce un modello preciso dell'evoluzione del codice ma porta ad un algoritmo di identificazione delle varianti metamorfe che e' indecidibile. Per guadagnare decidibilita' quindi necessario trovare opportune astrazioni del comportamento auto-modificante. Siamo interessati per esempio a capire come questi modelli possano essere approssimati rappresentando i programmi, e le rispettive varianti generate durante l'esecuzione, sul dominio dei Symbolic Finite Automata Astratti [DGLM15,DV14]. Piu' in generale siamo interessati allo sviluppo di domini astratti adatti all'analisi di codice che si auto-modifica.
Questi modelli di codice che si auto-modifica trovano una naturale applicazione nello sviluppo di nuovi algoritmi per l'identificazione automatica di codice malevolo che utilizza tecniche metamorfiche. Questi modelli possono essere utilizzati per

  Fare learning di signature astratte di malware a partire da alcuni campioni di varianti metamorfe di malware e quindi usare queste signature per l'identificazione automatica di nuove varianti metamorfe.

 Estrarre signature astratta dall'analisi di un campione di malware che si automodifica

 Fare learning del motore metamorfo che guida l'evoluzione di un malware metamorfo a partire da alcuni campioni di varianti del malware

I modelli sviluppati, i domini astratti proposti e gli algoritmi che ne derivano devono poi essere testati su malware esistenti per capirne potenzialita' e limiti. I dati sperimentali raccolti servono poi per migliorare il modello usato per l'identificazione automatica di malware al fine aumentare sempre piu' le prestazioni degli anti-virus.

[DGDCT10] M. Dalla Preda, R. Giacobazzi, S. K. Debray, K. Coogan, G. M. Townsend. Modelling Metamorphism by Abstract Interpretation. SAS 2010: 218-235

[GMR09] W. Guizani, J. Y. Marion, D. Reynaud-Plantey: Server-side dynamic code analysis. MALWARE 2009, pages 55-62

[DGLM15] M. Dalla Preda, R. Giacobazzi, A Lakhotia, I. Mastroeni. Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables. To appear in the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015). to appear

[DV14] Loris D'Antoni, Margus Veanes: Minimization of symbolic automata. POPL 2014, pages 541-554