UNIVERSITA’ DEGLI STUDI DI CAGLIARI
CONSIGLIO DELLA FACOLTA’ DI SCIENZE MATEMATICHE FISICHE E NATURALI
SEDUTA STRAORDINARIA DEL 16 DICEMBRE 2011
Il Consiglio della Facoltà di Scienze Matematiche Fisiche e Naturali si svolgerà in
forma telematica sino alle ore 11,00 del 16 dicembre 2011 nella per deliberare sul
seguente:
ORDINE DEL GIORNO
1.
2.
3.
4.
Approvazione verbali sedute precedenti
Conferma in ruolo ricercatori
Chiamata ricercatore
Provvedimenti insegnamenti vacanti
Sono presenti:
Professori ordinari e straordinari: G. Biggio, M. Gaviano, G. Verani, R. Caddeo, F. Meloni,
A. Anedda, A. M. Deiana, M. Franceschelli, A. Concas, G. Floris, M. A. Dessì, B. Saitta,
T. Gramtchev, M. Serra, C. Marini.
Professori associati: G. Alberti, S. Banni, G. Barbieri, L. Burderi, R. Cioni, A. Cogoni, S.
Cosentino, L. Dazzi, N. Dessì, F. Di Gregorio, C. Di Ruberto, S. Fais, G. Fenu, P. Follesa,
A. Greco, F. Ledda, Al. Loi, A. Marchi, E. Marini, R. Medda, M. L. Mercuri, G. Mezzorani,
A. M. Musinu, P. Orrù, Padiglia, A. Pani, G. M. Pinna, M. Quartu, P. Ruggerone, E. Sanna,
R. Scateni, G. Spano, I. Tomassini Barbarossa, E. Tramontano.
Ricercatori confermati: M. Arca, F. Biggio, S. Cabiddu, C. M. Calò, F. Congiu, R. Corpino,
A. De Falco, M. Deiana, C. Floris, M. C. Fogu, D. Lera, I. Leurini, M. C. Loi, G. Mula, M.
Murenu, P. Muroni, R. Oldeman, B. Pes, M. P. Piu, T. Pivetta, A. Sabatini, M. D. Setzu, E.
Tamburini.
Ricercatori non confermati: C. Anedda, M. Atzori, P. C. Ricci, A. Seu.
Rappresentanti studenti: M. Camedda, R. Frau.
Rappresentanti personale tecnico-amministrativo: J. Pisano, A. Garau.
Sono assenti giustificati:
Professori ordinari e straordinari: S. Massidda.
Ricercatori confermati: U. D’Alesio.
Sono in congedo: P. Deplano , A. Devoto.
Sono assenti:
1
Professori ordinari e straordinari: A. Cau, P. Lattanzi, R.Crnjar, P. La Colla, G. D’Ambra, C.
Van Der Mee, A. Lai, F. Bertolino, G. Crisponi, M. Monduzzi, A. Rossi, G. L. Pillola, V.
Lippolis, P. P. Piras, N. D’Amico, P. Pittau, S. Pennisi, E. Sanna.
Professori associati: D. Atzei, E. Cadoni, M. Cadoni, M. Casu, R. Cidu, C. Corradini, A.
Corrias, S. De Muro, I. Ferino, V. Fiorentini, F. Frau, G. Ghiglieri, F. Isaia, L. Lecca, An.
Loi, M. Marchi, A. Marini, B. Marongiu, M. E. Marongiu, R. T. Melis, R. Monaci, V. M.
Nurchi, M. Polo, S. Salvadori, E. Sanjust, G. Seu, G. Usai.
Ricercatori confermati: P. Addis, M. C. Aragoni, G. Bande, F. Bernardini, A. Bosin, M. G.
Cabiddu, L. Cadeddu, C. Caltagirone, C. Cannas, R. Cannas, M. Caria, S. M. Carta, F.
Cesare Marincola, E. Coluccia, S. Columbu, L. G. Costamagna, G. Cruciani, F. Cuccu, M.
G. Cutrufello, G. D’Appolonio, B. De Giudici, A. Erdas, C. Fattuoni, R. Floris, A. L.
Funedda, A. Geddo-Lehmann, A. Ibba, R. Loddo, S. Montaldo, M. T. Mura, M. Mureddu,
S. Murgia, M. Musio, G. Navarra, M. B. Pisano, Porcedda, E. Rombi, S. M. Saba, M. Salis,
P. Scano, A. Serpe, P. Solari, S. Spiga, A. Vacca.
Ricercatori non confermati: M. Bartoletti, A. Frongia, M. Marignani.
Rappresentanti studenti: M. Agus, E. S. Aresu, W. Brambilla, V. Carracoi, A. Cuccu, A.
Demartis, M. Depau, S. Desogus, B. Figus, C. Frau, V. Genna, S. Lai, V. Lallai, M. M.
Marrocu, M. Massida, G. E. Mauriello, C. Oppo, F. C. Pasetto, C. Pateri, A. Pettinau, M.
Pinna, S. Pisano, G. Pischedda, G. Rota, V. Selis, M. Soggiu, J. Sorgia, F. Tuveri.
Preside la seduta il Prof. G. Biggio, è segretario il Prof. E. Sanna
1. Approvazione verbali sedute precedenti
Si sottopone all’approvazione del Consiglio di Facoltà i verbali della seduta del 24
novembre 2011, già messo a disposizione in rete per la consultazione.
La Facoltà approva a maggioranza con 7 astenuti
2. Conferma in ruolo ricercatori
La Facoltà di Scienze MM.FF.NN. dell'Università degli studi di Cagliari, su richiesta
dell’interessato ai fini della conferma nel ruolo di ricercatore, sentiti i Consigli di Classe e di
Dipartimento competenti per quanto attiene rispettivamente all’attività didattica e all’attività
scientifica, e alle altre funzioni complessivamente svolte, dichiara quanto segue:
Relazione dell’attività didattica e scientifica
Massimo Bartoletti
Massimo Bartoletti ha preso servizio il 03/11/2008 in qualità di Ricercatore Universitario (S.S.D. INF/01)
presso la Facoltà di Scienze MM. FF. NN. dell’Università degli Studi di Cagliari, ed afferisce al Dipartimento
di Matematica e Informatica della medesima Università.
Attività di ricerca
Nel triennio dal 3/11/2008 al 2/11/2011 l’attivit`a di ricerca di Massimo Bartoletti si `e focalizzata sulla
definizione di metodi e strumenti per la specifica, l’analisi e la verifica di propriet`a di software e sistemi
2
informatici, sulla sicurezza, sui linguaggi funzionali impuri, sulla teoria della concorrenza, e sulla teoria delle
dimostrazioni nei sistemi logici, sia da un punto di vista applicativo che prettamente fondazionale.
Nel seguito vengono brevemente delineati alcuni dei principali risultati di
ricerca raggiunti. Language-based security. Un primo filone di ricerca ha riguardato lo sviluppo di sistemi di
tipo ed effetto e di algoritmi di model-checking come supporto per la definizione di modelli di sicurezza per
linguaggi di programmazione.
In [8] `e stata definita una nuova classe di tipi ed effetti, caratterizzati da un binder _ `a la _-calcolo, che
permettono di approssimare il comportamento di _-termini impuri in presenza di un costrutto di freshness.
Questo ha permesso di estendere i precedenti approcci statici per l’analisi dell’uso di risorse, considerando
anche programmi che possono generare nuove risorse a tempo di esecuzione.
In [6] sono state studiate tecniche di enforcement di politiche di sicurezza
sulla storia dell’esecuzione di programmi. In particolare, sono state introdotte politiche “locali”, che
permettono ai programmatori di confinare le porzioni critiche del codice in delle “sandbox”. Il meccanismo di
enforcement garantisce che, all’interno di una sandbox, l’esecuzione del programma rispetti la politica data. Il
punto chiave `e come realizzare l’enforcement di politiche locali in modo da minimizzare il sovraccarico a
tempo di esecuzione.
A tal fine, in [6] `e stata definita una tecnica di analisi statica a due fasi (sistemi di tipi/effetti + model
checking), per verificare a tempo di compilazione se un dato programma rispetta o meno le politiche locali
richieste.
In [1, 2, 7] `e stata studiata una nuove classe di automi per modellare politiche di uso di risorse. Tali automi
hanno un alfabeto infinito di simboli di ingresso, cos`ı da modellare politiche che parlano di risorse non
ancora
conosciute a tempo statico. Per questi automi sono stati sviluppati un algoritmo di enforcement online, e una
tecnica di model checking (di complessità polinomiale) per decidere se l’approssimazione statica del
comportamento di un programma rispetta o meno la politica espressa dall’automa dato.
In [3, 4] le tecniche sviluppate nei lavori precedenti sono state applicate per implementare e sperimentare un
nuovo modello di sicurezza per Java,
basato sull’enforcement di politiche locali sulla storia dell’esecuzione. Orchestrazione sicura di servizi Web.
Un secondo filone di ricerca ha riguardato la progettazione di infrastrutture di servizi Web che rispettano
vincoli di sicurezza imposti da clienti e fornitori di servizi.
In [5, 9] `e stato proposto un framework linguistico in cui i servizi possono
proteggersi dai loro chiamanti, confinando all’interno di una sandbox le porzioni di codice critiche per la
sicurezza. Anche i chiamanti possono controllare il comportamento dei servizi invocati, fornendo una
opportuna politica di sicurezza al momento della chiamata. Il meccanismo di invocazione permette ai
chiamanti di richiedere servizi che non solo rispettano i vincoli di sicurezza desiderati, ma che rispettano
anche un dato “contratto” sul loro comportamento funzionale. Per orchestrare una applicazione basata su
servizi, viene costruito un “piano” che associa la sequenza di richieste a tempo di esecuzione con una
sequenza di servizi scelti per evadere le richieste.
Il problema principale `e quello del “planning”, ovvero come costruire un piano che garantisca l’adempimento
di tutti i contratti, e allo stesso tempo eviti violazioni alla sicurezza. Selezionare i servizi che rispettano
localmente i contratti richiesti dai clienti non `e sempre una buona scelta, poich´e il loro comportamento
potrebbe ripercuotersi sulla sicurezza globale della composizione.
La soluzione al problema del planning proposta in [5] prevede che,
quando un servizio viene pubblicato, questo sia accompagnato da una “interfaccia comportamentale”.
Diversamente dalle segnature sintattiche, questa interfaccia include un’astrazione della semantica del
servizio, nella forma di tipi annotati. Per ottenere un servizio dal comportamento desiderato, un cliente
interroga la rete alla ricerca di un’interfaccia corrispondente al comportamento richiesto. Per costruire
automaticamente questa interfaccia, è stato introdotto un sistema di tipi ed effetti. Il tipo di un servizio
descrive il suo comportamento funzionale, mentre l’effetto rappresenta le sequenze di azioni rilevanti per la
sicurezza. `E stata dunque ideata una tecnica di modelchecking per estrarre dal tipo/effetto di un sistema di
servizi tutti i piani “percorribili”, ovvero quelli che guidano con successo esecuzioni sicure.
Contract-oriented computing. Un altro filone di ricerca ha riguardato la progettazione di infrastrutture di servizi
in cui l’interazione tra i partecipanti è guidata da opportuni “contratti”. Tali contratti sono descrizioni astratte
del comportamento dei servizi, che permettono di specificare obblighi e i diritti di clienti e fornitori, cos`ı come
le sanzioni da applicare in caso di violazioni.
Un aspetto innovativo della ricerca consiste nel fatto che non si ipotizza che un servizio rispetti sempre un
contratto da questi stipulato. Ci`o permette di modellare vari tipi di attacchi, e di definire quando un servizio `e
“onesto” (ovvero, quando rispetta sempre tutti i contratti che ha stipulato).
In [11] `e stata introdotta la logica per contratti PCL. Tale logica estende
la logica proposizionale intuizionista con un connettivo di implicazione “contrattuale”. L’uso di tale connettivo
permette alle varie parti coinvolte in una contrattazione di stipulare un contratto in presenza di vincoli di
assume/guarantee circolari. La circolarità gioca in effetti un ruolo cruciale nell’ambito dei contratti: quel che
3
tipicamente avviene `e che, in situazioni di mutual distrust, nessuna delle parti `e disposta a “fare il primo
passo”, mentre un accordo è possibile se si trova una corrispondenza tra le mutue promesse e le mutue
richieste. Il principale risultato tecnico in [11] `e la decidibilità del proof system della logica PCL, ottenuta
attraverso l’eliminazione del taglio.
In [10, 11, 12] sono stati proposti calcoli per modellare servizi che basano
la propria interazione sull’uso di contratti. I calcoli proposti in [11, 12] estendono Concurrent Constraint
Programming con primitive per comunicare, stipulare e realizzare contratti, e sono ulteriormente estesi in [10]
per modellare sessioni multi-party tra le parti contraenti. Inoltre, mentre [11, 12] utilizzano contratti modellati
nella logica PCL, il calcolo in [10] astrae dall’effettivo modello dei contratti. Questo permette di confrontare
all’interno dello stesso framework modelli diversi di contratti, p.e. quelli basati sulla logica e quelli basati su
calcoli di processi `a la CCS. Il principale risultato tecnico in [10] `e proprio un encoding da contratti PCL in
contratti CCS-like, che garantisce che gli atomi deducibili nel sistema logico sono esattamente quelli
raggiungibili dal corrispondente processo.
In [13] `e stata proposta una analisi statica in grado di garantire quando un servizio, espresso come un
processo in un _-calcolo temporizzato asin-crono, garantisce di rispettare una data proprietà entro una data
scadenza temporale.
Attività relative a progetti di ricerca
Massimo Bartoletti `e stato ed `e coinvolto in progetti di ricerca nazionali (Progetto PRIN Soft “Tecniche
formali orientate alla sicurezza”) ed internazionali (EU-FETPI Global Computing Project IST-2005-16004
Sensoria “Software Engineering for Service-Oriented Overlay Computers”, EU F7-257414 Ascens
“Autonomic Service-Component Esembles”).
Massimo Bartoletti `e coordinatore scientifico di due progetti di ricerca finanziati dalla Regione Autonoma
della Sardegna con la L.R. 7/2007 (TESLA “Tecniche di Enforcement di Sicurezza per Linguaggi e
Applicazioni”, TRICS “A Trusted Reservation Infrastructure for Computational Societies”), per un
finanziamento complessivo di EU 285K.
Attività didattica
Massimo Bartoletti ha svolto attività didattica per i corsi di Laurea in Informatica
e di Laurea Magistrale in Informatica dell’Università di Cagliari. In particolare, ha tenuto i seguenti corsi:
• Architettura degli Elaboratori (A.A. 2008/09, 2009/10, 2010/11);
• Informatica Teorica (A.A. 2009/10, 2010/11);
• Fondamenti di Sicurezza (A.A. 2011/12).
Ha inoltre affiancato il Prof. G.M. Pinna nel corso di Linguaggi di Programmazione (A.A. 2009/10, 2010/11,
2011/12). `E stato relatore di 8 tesi di Laurea in Informatica. Alcuni suoi lavori sono stati oggetto di un corso
nella scuola internazionale di dottorato “Advanced applications of model-checking techniques” (SEFM School
2010).
Attività editoriali
Massimo Bartoletti è stato membro del comitato di programma di vari workshope conferenze internazionali
(AINA 2010, ARES 2010, FAST 2010, Bytecode 2012), e peer-reviewer per varie riviste e conferenze
internazionali.
Riferimenti bibliografici
[1] M. Bartoletti. Usage automata. In Proc. of ARSPA-WITS, volume 5511 of LNCS, pages 52–69. Springer,
2009.
[2] M. Bartoletti, L. Caires, I. Lanese, F. Mazzanti, D. Sangiorgi, H. T. Vieira, and R. Zunino. Tools and
verification. In Rigorous Software Engineering for Service-Oriented Systems - Results of the SENSORIA
Project on Software Engineering for Service-Oriented Computing, volume 6582 of Lecture Notes in Computer
Science, pages 408–427. Springer, 2011.
[3] M. Bartoletti, G. Costa, P. Degano, F. Martinelli, and R. Zunino. Securing Java with local policies. Journal
of Object Technology, 8(4), 2009.
[4] M. Bartoletti, G. Costa, and R. Zunino. Jalapa: Securing Java with local policies: Tool demonstration.
Electr. Notes Theor. Comput. Sci., 253(5):145–151, 2009.
[5] M. Bartoletti, P. Degano, and G. Ferrari. Planning and verifying service composition. Journal of Computer
Security, 17(5), 2009.
[6] M. Bartoletti, P. Degano, G. Ferrari, and R. Zunino. Local policies for resource usage analysis. ACM
Trans. Program. Lang. Syst., 31(6), 2009.
[7] M. Bartoletti, P. Degano, G. Ferrari, and R. Zunino. Model checking usage policies. Mathematical
Structures in Computer Science, To appear.
4
[8] M. Bartoletti, P. Degano, G. L. Ferrari, and R. Zunino. _-types for effects and freshness analysis. In Proc.
of ICTAC, volume 5684 of Lecture Notes in Computer Science. Springer, 2009.
[9] M. Bartoletti, P. Degano, G. L. Ferrari, and R. Zunino. Call-bycontract for service discovery, orchestration
and recovery. In M. Wirsing and M. M. H¨olzl, editors, Rigorous Software Engineering for Service-Oriented
Systems - Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing,
volume 6582 of Lecture Notes in Computer Science, pages 232 261. Springer, 2011.
[10] M. Bartoletti, E. Tuosto, and R. Zunino. Contracts in distributed systems. In Proc. of ICE, volume 59 of
EPTCS, 2011.
[11] M. Bartoletti and R. Zunino. A calculus of contracting processes. In Proc. of LICS. IEEE Computer
Society, 2010.
[12] M. Bartoletti and R. Zunino. Primitives for contract-based synchronization. In Proc. of ICE, volume 38 of
EPTCS, 2010.
[13] M. Bartoletti and R. Zunino. Static enforcement of service deadlines. In Proc. of SEFM. IEEE Computer
Society, 2010.
Tenuto conto di quanto sopra, il Consiglio di Facoltà di Scienze MM.FF.NN.
esprime unanime parere pienamente positivo sull’attività didattica, scientifica e sulle
altre attività complessivamente svolte dalla dott. Massimo Bartoletti
3. Chiamata ricercatore
La Facoltà è chiamata a deliberare sulla chiamata della dott.ssa Francesca Pintus,
vincitrice del concorso per 1 posto da ricercatore T.D. per Biologia Molecolare (SSD
BIO/11) settore concorsuale 05/E2.
La Facoltà approva all’unanimità
La Facoltà è chiamata a deliberare sulla chiamata del Dott. Matteo Falzoi, vincitore
del concorso per 1 posto da ricercatore T.D. per Genetica (SSD BIO/18) settore
concorsuale 05/I1.
La Facoltà approva all’unanimità
4. Provvedimenti insegnamenti vacanti
La Facoltà è chiamata ad esprimersi sull’affidamento al Prof. Luciano Colombo
del corso di "Fondamenti di Fisica della Materia" per il CdL in Fisica
Denominazione Corso di
Laurea
L30-Fisica
Nominativo
docente
Denominazione Insegnamento
COLOMBO Luciano
Fondamenti di Struttura della Materia
CFU
9
Carico
didattico
72
Anno
Corso
III
Sem
I-II
Tipologia
incarico
Affidamento
La Facoltà approva a maggioranza con 1 astenuto
Alle ore 11,20 il Decano in sede chiude la seduta.
IL SEGRETARIO
(Prof. Enrico Sanna)
IL DECANO
(Prof. Giovanni Biggio)
5