Informatica: algoritmi, linguaggi, metodi formali e sicurezza
Strumenti formali per l'analisi dei linguaggi di programmazione. Linguaggi per coordinare le interazioni dinamiche fra componenti distribuite. Metodologie per l'analisi di algoritmi e l'esplorazione di basi di dati. Metodi formali per la specifica e la verifica di sistemi concorrenti, distribuiti e mobili. Linguaggi per la definizione e l'enforcement di politiche di controllo degli accessi alle risorse. Modelli e metodi per l'analisi di protocolli di sicurezza. Educational mining.
In particolare, tra i temi specifici, ci stiamo occupando di:
- Algoritmi per l'analisi di grafi del mondo reale
In una società in cui siamo quasi sempre "connessi", la capacità di acquisire facilmente diverse informazioni è diventata una fonte di enormi quantità di dati da elaborare e analizzare. I grafi sono una struttura dati che permette di modellare molte delle relazioni presenti in questi dati astraendo da aspetti specifici particolari e rappresentando in modo efficace milioni o miliardi di connessioni: la complessità delle entità coinvolte è racchiusa in un vertice del grafo e i complessi meccanismi di interazione tra di esse sono semplicemente descritti da un arco. Per esempio, un social network può essere visto come un grafo i cui nodi sono gli utenti e gli archi corrispondono alle loro relazioni di amicizia. Analogamente, l'economia di Bitcoin (o di qualsiasi altro sistema economico) corrisponde a un grafo i cui nodi sono gli utenti e i cui archi rappresentano i pagamenti tra di essi. In questo contesto, scoprire gli utenti più importanti e influenti, quali saranno le loro amicizie future, a quali comunità appartengono e la struttura della società in cui vivono possono essere tradotti in problemi su grafi. La ricerca in questo ambito si concentra sullo sviluppo di modelli e algoritmi per risolvere questo tipo di problemi in modo efficiente su grafi del mondo reale di grandi dimensioni. In particolare, il lavoro di ricerca si sviluppa in linea con due aspetti ortogonali: il primo è la traduzione di un problema reale in termini di un problema su grafi, il secondo è volto allo sviluppo di algoritmi efficienti, auspicabilmente con complessità temporale (quasi-) lineare, per risolverlo. In questo senso, teoria e pratica procedono insieme, in quanto problemi pratici motivano contributi teorici che a loro volta permettono di ottenere soluzioni pratiche e efficienti dei problemi originali.
Persone: Ferreira Da Silva, A. Marino - Analisi degli Algoritmi
Le tecnologie dell'informazione e delle telecomunicazioni richiedono una serie di algoritmi per trasformare, archiviare e trasmettere grandi quantità di dati. L'efficienza di questi algoritmi dipende sia dagli aspetti tecnologici sia dalla complessità spazio-temporale degli algoritmi. L'analisi degli algoritmi è una branca dell'informatica che studia l'efficienza degli algoritmi secondo alcuni parametri caratteristici. Lo scopo è fornire informazioni precise sull'efficienza di qualsiasi tipo di algoritmo studiando il suo comportamento nel caso peggiore, migliore e medio. Utilizzando i risultati così ottenuti, è quindi possibile scegliere il migliore tra diversi algoritmi che svolgono lo stesso compito.
Lo sforzo generale per prevedere con precisione le prestazioni degli algoritmi è arrivato a coinvolgere la ricerca nella combinatoria analitica, l'analisi di strutture discrete casuali, l'analisi asintotica, le distribuzioni esatte e al limite e altri campi di indagine in informatica, teoria della probabilità e combinatoria enumerativa, usando un approccio basato sulle funzioni generatrici e sul metodo dei coefficienti, sul metodo simbolico e sulle somme combinatorie. Le funzioni generatrici sono utilizzate nella combinatoria da 300 anni e negli ultimi decenni sono state uno degli strumenti maggiormente utilizzati nell'analisi degli algoritmi. In realtà, servono sia come strumento combinatorio per facilitare il conteggio sia come strumento analitico per sviluppare stime precise per quantità di interesse. Il metodo dei coefficienti rappresenta un completamento del concetto precedente mentre il metodo simbolico consente di sviluppare relazioni tra le strutture combinatorie e le funzioni generatrici associate. Le identità combinatorie hanno ricevuto attenzione da tempi molto antichi e parte di questa letteratura ha una forte connessione con l'analisi degli algoritmi.
Persone: Merlini, Verri - Design, formalizzazione e implementazione di linguaggi di programmazione
La ricerca in questo settore si focalizza sul design di nuovi linguaggi di programmazione o di estensione di linguaggi esistenti. I linguaggi in questione possono essere sia General Purpose Language (GPL) che Domain Specific Language (DSL). In particolare ci concentriamo su linguaggi staticamente tipati Java-like, quindi, principalmente, Object-Oriented. Si mira a dare la formalizzazione di tali linguaggi, provandone varie proprietà di correttezza. Inoltre, ci occuperemo anche di darne un’implementazione con integrazione in un IDE. Nel caso di estensione di linguaggi, ci concentriamo su estensione di linguaggi mainstream come Java, mirando a migliorarne le funzionalità dal punto di vista dello sviluppatore, così da ottenere maggior riuso di codice e maggiore flessibilità nella scrittura di programmi, sempre mantenendo le proprietà di correttezza.
Persone: Bettini - L'insegnamento dell'informatica nella scuola
C'è una missione culturale qui da intraprendere. Il problema non è quello dei contenuti specifici da somministrare in un certo tipo di scuola piuttosto che in un'altra. La questione è di portata ben più generale perché attiene alla rivalutazione dell'informatica quale branca della scienza, autonoma e fondativa quanto, ad esempio, la fisica e la chimica. La missione va tuttavia ben oltre anche all'eventuale "rivendicazione" di un adeguato numero di ore per la "materia dell'informatica" nel maggior numero possibile di scuole, perché concerne una revisione profonda del modo di insegnare le materie scientifiche in generale; per questo essa va considerata una missione culturale. In breve, si tratta di mettere in atto una transizione dell'attuale insegnamento, sostanzialmente didascalico, di alcune discipline scientifiche, quasi sempre come fossero indipendenti fra loro, in una vera educazione al pensiero scientifico, ancora di fatto largamente assente, persino nelle scuole più scientificamente orientate. Fra le conseguenze della distorsione prodotta da questo sistema si trova, caso esemplare, la disciplina fantasma, l'informatica, la quale, nel discorso generale, pare esaurire la propria ragione di esistenza nel trovarsi spennellata su tutto ciò che è tecnologico. Cosicché chiunque si occupi di "media", di costruzione di siti, di manipolazioni tecnologiche varie, chiunque sappia usare minimamente due o tre programmi di "produttività personale", diviene, in qualche modo, un informatico. Se l'informatica è presente nelle scuole, a parte alcuni casi particolari, lo è per imparare qualche applicazione di produttività personale o al più per qualche lavoro di "coding", frequentemente sterile, in quanto culturalmente scollegato dal resto. Occorre quindi intraprendere un'azione di ricerca sulla didattica dell'informatica, che deve tuttavia essere pensata all'interno di una più ampia azione di ripensamento della didattica del pensiero scientifico. L'abbiamo chiamata missione culturale perché le conseguenze dell'assenza di pensiero scientifico sono ubiquitarie, vaste e devastanti. Che non significa contrapporre le scienze alle humanities, anzi, quella della rivalutazione corretta del pensiero scientifico e del suo ruolo nella società è una missione umanistica.
Persone: Verri - Educational data mining
Numerosi settori, dalle attività economiche e commerciali alla pubblica amministrazione, sono coinvolti nella crescita dei dati nei sistemi informatici. Per questo motivo è importante sviluppare nuove metodologie e tecnologie per gestire e analizzare tutte le informazioni che possono essere derivate da tali grandi fonti di dati. Per quanto riguarda il campo dell'educazione, Educational data mining (EDM) è un'area di ricerca recente che esplora e analizza, utilizzando algoritmi di machine learning e data mining, sia i grandi archivi di dati normalmente presenti nelle banche dati delle scuole e delle università a fini amministrativi sia le grandi quantità di informazioni sull'interazione insegnamento-apprendimento generate in e-learning o in contesti educativi basati sul web. EDM cerca di utilizzare tutte queste informazioni per comprendere meglio le prestazioni del processo di apprendimento degli studenti e può essere utilizzato dall'università o dalla direzione della scuola per migliorare l'intero processo educativo. In particolare, la letteratura esistente sull'uso del data mining nei sistemi educativi si occupa principalmente di tecniche come il clustering, la classificazione, il la ricerca di regole associative e l'analisi di pattern sequenziali. I nostri studi riguardano tali tecniche e la loro applicazione a dati riguardanti varie coorti di studenti del corso di laurea in Informatica e dei corsi di laurea di ambito scientifico che condividono lo stesso test di autovalutazione richiesto agli studenti prima di iscriversi all'Università di Firenze.
Persone: Bertaccini, Merlini, Verri - Machine Learning per dati strutturati
In molti domini applicativi, le informazioni sono naturalmente rappresentate come dati strutturati. Un dato strutturato si contraddistingue da quello tabellare (o "flat") per la presenza di una struttura che indica come le varie componenti dell'informazione sono in relazione tra di loro. Ad esempio, in chimica una molecola è naturalmente rappresentata da un grafo la cui struttura ci indica come gli atomi interagiscono tra di loro. Allo stesso modo, una frase in linguaggio naturale o il codice di una programma sono intrinsicamente composizionali e possono essere rappresentate come un albero. La ricerca in questo ambito si concentra sullo sviluppo di nuove tecniche di Machine Learning (sia neurali che probabilistici) e sull'applicazione di queste in domini speicifici.
Persone: Bertaccini, Castellana - Metodi formali per la specifica e la verifica di sistemi concorrenti, distribuiti e mobili
La ricerca in questo ambito si concentra sulla comprensione dei problemi fondazionali ed applicativi sollevati dai moderni sistemi concorrenti, distribuiti e con mobilità, quali ad esempio le architetture orientate ai servizi, i sistemi di calcolo autonomici e i sistemi cyber-fisici, operanti in ambienti non completamente determinati e mutevoli. Lo scopo è individuare modelli, linguaggi e strumenti formali capaci di catturare aspetti differenti e specifici di tali sistemi complessi, permettendo così lo studio di problemi riguardanti, per esempio, interazione, connettività, adattività e sicurezza. Calcoli di processo, semantiche operazionali, denotazionali e osservazionali, sistemi di tipo, logiche modali e temporali sono alcuni dei metodi formali e delle tecniche di analisi utilizzati in tali studi.
Persone: Pugliese, Tiezzi
In particolare sono attive le seguenti linee di ricerca:- Politiche di controllo degli accessi alle risorse: Sviluppo di una metodologia incentrata sul linguaggio FACPL (Formal Access Control Policy Language), fondata su solide basi formali e supportata da strumenti software di facile utilizzo, per la specifica, l’analisi e l’enforcement di politiche di controllo degli accessi basate su attributi.
- Linguaggi domain specific: Progetto di linguaggi appositamente sviluppati per esprimere caratteristiche distintive di alcuni domini di sistemi distribuiti, quali network-aware programming, service-oriented computing (SOC), autonomic computing e collective adaptive systems programming.
- Contratti di servizi: Estensioni di contract automata, formalismi basati su automi sviluppati per formalizzare contratti per applicazioni orientate ai servizi, con meccanismi effettivamente utilizzati dalle tecnologie SOC del mondo reale, e sviluppo di algoritmi per sintetizzare orchestrazioni e coreografie di contratti di servizi formalizzati tramite contract automata.
- Modelli e metodi formali per Security e Safety
L'obiettivo generale è sviluppare metodologie, basate su un rigoroso quadro matematico, per analizzare i sistemi computazionali dal punto di vista della Sicurezza e della Safety.
Per quanto riguarda la Sicurezza, vengono sviluppati modelli e metodi che forniscono garanzie formali su:- Quantitative Information Flow (QIF), dove l'obiettivo è provare che un dato sistema, in media, non rilasci più di una quantità predefinita di informazione su un certo dato segreto (per esempio, una password, o l'identità di un utente in un sistema di anonimizzazione come Tor). Tecniche di Teoria dell'Informazione vengono ampiamente utilizzate per analizzare questo tipo di problemi.
- Privacy nel contesto della anonimizzazione e pubblicazione di dataset. Qui l'obiettivo generale è garantire che un utente malintenzionato non possa utilizzare dati (anonimizzati) resi pubblici per apprendere informazioni sensibili su specifici individui. Ciò implica in generale la possibilità di stabilire un compromesso adeguato tra utilità dei dati e privacy. In questo campo, uno strumento importante è costituito dai metodi di inferenza Bayesiana.
I modelli e i metodi risultanti vengono testati anche su sistemi e dataset del mondo reale. Per quanto riguarda la Safety, vengono presi in esame soprattutto sistemi continui, e più in generale ibridi. La dinamica di tali sistemi è descritta, per la parte continua, da sistemi di equazioni differenziali nonlineari, che raramente ammettono una soluzione in forma chiusa. Un ruolo centrale in questo campo è pertanto svolto dalla ricerca di "invarianti", che garantiscano che le traiettorie del sistema nello spazio degli stati non sfuggano mai da una "zona di sicurezza" specificata dall'utente (per esempio, nel caso di un aereo, che velocità e inclinazione mettano sempre al riparo dallo stallo). Strumenti teorici coalgebrici (teoria degli automi, bisimulazione) e algebrici (polinomi, ideali) vengono impiegati per definire algoritmi di generazione automatica di tali invarianti. Tali algoritmi vengono testati anche su specifiche di sistemi realistici.
Persone: Boreale
Persone: Bertaccini, Bettini, Boreale, Castellana, Ferreira Da Silva, A. Marino, Merlini, Pugliese, Tiezzi, Verri
Progetti di ricerca finanziati nell'area tematica "Informatica: algoritmi, linguaggi, metodi formali e sicurezza", con PI afferenti al Dipartimento:
- Assessment cybersecurity readiness, Programma POR FESR 2014-2020, Regione Toscana, (2019-2021, PI: R. Pugliese): L'obiettivo del progetto è valutare, empiricamente, il livello di maturità delle PMI nel contesto della cyber security e individuare misure concrete che possano consentire loro di migliorare la propria consapevolezza rispetto ai rischi e alle minacce cyber e di cogliere le opportunità di innalzare le proprie capacità di cyber security.
Ultimo aggiornamento
16.04.2024