1. | Area Scientifico Disciplinare | 01: Scienze matematiche e informatiche | 100% |
---|
Testo italiano
Testo italiano
INF/01 - Informatica |
Testo italiano
BUGLIESI (Cognome) |
MICHELE (Nome) |
|
Professore Associato (Qualifica) |
31/05/1962 (Data di nascita) |
BGLMHL62E31L483K (Codice di identificazione personale) |
INF/01 - Informatica (Settore scientifico-disciplinare) |
||
Università "Cà Foscari" di VENEZIA (Università) |
||
Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI (Facoltà) |
||
Dipartimento di INFORMATICA (Dipartimento) |
||
041-2348437 (Prefisso e telefono) |
041-2348419 (Numero fax) |
michele@dsi.unive.it (Indirizzo posta elettronica) |
Testo italiano
1. | BUGLIESI M., CRAFA S., MERRO M., SASSONE V. (in stampa). Communication and Mobility Control in Boxed Ambients. INFORMATION AND COMPUTATION. ISSN: 0890-5401 To appear. |
2. | BUGLIESI M., ROSSI S. (2005). Non Interference Proof Techniques for the Analysis of Cryptographic Protocols. JOURNAL OF COMPUTER SECURITY. vol. 13 pp. 83-113 ISSN: 0926-227X |
3. | BUGLIESI M., FOCARDI R., MAFFEI M (2005). Analysis of Typed Analyses of Authentication Protocols. CSFW 2005 - Computer Security Foundation Workshop. Giugno 2005 In corso di stampa. |
4. | BUGLIESI M., CASTAGNA G., CRAFA S. (2004). Access Control for Mobile Agents: the Calculus of Boxed Ambients. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. vol. 26 pp. 57-124 ISSN: 0164-0925 |
5. | BUGLIESI M., COLAZZO D., CRAFA S. (2004). Type Based Discretionary Access Control. CONCUR 2004. August (vol. LNCS 3170 pp. 225-239). |
6. | BUGLIESI M., RICCARDO FOCARDI, MATTEO MAFFEI (2004). Compositional Analysis of Authentication Protocols. ESOP 2004. April (vol. LNCS 2986 pp. 140-154). |
7. | BUGLIESI M., CRAFA S., PRELIC A., SASSONE V. (2003). Secrecy in Untrusted Networks. LECTURE NOTES IN COMPUTER SCIENCE. (vol. 2719 pp. 969-983). (ICALP'03, Int. Colloquium on Automata Languages and Programming). |
8. | BONO V., BUGLIESI M., CRAFA S. (2002). Typed Interpretations of Extensible Objects. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. vol. 3(4) pp. 562-603 ISSN: 1529-3785 |
9. | BUGLIESI M., CRAFA S., MERRO M, SASSONE V. (2002). Communication Interference in Mobile Boxed Ambient. FSTTCS'02. (vol. LNCS 2556 pp. 71-84). |
10. | BUGLIESI M., PERICAS-G S. (2002). Type Inference for Variant Object Types. INFORMATION AND COMPUTATION. vol. 177(1) pp. 2-27 ISSN: 0890-5401 |
11. | BUGLIESI M., CASTAGNA G. (2001). Secure Safe Ambients. 28th ACM Symp. on Principles of Progrogramming Languages. Boston, Jan. 2001 (pp. 222-235). ACM Press. |
12. | BUGLIESI M., CASTAGNA G., CRAFA S. (2001). Boxed Ambients. TACS'01 Theoretical Aspects of Computer Software, 4th International Symposium. Senday, Oct.2001 (vol. 2215 of LNCS pp. 38-63). |
13. | BUGLIESI M., CASTAGNA G., CRAFA S. (2001). Reasoning about Security in Mobile Ambients. CONCUR 01 - Concurrency Theory, 12th International Conference,. Aug 2001 (vol. 2154 of LNCS pp. 102-120). |
14. | BONO V., BUGLIESI M. (1999). Matching for the Lambda Calculus of Objects. THEORETICAL COMPUTER SCIENCE. vol. 212 pp. 101-140 ISSN: 0304-3975 |
15. | BONO V., BUGLIESI M., LIQUORI L., DEZANI-CIANCAGLINI M. (1999). A subtyping for Extensible Incomplete Objects. FUNDAMENTA INFORMATICAE. vol. 38(4) pp. 325 - 364 ISSN: 0169-2968 June 1999. |
Unità | Responsabile Scientifico | Qualifica | Settore Disc. | Università | Dipart./Istituto | Mesi Uomo |
---|---|---|---|---|---|---|
I | BUGLIESI MICHELE | Professore Associato | INF/01 | Università "Cà Foscari" di VENEZIA | Dip. INFORMATICA | 12 |
II | COPPO MARIO | Professore Ordinario | INF/01 | Università degli Studi di TORINO | Dip. INFORMATICA | 11 |
III | DE NICOLA ROCCO | Professore Ordinario | INF/01 | Università degli Studi di FIRENZE | Dip. SISTEMI E INFORMATICA | 12 |
IV | SANGIORGI DAVIDE | Professore Ordinario | INF/01 | Università degli Studi di BOLOGNA | Dip. SCIENZE DELL'INFORMAZIONE | 13 |
Testo italiano
Numero | Mesi uomo 1° anno |
Mesi uomo 2° anno |
Totale mesi uomo | ||
---|---|---|---|---|---|
Personale universitario dell'Università sede dell'Unità di Ricerca | 11 | 59 | 58 | 117 | |
Personale universitario di altre Università | 2 | 6 | 6 | 12 | |
Titolari di assegni di ricerca | 1 | 4 | 4 | 8 | |
Titolari di borse | Dottorato | 8 | 48 | 24 | 72 |
Post-dottorato | 1 | 6 | 0 | 6 | |
Scuola di Specializzazione | 0 | ||||
Personale a contratto | Assegnisti | 2 | 10 | 17 | 27 |
Borsisti | 0 | ||||
Dottorandi | 0 | ||||
Altre tipologie | 0 | ||||
Personale extrauniversitario | 3 | 6 | 8 | 14 | |
TOTALE | 28 | 139 | 117 | 256 |
Numero | Mesi uomo 1° anno |
Mesi uomo 2° anno |
Totale mesi uomo | ||
---|---|---|---|---|---|
University Personnel | 11 | 59 | 58 | 117 | |
Other University Personnel | 2 | 6 | 6 | 12 | |
Work contract (research grants, free lance contracts) | 1 | 4 | 4 | 8 | |
PHD Fellows & PHD Students | PHD Students | 8 | 48 | 24 | 72 |
Post-Doctoral Fellows | 1 | 6 | 0 | 6 | |
Specialization School | 0 | ||||
Personnel to be hired | Work contract | 2 | 10 | 17 | 27 |
PHD Fellows & PHD Students | 0 | ||||
PHD Students | 0 | ||||
Other tipologies | 0 | ||||
No cost Non University Personnel | 3 | 6 | 8 | 14 | |
TOTALE | 28 | 139 | 117 | 256 |
Testo italiano
Obiettivi e approccio
Lo scopo del progetto è di far progredire lo stato dell'arte sulle
tecniche proprie della teoria della concorrenza per l'analisi e la
verifica del software, estendendole in modo da renderle efficaci sia
nell'analisi di proprietà complesse, sia in presenza di ipotesi più
deboli sulle componenti del sistema. Ad alto livello gli obiettivi del
progetto hanno una doppia valenza ed includono:
. lo sviluppo di nuovi modelli astratti per descrivere computazioni
distribuite in sistemi con mobilità. Questi modelli saranno basati su
calcoli di processo e forniranno la base per condurre analisi formali
sull'esecuzione e sulla mobilià del codice, sull'esplorazione del
contesto di esecuzione, descritte in termini delle proprietà
osservabili rilevanti in tali computazioni.
. lo sviluppo di tecniche formali, basate su sistemi di tipo e teorie
logiche, per la specifica e verifica del comportamento di programmi
concorrenti. Tali tecniche dovranno rendere possibile esprimere le
politiche di autorizzazione per la migrazione del codice in ambienti
computazionali remoti, e allo stesso tempo permettere il controllo dei
meccanismi di accesso, protezione, negoziazione ed utilizzo delle
risorse disponibili in tali ambienti.
Il nostro approccio sarà incentrato sullo sviluppo dei fondamenti
teorici alla base delle tecniche di specifica ed analisi, con lo scopo
di identificare nozioni unificanti e produrre strumenti formali
flessibili e adattabili. Allo stesso tempo, svolgeremo una attività
complementare di ricerca su casi di studio per valutare i risultati
teorici, il loro progresso e la loro adeguatezza.
Sul piano delle tecniche, la nostra ricerca si fonderà su modelli
operazionali e sistemi "proof theoretic". La ricerca nell'area della
teoria della concorrenza ha da tempo prodotto strumenti potenti per
ragionare sul comportamento "contestuale" di processi concorrenti, e
per analizzare e specificare il loro comportamento tramite tipi e
sistemi logici. Negli anni questi strumenti hanno trovato una sempre
più ampia applicazione nei calcoli di processi del prim'ordine e, in
una certa misura, anche nei calcoli con mobilità di nomi come il
pi-calcolo. Nella presente proposta, intendiamo estendere le tecniche
esistenti a processi e sistemi le cui componenti siano mobili,
distribuite, possibilmente non fidate. Proponiamo l'uso di tipi e
formule logiche come interfacce, o come contratti, che esprimano e
regolino la negoziazione per l'acquisizione delle risorse tra i
processi e gli ambienti circostanti. L'uso di caratterizzazioni logiche
e coinduttive delle corrispondenti equivalenze comportamentali fornirà
la base per l'analisi formale degli effetti osservabili dell'esecuzione
dei processi. Saranno richieste tecniche innovative per fornire
adeguate caratterizzazioni dell'uso e della gestione delle risorse -
limiti, protezione, autorizzazione, confinamento. Analogamente, nuove
tecniche saranno necessarie per formalizzare meccanismi che consentano
al codice cliente di scoprire/acquisire le sue risorse, spostandosi in
una rete distribuita con connettività e struttura dinamiche, e con
diritti di accesso/autorizzazioni ugualmente dinamici.
L'analisi statica, basata sui tipi e su sistemi logici è la soluzione
che proponiamo per rendere sicure ed efficienti computazioni che devono
adattarsi sulla base delle informazioni relative al loro contesto.
Questa analisi contribuirà a dotare il codice cliente di certificati
verificabili che ne dimostrino la conformità alle politiche di
controllo dell'ambiente ospite in merito a diversi aspetti, che vanno
da garanzie di segretezza e integrità dei dati, a garanzie di uso
limitato delle risorse di sistema.
Le tecniche e gli strumenti di verifica sviluppati nel progetto
verranno valutati su un insieme di casi di studio. Se da un lato
l'identificazione dei casi di studio costituisce di per sè oggetto di
studio, abbiamo al momento già identificato due esempi significativi.
Il primo riguarda la specifica ed analisi di protocolli per la
comunicazione e l'instradamento in reti wireless "ad hoc". Se da un
lato le reti "ad hoc" sono interessanti di per sè per la loro natura
profondamente dinamica, dall'altro i protocolli di instradamento in
tali reti sono rilevanti all'interno del progetto poiché, vista la loro
natura tipicamente cooperativa, essi richiedono la capacità di
stabilire adeguate forme di "trust" tra i partecipanti
all'instradamento e, dualmente, di proteggersi da componenti verso le
quali non è disponibile sufficiente informazione per stabilire adeguati
livelli di trust. Il secondo scenario riguarda la pratica, sempre più
comune tra gli utenti, di scaricare codice remoto per mandarlo in
esecuzione sui propri dispositivi (portatili o palmari). Nell'ambito
del progetto, studieremo tecniche per rilevare attacchi di vario tipo,
da attacchi alla sicurezza ed integrità dei dati, ed attacchi di tipo
"denial-of-service" da parte di agenti ostili che degradano le
prestazioni del sistema ospite sovra-utilizzandone le risorse.
Lo scopo dei casi di studio è duplice. Da una parte, permetterà di
stimolare il lavoro sulle techniche di specifica e di analisi fornendo
problemi specifici. Dall'altro lato, fornirà un indicatore misurabile
per valutare il progresso del progetto e la qualità dei suoi risultati.
Per una descrizione dettagliata delle attività di progetto è si rimanda alla sezione "workplan" della proposta.
Objectives and approach
The purpose of the project is to advance the state of the art on
concurrency theoretic techniques for software analysis and
verification, so as to make them (i) more expressive, hence able to
capture the relevant observable properties of distributed computations,
and (ii) effective under the weaker and possibly partial assumptions on
structure behavior distinctive of the systems and applications of the
computing environments of interest. Generally stated, the objective of
the project is twofold, and includes:
. The study of abstract models of mobile computation in distributed
environments, based on process calculi. Such models will support formal
reasoning on code execution and migration, context exploration and
adaptive behavior based on new, resource-oriented observables and
associated behavioral equivalences.
. The development of formal techniques, based on types and logical
systems, for the specification and verification of concurrent program
behavior. Such techniques should make it possible to express the
admission/authorization policies for code migration to remote
computational environments and, dually, to control the mechanisms of
access, negotiation, monitoring, protection and use of the local
resources available at such environments.
Our approach will be centred on theory, with the goal of isolating core
unifying notions to yield effective techniques for analysis and
verification tools, but at the same time complemented by work on case
studies to assess the theoretical results and evaluate their advance.
The theoretical work we plan draws on operational models and
proof-theoretic tools for analysis and verification. The theory of
concurrency has long provided powerful foundational tools for reasoning
on the (contextual) behavior of concurrent processes, and for analyzing
and specifying their behavior by means of type and logical systems.
Consolidated progress has been made over the years on applying these
tools on first-order process calculi and, to some extent, also to
calculi for name mobility like the pi-calculus.
In the context of the present proposal, we seek to extend the existing
techniques to processes and systems whose components are mobile,
distributed, open, (partially) typed, possibly untrusted.
We propose to use types and logical formulas as interfaces, or as
contracts, expressing and governing the negotiation for resource
acquisition between processes and their environments. The use of
coinductive and logical characterizations of the corresponding
behavioral equivalences will then provide finitary representations of
contexts and serve as the basis for formal analysis of the observable
effects of process execution in such contexts. Innovation will be
required to find adequate characterizations of resource usage and
management - bounds, protection, authorization, confinement. Similarly,
novel techniques will be needed to formalize mechanisms for client code
to discover and acquire its resources, by migrating over a distributed
network with dynamic spatial structure and connectivity and dynamic
access/authorization rights.
Static analysis, based on type and logical (inference) systems, is our
proposed solution to reduce the overhead incurred by executions that
need to self-tune on the basis of the context information. Such
analysis will contribute to provide verifiable certificates for client
code to prove that it complies with the access control policies of its
hosting environment. Similarly, they will provide estimates of resource
usage to help minimize the cost of the run-time accesses to context
information.
The techniques and tools developed will be put to test on a set of case
studies. While finding relevant cases of study is in itself an
objective of the project, we already have plans to work on two, largely
orthogonal scenarios. The first concerns the specification and analysis
of protocols to regulate communication and routing in wireless ad-hoc
networks. While ad-hoc networks are interesting in themselves for the
mobility-intensive nature, the routing protocols are relevant for the
project as they are cooperative in nature and require adequate forms of
trust to be established among the peers that participate in the
routing. As such, these protocols provide a significant example of the
consequences of absence of centralized control and trust in distributed
computations. The second scenario addresses the nowadays common
practice by users to dowload code to run on their devices --laptops,
PDAs, etc. The focus here will be on techniques to detect and
anticipate various security threats, from attacks to the privacy and
integrity of data to denial-of-service attacks based on over-use of
system resources, mounted by malicious agents hosted in the downloaded
code.
The purpose of the work on case studies is twofold. On one hand, it
will help concretely stimulate and steer the theoretical work by
providing problem-specific challenges and continued feedback to the
activities in workpackages WP1-3. On the other side, it will provide a
measurable indicator to evaluate the project's progress towards its
objectives and to assess the quality of its results.
The structure and a detailed account of the project activities is given the workplan section of the present proposal.
Testo italiano
Sistemi di tipo
Negli ultimi anni le problematiche legate al controllo delle risorse e
della mobilità , in forme diverse, sono state un tema cardine della
ricerca di base nella teoria dei tipi. Gli argomenti considerati
comprendono l'analisi di aspetti quali: l'abilità di leggere da /
scrivere su un canale [PS96], il controllo della distribuzione dei nomi
dei canali [YH99], la garanzia che gli agenti mobili utilizzeranno le
risorse solo dopo essere stati autorizzati [HR02,DFPV00,BC01,HMR03], il
controllo dell'interferenza [LS03], il controllo della mobilità degli
agenti eventualmente basata su permessi specificati mediante tipi
[DS00,MS02,CGG02,CDGS03], le garanzie di safety per gli scambi
all'interno di ambienti di calcolo locali [CGG02], la segretezza di
tali scambi [CGG00], il controllo della diffusione e condivisione di
informazioni basato sul contenuto e sul contesto [Mye99,CDV03].
La maggior parte dei sistemi suddetti, con poche eccezioni, si fonda su
tecniche di tipizzazione classiche nelle quali ad ogni componente del
sistema è assegnato un tipo sulla base di assunzioni stabilite a
livello globale. Questo approccio nonè certamente realistico in
ambienti distribuiti e dinamici come quelli di interesse per il
progetto. Una soluzione che consente di superare questa limitazione
consiste nell'utilizzare primitive crittografiche per proteggere gli
agenti mobili trusted (ovvero, tipati) dagli ambienti untrusted che
tali agenti attraversano. Quindi il sistema di tipo separa il codice
trusted da quello untrusted, permettendo interazioni, che vengano
giudicate sicure, con siti non trusted [BCPS03]. Una soluzione
alternativa si basa sul type checking dinamico, che consente di
verificare, al momento dell'interazione, le assunzioni locali fatte sui
componenti remoti [BC01,HR02,DFPV00]. In alcuni casi [BC01,CDGS03] le
tecniche di type checking dinamiche sono formulate in termini di
sistemi di inferenza di tipo, in grado di estrarre informazioni di tipo
da un codice (non tipato) al fine di approssimarne il comportamento.
Tali tecniche sono particolarmente rilevanti ed efficaci nel caso di
sistemi che ammettono tipo principale, proprietà che risulta essenziale
per un analisi composizionale dei tipi [W02]. Per estrarre informazioni
sul comportamento di termini dei calcoli per la mobilità , tipati o
meno, sono state utilizzate anche altre tecniche di analisi statica.
Ricordiamo, tra queste, l'attività sulla flow analysis [DLB00,BDNN01],
sull'interpretazione astratta [NHN99] e sulle logiche modali [CG00].
Una linea di ricerca complementare nell'ambito dei sistemi di tipo si
concentra sulla certificazione di limiti sul consumo delle risorse. Tra
i riferimenti rilevanti ricordiamo [Hof02,HJ03], dove si introduce una
nozione di "tipo risorsa" in grado di rappresentare un'unità di spazio
astratta e si utilizza un sistema di tipo lineare al fine di garantire
che la computazione richieda uno spazio lineare; [CW00] dove l'uso di
un linguaggio assembly tipato consente di stabilire dei limiti
quantitativi sul tempo di esecuzione; e [IK02] che propone una
formulazione generale di analisi dell'uso delle risorse. Nel contesto
dei calcoli concorrenti e distribuiti ricordiamo [GHS02], che presenta
un calcolo in cui le risorse possono essere trasportate da una
locazione all'altra, a condizione che nella locazione di destinazione
vi sia sufficiente spazio; [TZH02,BBDS03] che usa i sistemi di tipo per
controllare l'uso ed il consumo delle risorse; e [CGT02] che adotta
tecniche statiche per analizzare il comportamento di processi con
controllo finito, ovvero processi con capacità limitata di allocazione
di ambienti e di creazione di output.
Equivalenze comportamentali
Un'equivalenza comportamentale identifica due processi quando questi
"si comportano allo stesso modo" in tutti i possibili contesti, ovvero
in tutti gli ambienti nei quali possono essere utilizzati. Il
comportamento dei processiè determinato da come questi interagiscono
con l'ambiente e dagli effetti che producono su di esso. Nelle teorie
classiche della concorrenza (dove sono assenti distribuzione e
tipizzazione) il comportamento viene rappresentato dalle azioni che i
processi possono eseguire ed è, in genere, formalizzato tramite la
semantica operazionale strutturata. Quindi due processi sono
considerati equivalenti quando possono "eseguire le stesse azioni".
La nozione di equivalenzaè particolarmente utile per giustificare
formalmente le tecniche di trasformazione dei programmi ("è possibile
rimpiazzare un programma P con un programma Q perché essi hanno lo
stesso comportamento in tutti i contesti"), utilizzate sia dai
programmatori durante lo sviluppo di software che dai compilatori nelle
fasi di ottimizzazione. Tali trasformazioni richiedono però che le
relazioni di equivalenza siano congruenze. e quindi che siano
preservate da tutti gli operatori del calcolo, una proprietà che
risulta fondamentale anche per poter ragionare in modo composizionale
su sistemi complessi.
Sono state definite diverse nozioni di equivalenza comportamentale tra
processi (una buona rassegnaè presentata da van Glabbeek in [Gla93]).
In particolare l'equivalenza "testing" [DeHe84] e quella basata sulla
bisimulazione [Pa81] si sono dimostrate tra le più utili e stabili. A
partire dagli studi di Hennessy e Milner [HeMi85], queste equivalenze
sono state messe in relazione con logiche modali, caratterizzando
l'equivalenza tra processi in termini di equisoddisfacibilità di
proprietà modali, e con teorie algebriche che permettono di trasformare
processi a stati finiti in processi equivalenti utilizzando tecniche di
riscrittura. Altre tecniche per verificare l'equivalenza tra processi
sono quelle operazionali basate sulla coinduzione. Particolarmente
importante è il caso della bisimulazione e delle "tecniche up-to"
[Mil89,San98] basate sul rafforzamento del principio di coinduzione.
Tutti questi risultati sono in genere consolidati nel caso "classico"
dei calcoli di processi à la CCS e, in qualche modo, anche per i
calcoli puri per la mobilità come il pi-calcolo (con il termine "puro"
si vuole intendere la presenza di mobilità , data dal fatto che i nomi
possono essere comunicati, ma nè tipi nè primitive per la distribuzione
sono considerate in questi calcoli). Nel pi-calcolo, tuttavia, lo
sviluppo di strumenti per l'analisiè stato nettamente minore rispetto
al caso dei calcoli classici.
Le equivalenze comportamentali per calcoli che supportano mobilità di
codice e agenti, con locazioni distribuite e topologie di rete
complesse, hanno ricevuto una crescente ma purtroppo ancora limitata
attenzione in letteratura. I primi lavori in quest'area [LS03,BCMS04]
mostrano che concetti come la mobilità e la distribuzione hanno un
forte impatto sui problemi classici della teoria della concorrenza, ad
es. sull'interferenza, con effetti non trascurabili sulle teorie
algebriche e sugli algoritmi di verifica. Anche la mobilità stessa crea
difficoltà sorprendenti nella modellazione di semplici equivalenze
basate sulla bisimulazione e nell'individuazione di caratterizzazioni
coinduttive di equivalenze contestuali [GHS02,CZ02,MZ03]. Difficoltà
simili si riscontrano quando si utilizzano i tipi per disciplinare il
comportamento dei processi con forme di controllo degli accessi
[PiSa00] e della mobilità del codice [HMR03, HRY03].
Le equivalenze comportamentali per i calcoli di processi sono state
studiate anche nell'approccio conosciuto come "semantica logica" nel
quale gli elementi di un calcolo sono interpretati come l'insieme
(filtro) delle proprietà che essi soddisfano. Queste proprietà sono di
solito espresse come tipi, stabilendo così una dualità tra i termini
del calcolo e i loro tipi (proprietà ), che spesso rappresentano in
modo approssimato il comportamento dei processi. Quest'ideaè stata
approfondita e studiata in diversi articoli sulla teoria dei calcoli
dei processi. Sono stati costruiti modelli a filtro per il pi-calcolo
[HH97, DDG99], il calcolo degli ambienti [CD02,MZ04] e alcune sue
estensioni ad oggetti [BdL03]; le teorie equazionali di questi modelli
sono state messe in relazione con equivalenze osservazionali tra
processi. Esistono relazioni interessanti tra sistemi di tipo
soggiacenti ai modelli a filtro e sistemi di transizione etichettati,
come mostrato in [MZ04].
Logiche di Specifica
Il lavoro sulle logiche per sistemi distribuiti si è sviluppato nella
letteratura recente in direzioni diverse. La logica per gli ambienti
[CG00]è una logica modale, solidamente basata sul calcolo degli
ambienti, che& egrave; in grado di trattare tanto lo spazio quanto
il tempo. Questa logica è dotata di operatori che permettono di fare
asserzioni sulle locazioni e sui loro nomi, e di esprimere loro
proprietà . Un approccio collegato è quello seguito per Klaim, dove è
stata adottata una logica temporale per specificare e verificare
proprietà dinamiche di agenti mobili eseguiti su reti di larga scala.
Inoltre, le logiche spaziali e temporali sono anche utili per
analizzare sistemi aperti, dove le componenti possono essere
dinamicamente connesse per interagire con i servizi di rete. Di
particolare interesse in questo contesto è il nuovo approccio per la
modellizzazione di sistgemi aperti basato sui "bigrafi", un formalismo
che sta emergendo come una generalizzazione di molti calcoli di
processo esistenti.
Le logiche modali e temporali si sono dimostrate efficaci come
formalismi per la specifica e la verifica di proprietà di sistemi
concorrenti, e diversi strumenti software sono stati sviluppati per
supportare tali attività . La logica di Hennessy-Milner, il mu-calcolo,
CTL, CTL*, ACTL si sono affermati come strumenti utili per descrivere e
stabilire proprietà di sistemi concorrenti modellati per mezzo di
calcoli di processi. Facendo seguito al lavoro di Hennessy e Milner
[HeMi85], varie corrispondenze sono state fissate in [BCG88], dove due
equivalenze sulle strutture di Kripke (sistemi di transizione con nodi
etichettati) sono state messe in relazione con varianti di CTL*, e in
[DV95] dove CTL e HML sono state messe in relazione con la
bisimulazione branching.
Il crescente utilizzo delle reti su larga scala e la computazione
pervasiva, insieme con l'introduzione di nuovi paradigmi e linguaggi
che modellano l'interazione tra attori differenti (possibilmente
mobili), ha suscitato un rinnovato interesse per lo studio di nuove
logiche. Per queste nuove classi di programmi, come per i formalismi
concorrenti, è cruciale avere strumenti per stabilire proprietà quali
l'assenza di deadlock, la liveness e la correttezza rispetto a
specifiche date. Comunque, per questa nuova classe di sistemi, è anche
importante stabilire altre proprietà riguardanti l'allocazione e l'uso
delle risorse e la diffusione delle informazioni. Per tale motivo,
l'uso delle logiche modali per specificare e verificare proprietà di
sistemi mobili ha trovato ampia diffusione. Le proprietà sono
specificate per mezzo di operatori modali spaziali e temporali e quindi
verificate tramite sistemi di prova o con il supporto di model checker.
Nell'approccio basato sui sistemi di prova vengono fornite delle regole
di inferenza che consentono di costruire dimostrazioni formali del
fatto che le formule di interesse sono soddisfatte dai sistemi
studiati. Nell'approccio basato su model checking viene introdotta,
invece, una metodologia per verificare automaticamente se un sistemaè
un modello formale di una formula data. Le logiche per calcoli di
processi con mobilità sono state studiate in diversi articoli. A
seguire riportiamo una breve panoramica dei riferimenti presenti in
letteratura che sono rilevanti per gli scopi della presente proposta.
[MPW93] introduce una logica modale per il pi-calcolo. Questa logica,
che mira a catturare le differenti equivalenze tra i processi e a
stabilire le diversità tra la bisimulazione late e la early, è basata
sulla logica di Hennessy e Milner ma non ha operatori per la
ricorsione. In [D96]è presentata una logica, ispirata alla logica di
Hennessy-Milner con ricorsione, per il pi-calcolo. Questa logica è
dotata di un sistema di prova basato su tableau, ma non offre operatori
per trattare proprietà spaziali e la mobilità degli agenti.
[CG00] presenta una logica modale per gli Ambienti Mobili. Tale logica,
solidamente basata sul calcolo degli Ambienti, permette di descrivere
sia proprietà spaziali che proprietà temporali. È dotata di operatori
logici che possono essere usati per fare asserzioni sulle locazioni e
sui loro nomi, e permette di esprimere proprietà di natura piuttosto
intensionale [San01]. Il lavoro sulle logiche spaziali per i sistemi
distribuiti è quindi proseguito in diverse direzioni.
[CC01] introduce una variante della logica per gli ambienti adattata al
pi-calcolo asincrono. Questa interessante logica è dotata di operatori
per la specifica di proprietà temporali e spaziali, e per la specifica
composizionale di proprietà di sistemi. In [CG01] sono stati introdotti
nuovi operatori per esprimere proprietà logiche dei nomi ristretti.
Questa logica consente di specificare configurazioni spaziali e
numerose proprietà di computazioni mobili, comprese le proprietà di
sicurezza.
[DL04] sviluppa una logica temporale per la specifica di proprietà nel
linguaggio Klaim [DPF98]. Questa logica, ispirata alla logica di
Hennessy-Milner e al mu-calcolo, presenta nuove caratteristiche che
permettono di catturare sia proprietà degli stati che l'impatto delle
azioni e dei movimenti degli agenti sui diversi siti. La logica è
dotata di un sistema di prova che consente la verifica di proprietà per
sistemi mobili. Le logiche temporali sono state studiate anche
nell'ambito dell'approccio ai sistemi concorrenti basato sulla teoria
degli automi, con lo sviluppo di tecniche di verifica fondate sul
model-checking. Gli automi History Dependent, che sono in grado di
allocare e deallocare i nomi dinamicamente, sono stati introdotti e
utilizzai per la verifica di (frammenti finiti di) calcoli con
causalità , località e mobilità [FGMP04].
Type systems
Resource and mobility control, in diverse
incarnations, has been the focus of extensive foundational research in
type theory. Topics considered include the ability to read from and to
write to a channel [PS96], the control of the location of channel names
[YH99], the guarantee that distributed agents will access resources
only when allowed to do so [HR02,CGZ01,BCC01,HMR03], the control of
interference [LS03], the control of mobility, based on type-based
permissions [DS00,MS02,CGG02,CDGS03], the guarantee of safety within
local computational environments [CGG02], their secrecy [CGG00], the
control on the flow and sharing of information, based on content and
context [Mye99,CDV03].
With few exceptions, most of these systems rely on classical
typing techniques whereby all the system components are type-checked
under the same global typing assumptions. This is clearly unrealistic
in distributed and dynamic environments as the ones of interest to the
project. One solution to overcome this limitation is to rely on
cryptographic primitives to protect trusted (i.e. typed) migrating
agents against the untrusted sites they traverse, and to rely on a type
system that separates trusted and untrusted code, while allowing safe
interactions with untrusted sites [BCPS03]. An alternative solution is
to rely on dynamic type checking, to contrast and validate the local
assumptions made about remote components when such components interact
[BC01,HR02,DFPV00]. In some cases [BC01,CDGS03] dynamic typing
techniques have been formulated in terms of type inference systems
extracting typing informations from untyped code to approximate the
code's behavior. Such techniques are especially relevant, and
effective, for systems which admit principal types, or typings, a
property which is essential for compositional type analysis [W02].
Other static analysis techniques have been applied to extract
information on the behavior of terms of typed or untyped calculi with
mobility. Relevant references include flow analysis [DLB00,BDNN01],
abstract interpretation [HJNN99], modal logics [CG00].
A complementary line of research on type systems focuses on the
certification of bounds on resource consumption. Relevant references
include the following ones: [Hof02,HJ03] introduce a notion of resource
type representing an abstract unit of space, and uses a linear type
system to guarantee linear space consumption; [CW00] enforces
quantitative bounds on time usage using a typed assembly language;
[IK02] puts forward a general formulation of resource usage analysis;
more recently [CEI+05] proposes a new resource management paradigm that
combines static and dynamic checks in a novel way. Briefly, the
approach is based on the use of explicit language constructs to
dynamically verify the availability of the required resources, and
static analysis to verify that the dynamic checks enforce the resource
intended bounds policies. In the context of distributed and concurrent
calculi, relevant references include [GHS02], which presents a calculus
in which resources may be moved across locations provided suitable
space is available at the target location; [TZH02,BBDS03], which use
typing systems to control resource usage and consumption; and [CGT02],
which uses static techniques to analyze the behavior of finite control
processes, i.e., those with bounded capabilities for ambient allocation
and output creation.
Behavioral equivalences
Behavioral equivalences equate processes that "behave in the same way"
in all contexts, that is, under all environments in which they could
possibly be used. The behavior of processes is determined by how they
interact with, or affect, such environments. In classical theories of
concurrency (where processes are undistributed, untyped) the behavior
is represented by the actions that the processes can perform, and
formalized in the framework of Structural Operational Semantics. Thus
processes are deemed equivalent if they can "perform the same actions".
Equivalence is particularly useful as a tool for justifying program
transformations, ("we can validly replace P by Q because they have the
same behavior in all contexts"), performed either by programmers during
system development or by optimizing phases of compilers. Such
transformations require equivalences relations to be congruences, i.e.
preserved by all operators of the underlying calculi, a property that
is also fundamental to perform compositional reasoning on complex
systems.
Several notions of behavioral equivalence on processes have been
defined (see for instance van Glabbeek's review [Gla93]). Among these,
testing equivalence [DeHe84] and bisimulation equivalence [Pa81] have
emerged as the most useful and stable. Beginning with work of Hennessy
and Milner [HeMi85], they have been closely coupled with the use of
various modal logics to characterize equivalent processes in terms of
equi-satisfaction of modal process properties, and algebraic theories
to transform finite-state equivalent processes by means of rewriting
techniques. Another form of techniques developed for equivalence
checking are operational techniques based on co-induction. This is
especially important in the case of bisimulation, and includes
strengthenings of the co-induction principle underlying bisimulation,
called "up-to techniques" [Mil89,San98].
All of this is well-understood for the `classical' case of simple,
CCS-like process calculi and, to some extent, for pure calculi of
mobility like the pi-calculus (by pure we mean that there is mobility
since names can be communicated, but there are no type and no
primitives for distribution). Even in the pi-calculus, however, tools
for analysis have had a limited development compared to that for
classical process calculi.
Theories of behavioral equivalences for calculi of code and agent
mobility, with distributed locations and complex network topologies
have received increasing but still limited attention in the recent
literature. Initial work in this area [LS03,BCMS04] shows that mobility
and distribution have deep impact on classical problems in the theory
of concurrency, such as interference, with serious effects on the
algebraic theory and algorithms for verification. Mobility also creates
unexpected difficulties in modelling simple notions of bisimilarity,
and in providing coinductive characterizations of contextual
equivalences [GHS02,CZ02,MZ03]. Similar difficulties arise when types
are employed to discipline behavior with forms of access control
[PiSa00], and to control code mobility [HMR03, HRY03].
Behavioral equivalences for process calculi have also been studied in
the approach known as "logical semantics" in which the elements of a
calculus are interpreted as the set (filter) of the properties they
satisfy. These properties are usually expressed as types, thus
establishing a duality between a term of the calculus and its types
(properties), which often represent approximate process behaviors. This
idea has been investigated in several papers on the theory of process
calculi. Filter models have been built for the pi-calculus [HH97,
DDG99], Ambient Calculi [CD02,MZ04] and extensions of ambient calculi
with objects [BdL03]; the equational theories of these models have been
related to observational equivalences among processes. Relations
between type systems underlying filter models and labelled transition
systems exist as it is shown in [MZ04].
Specification logics
The work on logics for distributed systems has evolved along several
directions in the recent literature. The ambient logic [CG00] is a
modal logic, solidly based on the ambient calculus, that can talk about
space as well as time. It has logical operators that can be used to
make assertions about locations and their names, and express their
properties. A related approach has been taken for KLAIM, with temporal
logics employed to specify and verify dynamic properties of mobile
agents running over a wide area network. Spatial/temporal logics are
also useful for the analysis of open systems, where components can be
dynamically connected to interact with network services. Of particular
interest in this context is the novel approach to model dynamic open
systems based on bigraphs [JM04], which are emerging as a
generalisation of several process calculi.
Modal and temporal logics have been proved useful formalisms for
specifying and verifying properties of concurrent and different tools
have been developed to support such activities. Hennessy-Milner Logic,
mu-calculus, CTL, CTL*, ACTL have proved to be useful tools for
describing and establishing properties of concurrent systems described
as process calculi. Following the work of Hennessy and Milner [HeMi85],
various correspondences have been established in [BCG88], where two
equivalences over Kripke structures (node-labeled transition systems)
are related to two variants of CTL* and in [DV95] where CTL and HML are
related to branching bisimulation.
The increasing use of wide area networks and pervasiveness of
computing, together with the introduction of new programming paradigms
and languages that model interactions among different (possibly mobile)
actors have created revived interest in the study of new logics. For
the new class of programs, like for concurrent formalisms, it is
crucial to have tools for establishing deadlock freeness, liveness and
correctness with respect to given specifications. However, for this new
class of systems, it is also important to establish other properties
such as resources allocation, access to resources and information
disclosure. To this purpose, the use of temporal logics for specifying
and verifying dynamic properties of mobile systems has been advocated
and pursued. Properties are specified by means of temporal and spatial
modalities and then verified, either proof-theoretically, or with the
aid of model checkers. In the proof system approach, inference rules
are provided in order to build proofs that establish the satisfaction
of formulae by systems. In the model checking approach, a methodology
is introduced to verify automatically whether a system belongs to the
to the formal model of a formula.
Logics for process calculi with mobility have been studied in various
papers. Below we briefly outline the references to the literature that
are relevant to our present purposes.
[MPW93] introduces a modal logic for the pi-calculus. This logic aims
at capturing different equivalences between processes and at
establishing the differences between late and early bisimulation. It is
based on Hennessy-Milner Logic (HML) but it has no operators for
recursion. In [D96] a HML-like logic with recursion for pi-calculus is
presented. This logic is equipped with a tableau-based proof system but
has no operator for dealing with spatial properties and agent mobility.
[CG00] presents a modal logic for Mobile Ambients. It is a modal logic,
solidly based on the Ambient calculus, that can talk about space as
well as time. It has logical operators that can be used to make
assertions about locations and their names, and can express also rather
intensional properties [San01]. The work on spatial logics for
distributed systems has since then evolved in several directions.
[CC01] introduces a variant of the Ambient logic, tailored for
asynchronous pi-calculus. This very interesting logic is equipped with
operators for spatial and temporal properties, and for compositional
specification of systems properties. In [CG01], new operators for
expressing logical properties of name restrictions have been added.
This logic supports the specification of spatial configurations and of
a variety of properties of mobile computation, including security
properties.
[DL04] develops a temporal logic for specifying properties of Klaim
[DFP98]. The logic is inspired by Hennessy-Milner Logic and the
mu-calculus, but has novel features that capture state properties and
the impact of actions and movements over the different sites. The logic
is equipped with a complete proof system that enables one to prove
properties of mobile systems.
Temporal logics have also been studied in connection with the
automaton-theoretic approach to concurrent system based on verification
by model checking. History Dependent (HD) automata, which are able to
allocate and deallocate names dynamically, have been introduced and
proved effective for the verification of (finite fragments of) calculi
with causality, locality and mobility [FGMP04].
[CMS05] proposes a spatial logic built on bigraphs. As it is equipped
with a contextual operator, the logic can characterise both closed
systems (processes) and open systems (contexts). It can describe also
the composition of contexts and the separation of resources. Thanks to
the generality of bigraphs, such a logic aims at embedding and
contextualising the spatial logics proposed up to now.
Testo italiano
WP1 - Sistemi di Tipi.
La nostra ricerca si svilupperà lungo due direzioni complementari. Da
un lato, svilupperemo sistemi di tipo in grado di assicurare che siano
rispettati i vincoli sulle autorizzazioni, le restrizioni globali
sull'accesso alle risorse e i limiti all'uso delle risorse stesse
imposti dagli ambienti di computazione agli agenti mobili che li
visitano. Dall'altro lato, studieremo nuove tecniche che permettano di
esprimere politiche decentralizzate e discrezionali per la gestione
delle "capability" e della loro propagazione nel sistema.
Caratteristica distintiva di entrambe le attività sarà la necessità di
affrontare problematiche legate all'assenza di conoscenza, controllo e
"trust" definiti centralmente, caratteristica propria dei sistemi di
interesse per questa proposta di ricerca.
*Controllo della mobilità e gestione delle risorse.
Proporremo varie estensioni dei sistemi di tipo attuali per il
controllo dell'accesso alle risorse e della mobilità del codice, al
fine di fornire meccanismi per monitorare e vincolare la mobilità dei
processi all'interno di aree prestabilite, così da evitare spostamenti
verso nodi giudicati inaffidabili. Tali sistemi dovranno consentire di
modificare dinamicamente i diritti di accesso e i privilegi del codice
mobile sulla base del comportamento del codice stesso, del sito da cui
proviene e del livello di trust delle locazioni che il codice ha
attraversato durante la sua esecuzione. Il nostro obiettivo è quindi un
sistema che permetta di caratterizzare il comportamento del codice
mobile per mezzo di tipi ed effetti che descrivono le capability
tramite le quali il codice può operare sulle risorse. Ci concentreremo
su tecniche di analisi basate su di una descrizione del comportamento
dei processi che assegna capability e risorse ad opportune classi di
sicurezza, e quindi estenderemo il nostro lavoro sviluppando sistemi
basati su tipi dinamici e dipendenti.
Svilupperemo inoltre sistemi di tipo in grado di limitare l'utilizzo
delle risorse. La ricerca in questo ambito, per quanto riguarda i
sistemi concorrenti e distribuiti, ha una storia recente
[TZH02,BBDS03]. Il nostro obiettivo qui è l'estensione delle idee e
delle tecniche presentate in [HJ03,CW00,CEI+05] ai sistemi concorrenti
e distribuiti. Questa linea di studio è fortemente innovativa, ed il
problema interessante per due motivi complementari. Da un lato, le
tecniche disponibili in letteratura non si estendono naturalmente al
caso di linguaggi e sistemi concorrenti per l'inerente non-determinismo
delle richieste di allocazione di memoria in questi sistemi. Dall'altro
lato, le algebre di processi correnti non forniscono meccanismi per la
rappresentazione esplicita di computazioni con risorse limitate, in cui
siano osservabili, e quantificabili, i limiti e ed i vincoli sulla
capacità dei processi di allocare, utilizzare, deallocare e recuperare
mediante "garbage collection" nuove risorse (come ad esempio canali e
locazioni).
Per trattare sistemi nei quali non si possa assumere la disponibilità
di conoscenza, controllo e trust centralizzati, si svilupperanno nuovi
meccanismi e protocolli per determinare le credenziali del codice
mobile e per definire la negoziazione di autorizzazioni. È naturale che
questa attività di negoziazione avvenga in corrispondenza dei
"contorni" (boundary): i contorni sono quindi entità speciali, per cui
ne proporremo ed analizzeremo differenti formalizzazioni. Possiamo
prefigurare due soluzioni possibili.
Da un lato, saranno sviluppate tecniche che integrano il typing locale,
statico del codice mobile, con un'attività di type checking dinamica,
just in time, svolta in corrispondenza dei contorni al fine di
certificare il codice in arrivo. Dato che le informazioni di tipo
relative al codice in questione possono essere parziali, inesatte o
addirittura mancanti, particolare attenzione verrà rivolta allo
sviluppo di sistemi di inferenza e di ricostruzione dei tipi. Sarà
centrale, in questa attività , lo sviluppo di teorie di tipi che
ammettano tipi principali, al fine di guidare l'inferenza e la
ricostruzione dei tipi e di permettere l'analisi composizionale dei
tipi.
Un approccio alternativo che intendiamo studiare si fonda sulla
certificazione del codice in arrivo sulla base di "guardiani" associati
a nodi ed entità computazionali, o membrane. Queste entità sono in
grado di gestire eventuali tentativi di effettuare azioni non
consentite e di trasferire processi al loro interno. Le due soluzioni
verranno messe a confronto sulla base dei meriti e del potere
espressivo.
* Controllo decentralizzato dell'information-flow e delle capability.
Questa linea di ricerca è complementare all'attività sul controllo
dell'accesso alle risorse e la integra con lo sviluppo di tecniche che
permettono di imporre limitazioni sulla propagazione delle capability
tra i componenti di un sistema. Pi๠precisamente, intendiamo
sviluppare sistemi di tipi che permettono la gestione dinamica e
decentralizzata dei diritti di accesso, e la propagazione selettiva
delle capability basata sulla "clearance" e sul livello di trust dei
destinatari.
Traendo ispirazione da [CDV03,HR02,Mye99] e dal nostro stesso lavoro
presentato in [BCC04] ci proponiamo di sviluppare teorie di tipo che
controllino staticamente il flusso dinamico delle risorse e delle
"capabilities" attraverso le componenti del sistema. Questo lavoro sarà
basato su politiche discrezionali di controllo degli accessi (DAC), che
permettano ai proprietari delle risorse di assegnare a loro discrezione
diritti di autorizzazione diversi a utenti diversi. In particolare,
intendiamo sviluppare la tecnica introdotta in [BCC04] in due
direzioni. Da un lato extendendola a sistemi e calcoli con una nozione
esplicita di locazione e di distribuzione, come per esempio il Dpi
calcolo; dall'altro lato sviluppando sistemi con tipi dinamici e
dipendenti per ottenere politiche più flessibili basate su
distribuzione di specifici servizi a specifici utenti.
Un altro aspetto che intendiamo studiare riguarda l'implementazione
delle politiche di gestione delle risorse di interesse in calcoli di
processi di basso livello, dotati di primitive per la crittografia.
Pi๠precisamente, proponiamo di implementare la distribuzione
controllata dei diritti di accesso tramite una distribuzione
corrispondente di "term-level capability", protette mediante cifratura
con chiavi segrete note soltanto agli utenti specifici che possono
riceverle (oppure con le chiavi pubbliche di quegli utenti). Per
verificare l'adeguatezza di questa tecnica di implementazione,
svilupperemo tecniche sistematiche per confrontare le equivalenze (non
tipate) del calcolo crittografico di basso livello con le equivalenze
tipate del calcolo sorgente di alto livello.
Un'attività connessa riguarda lo studio di tecniche di tipo per
esprimere politiche di information-flow basate sulla declassificazione.
Le politiche di sicurezza che intendiamo rappresentare dovrebbero
permettere di specificare il cambiamento dinamico dei livelli a cui
sono assegnate le risorse, nonchè di associare tali cambiamenti a
condizioni dinamiche. L'impatto di tali politiche sarà valutato in
termini di nozioni raffinate di non-interference, formalizzate tramite
corrispondenti nozioni di equivalenza osservazionale.
WP2 - Equivalenze comportamentali
Le equivalenze comportamentali, basate su tecniche di testing e
bisimulazione, sono state largamente sviluppate nel contesto dei
calcoli di processi classici del prim'ordine ed estese, in alcuni casi,
a calcoli puri sviluppati per modellare la mobilità di nomi come ad
esempio il pi-calcolo. Negli ultimi anni sono stati fatti diversi
progressi che hanno portato a consolidare le tecniche operazionali
basate su metodi coinduttivi e "up-to", o basati su tracce. Lo scopo di
questo workpackage è di sviluppare tecniche simili per sistemi i cui
componenti sono mobili, distribuiti, aperti, (parzialmente) tipati e
non necessariamente affidabili. La nostra attività si svilupperà
seguendo diverse linee di ricerca interdipendenti che sono presentate
in dettaglio nel seguito.
Equivalenze con tipi e distribuzione. Nella teoria dei processi,
due processi vengono considerati equivalenti se non possono essere
distinti da nessun contesto nel linguaggio dato. Mentre questa nozione
di equivalenza puಠavere un'elegante lettura
dichiarativa/estensionale, la quantificazione su tutti i possibili
contesti osservati la rende difficile da usare nelle dimostrazioni; di
conseguenza vengono utilizzate versioni rafforzate basate
sull'osservazione delle azioni che un processo puಠeffettuare [SW01].
In presenza di tipi, distribuzione e caratteristiche di ordine
superiore, la nozione ordinaria di osservazione di azioni ਠmolto pià¹
forte, ed il significato dell'affermazione "due processi eseguono le
stesse azioni" è poco chiaro. Per esempio non è chiaro quale delle
azioni eseguite dai processi debbano essere considerate rilevanti, o
uguali, dato che la distribuzione e i tipi possono implicare
l'equivalenza di azioni molto diverse tra loro dal punto di vista
strettamente sintattico. Esistono alcuni risultati preliminari ma sono
applicabili solamente a pochi calcoli specifici. L'idea invece sarebbe
quella di costruire un framework generale che si possa applicare a
diversi sistemi di tipi e calcoli di processi, e che permetta di
dedurre come casi speciali i risultati ottenuti fino ad ora. Si farà un
uso esteso dei sistemi di transizione etichettati, ma sarà necessaria
una notevole innovazione per utilizzare queste tecniche descrittive nei
sistemi in questione. L'utilizzo di queste tecniche nello sviluppo di
equivalenze comportamentali basate sulla bisimulazione richiederà
inoltre l'estensione delle metodologie esistenti con nuovi sviluppi ed
idee. Questo non riguarda solamente la definizione delle equivalenze
stesse e le prove delle loro proprietà di congruenza, ma anche lo
sviluppo di migliori tecniche coinduttive come ad esempio la
bisimulazione-up-to, che nel pi-calcolo si è dimostrata essenziale per
portare a termine molte dimostrazioni.
Tecniche per la verifica automatica, la minimizzazione ed la dimostrazione di equivalenze.
Questa linea di ricerca riguarda lo studio di tecniche di tipo diverso
che permettano lo sviluppo di strumenti formali per meccanizzare la (o
aiutare nella) costruzione di dimostrazioni, nonchè di tecniche per
migliorare l'efficienza di questi strumenti. I tipi possono risultare
molto utili in questo contesto, dato che consentono di ridurre lo
spazio degli stati sul quale si lavora per costruire la dimostrazione:
per esempio alcuni tipi garantiscono che le comunicazioni non sono
"preemptive", una proprietà di confluenza parziale che permette di
analizzare solo un sottoinsieme dei possibili comportamenti dei
processi. Verranno anche utilizzate tecniche simboliche [HeLi95] per
migliorare lo sviluppo di prove di equivalenza basate sull'abilità di
fornire rappresentazioni finitarie del grafo di esecuzione.
Un'ulteriore linea di ricerca riguarderà lo studio di asiomatizzazioni
per calcoli tipati e/o distribuiti. Per alcune varianti di calcoli di
processi sono state definite opportune assiomatizzazioni. Queste
forniscono insiemi completi di leggi algebriche che caratterizzano
diverse nozioni di equivalenza comportamentale. Sarebbe interessante
estendere queste nozioni in modo da tener conto di aspetti di
tipizzazione e di distribuzione spaziale dei processi. Diverse
problematiche cruciali per realizzare questa estensione sono tuttora
aperte. Una difficoltà è legata alla legge di espansione (che permette
di esprimere la composizione di processi paralleli come la somma delle
loro azioni individuali). Questa legge, in genere, non vale, o vale
solo in un contesto limitato, in presenza di tipi e distribuzione.
Un'ulteriore problematica riguarda il fatto che la rappresentazione
della migrazione di processi attraverso diverse locazioni è un aspetto
inerentemente di ordine superiore (sia se che si utilizzino costrutti
espliciti per la migrazione, sia che questa sia rappresentata con
primitive di comunicazione).
*Equivalenze comportamentali e proprietà di sicurezza. Il
nostro obiettivo su questo tema è quello di sviluppare tecniche
accurate ed efficienti che consentano di specificare e garantire il
rispetto di politiche di sicurezza che controllano il flusso delle
informazioni permettendo però il rilascio di informazioni
private/segrete (declassification) ove necessario. Ciò naturalmente
richiede lo sviluppo di formalismi adatti ad esprimere tali politiche
in modo tale da poter essere automaticamente verificate. Il punto di
partenza per il nostro lavoro sarà la nuova caratterizzazione della
non-interferenza in questi calcoli che abbiamo recentemente proposto in
[CR05]. Le politiche di sicurezza che intendiamo modellare dovrebbero
rendere possibile la variazione dinamica dei livelli di sicurezza
assegnati alle risorse e/o agli utenti, in funzione di diverse
condizioni sullo stato delle risorse e della computazione.
*Logical Relations. Le logical relations sono tecniche
potenti, largamente utilizzate nel settore della semantica
denotazionale dei linguaggi di programmazione ad alto livello per
dimostrare proprietà comportamentali come la terminazione (ad esempio,
per verificare che la computazione per un certo termine avrà fine), e
la parametricità (ad esempio, per dimostrare che due termini che
possono manipolare diversi tipi di valori non sono distinguibili).
Infatti, nei linguaggi ad alto livello tipati e di ordine superiore le
relazioni logiche sono a volte l'unico strumento disponibile per
dimostrare proprietà osservazionali (alcuni esempi si possono trovare
in [Pit98]). Riteniamo che le relazioni logiche possano essere
utilizzate con successo anche nel settore dei linguaggi tipati per
processi. Un lavoro preliminare al fine di utilizzare le relazioni
logiche nel contesto dei processi è stato presentato in [San02], ma il
linguaggio risultante ha ancora una caratterizzazione funzionale; un
ulteriore approfondimento è necessario per modellare tipologie di
processi pi๠generali.
Costruzione di modelli a filtro. Un'ulteriore linea di ricerca
nel contesto di questo workpackage ha l'obiettivo di studiare l'impatto
delle tecniche per costruire modelli a filtro sull'individuazione di
nozioni interessanti di equivalenza comportamentale. Alcuni esperimenti
in questa direzione sono già stati fatti e sono disponibili nella
letteratura sui sistemi distribuiti con processi mobili
[DDG99,CD02,MZ04]. Il nostro obiettivo è quello di indagare la
possibilità di definire modelli a filtro per calcoli con tipi dinamici,
e di confrontare le equivalenze così indotte con quelle definite
utilizzando tecniche standard, come quelle operazionali basate su
bisimulazione e tracce.
WP3 - Logiche di Specifica.
Le logiche modali stanno
giocando un ruolo sempre più centrale nella formalizzazione e nella
verifica di proprietà dinamiche di sistemi mobili e distribuiti.
L'allocazione e l'accesso alle risorse, la diffusione
dell'informazione, e le diverse proprietà topologiche sono specificate
per mezzo di operatori modali spaziali e temporali e quindi verificate
con sistemi di prova e/o con il supporto di model checker. Più in
dettaglio, le attività del workpackage procederanno secondo due
direzioni.
*Logiche modali per proprietà spaziali e temporali di sistemi aperti.
Questo tema di ricerca si focalizzerà sull'uso delle logiche per
ragionare sul comportamento dei processi in sistemi aperti, e per
controllare le loro interazioni. Questa linea di lavoro ha due
obiettivi complementari che condividono motivazioni e tecniche. Da un
lato, miriamo a sviluppare logiche per la specifica e verifica di
proprietà comportamentali di processi operanti in ambienti parzialmente
sconosciuti/parzialmente specificati. Il framework che noi prefiguriamo
dovrebbe consentire una presentazione operazionale di sistemi
parzialmente specificati composti da componenti concrete (i.e.
completamente specificate), e contesti astratti che rappresentano
l'ambiente che racchiude tali componenti. L'uso di equivalenze
comportamentali (o preordini) per definire nozioni di accordo tra
contesti astratti e componenti concrete, dovrebbe portare ad un
framework logico che consenta il raffinamento dei sistemi per passi
successivi. Il sistema logico sottostante dovrà fornire un meccanismo
uniforme per specificare le proprietà comportamentali delle componenti
concrete e dei contesti astratti, e tecniche effettive per verificare
il preservarsi delle proprietà comportamentali di interesse durante la
procedura di raffinamento. Al fine di garantire il mantenimento delle
specifiche logiche del sistema durante il raffinamento del contesto, si
dovrà dimostrare che l'equivalenza comportamentale che definisce la
nozione di accordo è adeguata (e fully-abstract) rispetto
all'equivalenza indotta dalla logica. Una linea parallela di lavoro
mirerà a sviluppare strumenti per l'analisi comportamentale di sistemi
aperti basati su sistemi di transizione simbolici. L'obiettivo qui è
quello di analizzare il comportamento dei sistemi aperti, ossia
contesti con buchi, senza che questi vengano istanziati esplicitamente,
ma piuttosto stabilendo le proprietà che i processi da inserire nei
buchi dovranno soddisfare. I requisiti che un componente dovrebbe
soddisfare (ossia, le azioni che questo è in grado di eseguire o le
risorse di cui avrà bisogno) per potersi inserire nel contesto saranno
espressi tramite formule logiche; questo influenzerà la nozione di
equivalenza comportamentale. Come parte di questa ricerca, studieremo
anche logiche capaci di esprimere nozioni di freshness, una proprietà
centrale per la specifica di sistemi in grado di generare risorse nuove
o segrete.
*Espressività e decidibilità delle logiche spaziali.
Questa linea di ricerca coinvolge questioni più fondazionali
riguardanti l'espressività e la decidibilità di alcune delle logiche
spaziali attualmente studiate in letteratura. Una caratteristica
peculiare di queste logiche è la loro intensionalità , che rende la
nozione di equivalenza associata alla logica più fine dell'equivalenza
indotta dalla semantica operazionale standard. Questo è in singolare
contrasto con ciò che accade nelle logiche modali classiche, la cui
caratterizzazione risulta correlare le equivalenze logiche e
comportamentali (tipicamente espresse come bisimulazioni) esistenti.
L'obiettivo della nostra ricerca è di indagare sulle conseguenze di
questa intensionalità sul problema della decidibilità delle logiche.
Puntiamo a definire logiche spaziali che siano in accordo con la
semantica operazionale, esattamente come accade per le logiche modali
classiche e la bisimilarità . A complemento del nostro lavoro
sull'espressività , intendiamo inoltre studiare logiche che si prestino
ad esprimere proprietà spaziali e comportamentali di modelli grafici e
di sistemi di riscrittura di grafi. Queste tecniche saranno poi
applicate per ragionare sui calcoli per sistemi distribuiti con
mobilità , e specificatamente per esprimere proprietà topologiche
quali: "due dati processi saranno sempre connessi mediante un canale",
o "un agente che richiede un servizio sarà prima o poi connesso ad
esso".
Casi di studio
Il progresso delle attività su modelli e tecniche portato avanti nei
WP1-3 verrà valutato su casi di studio rappresentativi dei sistemi di
riferimento per il progetto. Se da un lato rappresenta un obiettivo
specifico di questa attivita l'identificare esempi interessanti per
valutare le tecniche sviluppate nel progetto, dall'altro lato abbiamo
già piani definiti in tal senso
Un primo scenario che studieremo riguarda l'analisi dei protocolli che
regolano la comunicazione ed il "routing" in reti wireless "ad hoc". In
una rete ad-hoc, non c'è un'infrastruttura fissa come nel caso delle
stazioni base e dei centri di "switch" mobile nelle reti di telefonia
mobile: i dispositivi mobili (o nodi) cooperano tra di loro per
inoltrare i pacchetti lungo la rete. I nodi che sono fisicamente
vicini, ovvero sono posizionati entro il raggio di copertura, possono
comunicare, mentre quelli che sono distanti devono contare su altri
nodi perché fungano da tramite e inoltrino i pacchetti comportandosi
come router. L'itinerario seguito dal pacchetto dal mittente al
ricevente puಠrichiedere il passaggio attraverso nodi intermedi, ai
quali è richiesto di ritrasmettere il pacchetto in questione generando
un percorso "multi-hop".
Queste caratteristiche salienti delle reti ad-hoc rendono inadeguati i
protocolli tradizionali usati nelle reti fisse. Infatti, la maggior
parte dei protocolli di routing per le reti ad-hoc è di natura
cooperativa e presuppone un implicito rapporto di fiducia tra nodi
vicini quando si tratta di instradare uno o pi๠pacchetti. Questo
modello ingenuo di fiducia reciproca permette ai nodi "cattivi" di
paralizzare una rete ad-hoc inserendo aggiornamenti sbagliati sui
percorsi di routing, oppure riutilizzando le informazioni di un vecchio
percorso di routing, modificando gli aggiornamenti del percorso, o
rendendo pubbliche informazioni di percorso errate. Per esempio, due
protocolli che sono allo studio dallo IETF per diventare uno standard,
il protocollo Dynamic Source Routing (DSR) [J02], il protocollo Ad-hoc
On-demand Distance Vector routing protocol (AODV) [PRD02], e le loro
varianti "sicure", quali Ariadne [HPJ02] e ARAN (Authenticated Routing
for Ad hoc Networks) [S05], permettono agli attaccanti di rendere
pubbliche informazioni errate sul percorso di routing, di dirottare i
pacchetti spediti dai nodi intermedi, e di lanciare gli attacchi di
denial-of-service. Ad oggi, le valutazioni di correttezza per tali
protocolli sono essenzialmente basate su simulazione. Risulta peraltro
del tutto evidente l'importanza di possedere modelli formali per tali
protocolli da poter utilizzare in verifiche semi-automatiche.
Il secondo scenario che utilizzeremo come base per le nostre
valutazioni riguarda la pratica sempre più frequente da parte gli
utenti di scaricare codice dalla rete per eseguirlo sui propri
dispositivi, portatili, palmari, ecc. Il codice così scaricato può
essere di natura molto varia e si presta facilmente ad essere
utilizzato da virus e "worms" come veicolo per introdursi nel sistema
allo scopo di manipolare dati, violare la privaci o tentare attacchi di
"denial of service" mediante un sovra utilizzo delle risorse di
sistema, problema quest'ultimo particolarmente rilevante per
dispositivi di dimensioni e capacità computazionali limitate. Se da un
lato la ricerca nel campo delle tecniche di analisi per codice movile
ha contribuito a sviluppare strumenti potenti per prevenire attacchi
all'integrità dei dati (un tipico esempio sono le tecniche di verifica
del bytecode), dall'altro lo studio di metodi per imporre limiti
sull'uso di risorse è ancora in fase iniziale.
Giustificazione della richiesta di finanziamento Il
finanziamento richiesto dal consorzio verrà utilizzato per assumere due
assegnisti di ricerca, uno per 12 mesi a metà tempo per tutta la durata
del progetto, e l'altro per 15 mesi a tempo pieno con inizio al mese 9.
La parte rimanente del finanziamento verrà utilizzata per spese
addizionali sostenute dai contraenti principali per hardware (desktop e
laptop), diffusione dei risultati (tasse di iscrizione a conferenze,
spese di viaggio e di sussistenza), visite reciproche tra membri del
progetto e collaborazioni sui temi del progetto con personale esterno.
Struttura del consorzio Il progetto sarà intrapreso da un
consorzio di quattro unità di ricerca, un consorzio volontariamente
piccolo, sia nel numero dei contraenti che nella grandezza dei team,in
modo da semplificare la gestione del progetto su un piccolo insieme di
obiettivi comuni ben definiti, e mantenere il progetto centrato sui
suoi scopi.
Risultati Attesi
Anticipiamo i seguenti contributi dei diversi workpackage. Dove non
altrimenti specificato, i contributi si baseranno su articoli tecnici
pubblicati o sottoposti a revisione per la pubblicazione in riviste e/o
atti di conferenze internazionali, e daranno conto dei principali
risultati raggiunti nei corrispondenti argomenti di ricerca.
. Certificati "type-based" per il controllo della mobilità ed il confinamento di agenti.
. Osservabili "resource-centric" per equivalenze comportamentali in sistemi distribuiti con mobilità.
. Inferenza e ricorstruzione di tipi per codice mobile.
. Analisi di politiche per la gestione di risorse.
. Teorie algebriche e assiomatizzazione in presenza di mobilità.
. Specifica e raffinamento di sistemi aperti basati su logiche modali.
. Controllo degli accessi mediante tipi in sistemi aperti.
. Tecniche coinduttive per la bisimulazione in calcoli concorrenti distribuiti.
. Ottimizzazione guidata dai tipi per algoritmi e strumenti di verifica.
Inoltre, ai mesi 12 e 24 produrremo dei rapporti tecnici che descrivono
in dettaglio lo stato di avanzamento dei lavori sui casi di studio. In
particolare, produrremo i seguenti documenti:
. Mobilità e comunicazione in reti ad-hoc: specifiche formali e tecniche di verifica.
. Protezione di risorse e di dati mediante certificazione di codice mobile.
Coordinamento e auto-valutazione
Il progetto sarà gestito in modo semplice ma efficace per assicurare
l'avanzamento lungo le linee di lavoro proposte. Il coordinamento sarà
assicurato dal Project Coordination Board (PCB), composto dal Project
Coordinator (PC) e dai tre Workpackage Leaders (WPL). I responsabili
scientifici delle unità del progetto svolgeranno il ruolo di WPL, come
anticipato precedentemente: ciascun WPL è responsabile del
coordinamento del lavoro tecnico di un workpackage, e assicura che gli
obiettivi del workpackage siano raggiunti in modo da permettere la
stesura dei deliverable finali. Ci saranno degli incontri regolari,
almeno due volte all'anno, dei membri del PCB, in modo da assicurare un
monitoraggio constante dell'avanzamento del progetto. Il PCB inviterà
esperti di chiara fama, esterni al progetto, ad agire da project
advisor, nel ruolo di revisori della qualità scientifica e della
rilevanza dei risultati prodotti.
La valutazione avverrà in coincidenza con i naturali punti cardine
del progetto ai mesi 8, 16 e 24. I meeting di progetto, tramite
presentazioni dei risultati ai membri e agli advisor del progetto,
costituiranno i momenti di valutazione. Nell'organizzazione di questi
meeting cercheremo di massimizzare la coordinazione con progetti
analoghi, in modo da aumentare la diffusione dei risultati e lo scambio
di idee.
WP1 - Typing Systems
Our research will proceed along two complementary directions. On one
side, we will design type systems to enforce the authorization
constraints and the system-wide resource access restrictions and usage
bounds placed by computational environments on the code they host. On
the other side, we will investigate new techniques to express
decentralized, discretionary policies to control the administration of
capabilities and their propagation among the components of the system.
Distinctive of both activities will be the need to accommodate
techniques to address the lack of centralized knowledge, control and
trust characteristic of the systems of interest in this proposal. Our
activities will be organized along the topics we discuss next.
* Mobility control and resource management. We will
investigate extensions of current type systems for resource access and
code mobility control to provide mechanisms for monitoring and
restricting process mobility within confined areas, so as to prevent
migrations on malicious nodes. Such systems should provide ways to
dynamically tune the access rights and privileges of migrating code on
the basis of the code's behavior, its originating site, the (trust
level of) the locations traversed during its execution. The systems we
target should make it possible to characterize the behavior of mobile
code by means of types and effects describing the capabilities
available for the code to operate on resources. We shall focus on
analyses in which process behavior is described by putting capabilities
and resources in security classes, and then refine our work by
developing systems with dynamic and dependent types.
We will also devise systems to enforce bounds on the use of
resources. Work on resource bounds has initiated only recently in the
literature on concurrent and distributed systems [TZH02,BBDS03]. Our
plan is to investigate how to extend the ideas and techniques of
[HJ03,CW00,CEI+05] to concurrent settings. This is a rather innovative,
and challenging task for at least two reasons. On the one side, the
existing techniques do not scale naturally to concurrent languages and
systems due to the inherent nondeterminsm of resource allocation in
this setting. On the other side, current process calculi lack explicit
representation for resource boundedness and its import on the ability
of processes to allocate new resources (channels, locations), use,
deallocate and garbage collect them. Similarly, virtually no literature
is available on typing techniques to specify and enforce the associated
QoS requirements for communication channels or availability of
resources.
To cope with systems in which no centralized knowledge, control,
and trust may be assumed, we will devise novel mechanisms and protocols
to establish the credentials of migrating code and to define the
negotiation of authorization rights. A natural place for such
negotiation activity to take place is at location boundaries:
boundaries are therefore very special entities, for which we will
explore different formalizations. We envision two solutions for that.
On one side, we will develop techniques that complement local, static typing of migrating code, with dynamic, just in time
type checking to be performed at location boundaries to certify the
visiting code. Since the type information of such code could be
partial, inaccurate or missing, specific emphasis will be given to the
development of type inference and reconstructing systems. Central to
this activity will be the study of type theories which admit principal
types, or typings, to guide type inference and reconstruction, and to
support compositional type analyses.
As an alternative approach, we will investigate solutions for
certifying incoming code based on equipping nodes and computing
entities with guardians, or membranes, that should be able to react to,
or to manage, attempts to perform forbidden actions and to spawn
processes over to them. We shall contrast the relative merits and
expressive power of the two solutions.
* Decentralized information-flow and capability control.
This line of work complements the activity on resource access control
by devising techniques to place restrictions on the propagation of
capabilities across system locations and components. Specifically, we
target the development of type systems that provide for decentralized
and dynamic administration of access rights, and the selective
propagation of capabilities based on the clearance and trust level of
the intended recipients. Drawing inspiration from existing work
[CDV03,HR02,Mye99], we plan to develop type theories to control the
dynamic flow of resources and capabilities among system components, and
study their extensions required to express policies for down/upgrading
of the access rights.
The plan here is to extend the work in [BCC04] in two, largely
orthogonal directions: on one side, to port them to calculi with
explicit locations and distribution, such as the Dpi calculus; on the
other side, we will extend our current framework to capture more
flexible policies, personalized on specific users and services, by
relying on system with dynamic and dependent types.
We will also investigate the implementation of the resource
management policies of interest in low-level process calculi equipped
with cryptographic primitives. Specifically, the solution we envision
here is based on implementing the selective distribution of access
rights by a corresponding distribution of term-level capabilities
protected by encryption under secret keys only known to the intended
receiver users (or else under those users' public keys). To assess the
adequacy of this implementation schema, we will then develop systematic
techniques to contrast the untyped equivalences of the low-level
cryptographic calculi with the typed equivalences of the high-level,
and typed, source calculi.
A related activity targets the development of typing techniques
to express information-flow policies based on declassification. The
security policies we intend to model should support the specification
of dynamic changes of the levels to which resources may be assigned,
and predicate such changes to dynamic conditions. The import of such
policies will be assessed in terms of refined notions of
non-interference, formalized by means of corresponding observation
equivalences.
WP2 - Behavioral Equivalences
Behavioral equivalences, based on testing and bisimulation, are well understood for the case of classical,
first-order process calculi and, to some extent, also for pure calculi
for name mobility like the pi-calculus. Consolidated progress has been
made over the years on operational techniques based on co-inductive
methods and up-to techniques, or traces. This workpackage seeks to
develop similar techniques for systems whose components are mobile,
distributed, open, (partially) typed, possibly untrusted.
Our activities will develop along several inter-dependent directions, detailed below.
* Equivalences with types and distribution. In
process theory, two processes are equal if they cannot be distinguished
by any context expressed in the given process calculus. While this
notion of equivalence has an elegant declarative/extensional flavor,
the quantification over all possible observing contexts makes it rather
awkward to use in proofs: thus one employs stronger versions based on
the actions a process can perform [SW01]. However, in presence of
types, distribution, or higher-order features the ordinary notion of
action is much too strong, and the very meaning of "two processes
perform the same actions" is unclear. For instance, it is unclear which
actions of processes should be considered relevant, or equal, as
distribution and types may imply the equivalence of syntactically very
different actions. Some initial results on this problem exist, but they
only apply to few, specific, calculi. We target the development of a
general, uniform, framework in which several type systems and
foundational calculi can be accommodated, and in which the existing
results can be extracted as special cases.
We will make extensive use of labelled transition systems, but
considerable innovation will be required in order to use these
descriptive techniques on the systems of interest. The use of these
techniques in the elaboration of bisimulation-based behavioral
equivalences will also require novel developments of existing
methodologies. This includes not only the definition of the
equivalences themselves and the proofs of their congruence properties,
but also the development of enhanced co-inductive techniques such as
the so-called ``bisimulation-up-to'' techniques that in the pure
pi-calculus have been shown to be essential for carrying out proofs.
* Techniques for automatic verification, minimization and equivalence checking.
This line of work studies the use of different techniques to support
the development of formal tools for mechanizing (or assisting)
equivalence proofs, and of techniques to increase the efficiency of
such tools. Types may prove very effective in this context, as they may
help prune the proof search-space: for instance, certain types
guarantee that communications are not preemptive, a partial confluence
property, in the presence of which only parts of process behaviors need
to be explored. Symbolic techniques [HeLi95] will also be employed to
assist the development of equivalence proofs based on the ability to
provide finitary representations of the execution graphs.
A further line of work will explore axiomatizations of typed
and/or distributed calculi. Axiomatizations have been developed for a
variety of classical process calculi, giving complete sets of algebraic
laws characterizing various notions of behavioral equivalence. There
would be significant interest in extending these to take typing and
spatial distribution into account. Serious challenges arise here to
extend the results currently available in first-order process calculi.
One difficulty is related to the expansion law (by which parallel
process composition may be expressed as the sum of their individual
actions) which is usually not available, or only limitedly available,
with types or distribution. A further challenging problem is in the
inherently higher-order nature of the actions characterizing the
migration of processes across locations (via explicit movement, or
communication)
* Behavioral equivalences for information-flow security.
Our goal is to develop accurate and efficient techniques for specifying
and enforcing security policies that control information flow while
also allowing information release (i.e., declassification) where
appropriate. This in turn requires the development of adequate
formalisms for expressing such policies in a way that enables their
automatic verification. The starting point for this investigation will
be the characterization of non-interference in these calculi, which we
have proposed recently in [CR05]. The security policies we intend to
model should support the specification of dynamic changes of the levels
through which resources may be assigned, and to predicate such changes
to the verification of suitable conditions.
* Logical relations. Logical relations are a
powerful technique, widespread in the denotational semantics of
traditional sequential languages, for proving behavioral properties
such as termination (for instance, to ensure that the computation of a
term will terminate), and parametricity (for instance, to prove that
two terms that can manipulate different types of values are
indistinguishable). Indeed, in typed higher-order sequential languages
sometimes logical relations are at present the only viable techniques
to prove behavioral properties (some examples are for instance in
[Pit98]). We believe that logical relations could be equally useful in
languages of typed processes. Some initial work in transplanting
logical relations to processes is [San02], but the resulting language
is still rather functional; work is needed in order to capture more
general process patterns.
* Filter model constructions. A further line of work
in this workpackage studies the impact of filter model constructions in
capturing interesting notions of behavioral equivalences. Some
experiments in that direction have already been carried out in the
literature on mobile and distributed systems [DDG99,CD02,MZ04]. Our
goal here is to investigate the possibility of defining filter models
for calculi with dynamic types and to compare their induced
equivalences with the ones defined with more standard, operational
techniques based on bisimulations and traces.
WP3 - Specification Logics.
Modal logics are playing an increasingly central role in the
formalization and verification of dynamic properties of mobile and
distributed systems. Resources allocation and access, information
disclosure, and diverse topological properties are specified by means
of temporal and spatial modalities and then verified
proof-theoretically and/or with the aid of model checkers. Recent
progress has also being made on the development of logics equipped with
contextual operators to be employed for compositional specification of
open systems. Drawing on this body of work, the activities of this
workpackage will proceed along two directions.
* Modal logics for behavioral and spatial properties of open systems.
This research theme focuses on the use of logics to reason on the
behavior of processes in open systems, and to control their
interaction. This line of work has two complementary objectives which
share motivations and techniques.
On one side, we aim at developing logics to specify and verify
behavioral properties of processes operating in partially
unknown/unspecified environments. The framework we envision relies on
operational presentations of partially specified systems composed of
concrete (i.e. fully specified) components, and abstract contexts
representing the enclosing environments of such components. By relying
on behavioral equivalences (or preorders) to define notions of
agreement between abstract contexts and concrete components, we aim at
developing a logical framework for stepwise system refinement. The
underlying logical system should provide uniform mechanisms for
specifying the behavioral properties of the concrete components and of
the abstract contexts, and effective ways to verify the preservation of
the behavioral properties of interest along the refinement process. In
order to guarantee the preservation of logical specification of the
system through context refinement, the behavioral equivalences defining
the notion of agreement should be proved to be adequate (and fully
abstract) with respect to the equivalence induced by the logic.
A parallel line of work aims to develop behavioral analysis of
open systems based on symbolic transition systems. The goal here is to
analyze the behavior of open terms, i.e. contexts with holes, without
instantiating them explicitly, but rather by predicating on the
properties expected of the processes to be `plugged into' the holes.
Modal formulae will be employed to define requirements that a component
should meet (e.g., the actions it can perform or the resources it will
ask for) to be allowed to instantiate one of the context holes, thus
influencing the notion of behavioral equivalence. As part of this
research, we will also investigate logics capable of expressing notions
of freshness which is central for the specification of systems with
fresh or secret resources.
* Expressiveness and decidability of spatial logics.
This line of work involves more foundational questions of
expressiveness and decidability of some of the spatial logics currently
studied in the literature.
A distinctive feature of such logics is their intensionality, which
makes the associated notion of logical equivalence much finer than the
equivalences induced by standard operational semantics. This is in
striking contrast with the situation for classical modal logics, for
which characterization results relating logics and operational
equivalences (typically forms of bisimilarity) exist. The goal of our
research here is to investigate the consequences of this intensionality
on decidability problems for the logics. We aim at defining spatial
logics that agree with operational semantics, just like classical modal
logics do with bisimilarity. A direction of work we envision here is to
introduce a notion of "transparency" for the logical operators so as to
prevent the logic to directly observe the entire structure of the
model, and thus reflect the computational properties of contexts, which
can be `opaque' and do not allow the inspection of their contents.
As a complement to our work on expressiveness, we also plan to
investigate logics to express behavioral and spatial properties of
graphical models. Such techniques will later be applied to reason on
calculi for distributed systems with mobility, and specifically on
topological properties such as: "two given processes will be always
connected by a channel", "no untrusted agent will ever be co-located
with a secret resource" or "an agent asking for a service will be
eventually connected to it".
Case Studies
While it will be a specific objective of this workpackage to isolate
interesting examples and benchmarks for the techniques and methods
developed by the project, as we mentioned earlier in the proposal we
already have specific plans in that direction.
A first scenario we will address concerns the analysis of protocols to
regulate communication and routing in wireless ad-hoc networks. In such
networks there is no fixed infrastructure such as base stations or
mobile switching centers: mobile devices (or nodes) cooperate to
forward packets for each other. Nodes that are physically located
within their transmission range communicate directly via wireless
links, while those that are far apart rely on other nodes to relay
messages as routers. The network route from some sender node to a
destination node may require a number of intermediate nodes to forward
packets to create a "multi-hop" path from this sender to this
destination. The features of ad-hoc networks make traditional
fixed-network routing protocols inadequate. Indeed, most ad-hoc routing
protocols are cooperative by nature, and rely on implicit
trust-your-neighbor relationships to route packets among participating
nodes. This naive trust model allows malicious nodes to paralyze an
ad-hoc network by inserting erroneous routing updates, replaying old
routing information, changing routing updates, or advertising incorrect
routing information. For example, two protocols that are under
consideration by the IETF for standardization, Dynamic Source Routing
(DSR) [J02], Ad-hoc On-demand Distance Vector routing protocol (AODV)
[PRD02], and "secure" protocols based on them, such as Ariadne [HPJ02]
and Authenticated Routing for Ad hoc Networks (ARAN) [S05], allow
attackers to easily advertise falsified route information, to redirect
routes, and to mount other security attacks. While the correctness of
such protocols is still typically established by way of simulation, the
added-value of rigourous models for such protocols, to be then analyzed
and formally verified is self-evident.
The second scenario we envision addresses an increasingly common
practice by which users dowload code to run on their devices --laptops,
PDAs, etc. Downloaded code may include software updates, applications,
games, active web pages, and more. All these are potential home to
viruses worms and other malicious code that may corrupt data on the
host system, may violate privacy, or deny service to other applications
by overusing system resources. The latter problem is particularly
relevant for small devices with limited computational power. While the
research in analysis techniques for mobile code execution has developed
powerful tools for data corruption (such as bytecode verification) the
enforcement of resource bounds is considerably less developed, and
flexible techniques to address this problem are still largely
unavailable. Similarly, several techniques for bytecode verification
are developed for sequential code, and fail to address the effects of
nondeterminism and concurrency in the analysis.
Structure of the consortium
The project will be undertaken by a consortium of four research units,
a purposely small consortium -- both in the number of contractors and
in the size of the teams -- so as to ease project management on a small
set of clearly defined common goals, and keep the project very focused
on its objectives. We detail the role of each unit below, in the
dedicated section of the proposal, leaving a more detailed description
of the research by each unit on the specific themes of the project is
given in part B of the proposal.
Justification of funding
The consortium asks funding to employ two reserch fellows on the
project, one for 12 months, working part time on the project for its
full duration, the other for 15 months working full time and starting
at month 9. The remaining funding request is for additional costs
incurred by the contractors on additional admnistrative overheads,
hardware (PCs) for PhD students, dissemination (conference fees, travel
and subsistence), exchange visits, and research collaborations on the
themes of the project with external personnel.
Expected Results
We anticipate the following deliverables for the theory-centred
workpackages. When not otherwise specified, each deliverable will be
based on technical articles published, or submitted for publication, in
international journals and/or conference proceedings, and will provide
insight into the most significant achievements on the corresponding
subject of research.
. Type-based certificates for mobility control and confinement.
. Resource-centric observables for behavioral equivalences in distributed calculi with mobility.
. Type inference and reconstraction for mobile code.
. Analysis and enforcement of resource bounds policies.
. Algebraic theories and Axiomatizations in the presence of name and code mobility.
. Specification and refinement of open systems based on modal logics.
. Type-based access control and resource bounds in untrusted networks.
. Coinductive techniques for bisimulation in calculi with explicit distribution.
. Type-driven optimizations for verification algorithms and tools.
In addition, at months 12 and 24, we will deliver reports detailing the
progress of the work on the case studies. More precisely, we anticipate
the following deliverables:
. Mobility and communication in ad-hoc networks: formal specification and verification.
. Resource and data protection via mobile code inspection and certification.
Management and self-evaluation
The project will employ a simple but effective management practice.
Coordination will be ensured by the Project Coordination Board (PCB),
composed by the Project Coordinator (PC) and three Workpackage Leaders
(WPL). The principal investigators of the project contractors will act
as WPLs, as outlined earlier on: WPLs are responsible for coordinating
the technical work of a workpackage, and ensure that the workpackage's
objectives are achieved with timely production of deliverables. Regular
meetings of the PCB, at least twice a year, will ensure constant
monitoring of the project progress. The PCB will invite renowned
personalities, external to the project, to act as project advisors,
whose role is to review the scientific quality and relevance of the
project's production.
Evaluation will take place in rounds coincident with the natural
milestones of the project at months 12 and 24. Project meetings, with
presentation of results to project members and to the project advisors
will mark the evaluation rounds.
Testo italiano
Unità I BUGLIESI Michele |
Questa unità, spesso denominata Unità C nella proposta, contribuirà con la propria esperienza riconosciuta a livello internazionale su tecniche di verifica per protocolli crittografici, se su analisi di proprietà sicurezza e controllo degli accessi basate su sistemi di tipo e equivalenze comportamentali. Oltre ad essere attiva sui workpackages WP1-3, l'unità coordinerà il lavoro sui casi di studio. In questo modo assicurerà una effettiva azione di coordinamento del progetto attuata mediante il monitoraggio costante progresso delle attività e della qualità dei risultati prodotti. |
Unità II COPPO Mario |
Questa unità, spesso denominata Unità T nella proposta, ha competenze riconosciute a livello mondiale su teorie di tipi e, più di recente, su algebre di processi per sistemi distribuiti. L'unità contribuirà a tutte le attività del progetto ed in particolare, in forza della propria esperienza su tecniche di analisi basate su teorie dei tipi, si prenderà carico del coordinamento del relativo workpackage WP1. |
Unità III DE NICOLA Rocco |
Questa unità, denominata Unità L nella proposta, metterà a disposizione le proprie competenze riconosciute a livello internazionale su semantiche per algebre di processi, sul progetto di linguaggi di coordinamento in ambienti mobili, e linguaggi di specifica basati su logiche modali e temporali. Oltre a fornire contributi su tutte le tematiche del progetto, questa unità coordinerà le attività sul workpage WP3. |
Unità IV SANGIORGI Davide |
Questa unità, denominata Unità E nella proposta, ha esperienza e competenza riconosciute a livello internazionale su tecniche coinduttive per la caratterizzazione di equivalence comportamentali (tipate e non) e le relazioni di queste con logiche spaziali. Oltre ad essere attiva sui workpakages WP1-3 il contributo prevalente al progetto sarà sulle equivalenze comportamentali relative al workpackage WP2 del cui coordinamento l'unità si farà carico. |
Unit I BUGLIESI Michele |
This unit, referred to as Unit C in the proposal, will contribute its world-renowned competence in verification techniques for cryptographic protocols, and on security and resource access control analysis based on type systems and behavioral equivalences. In addition to being active on Workpackages 1-3, Unit C will lead the work on case studies, thus effectively coordinating the activities of the project as a whole, by ensuring constant monitoring on the project's progress and continuing feedback to the other workpackages. |
Unit II COPPO Mario |
This unit, referred to as Unit T in the proposal, has world-recognized competence on foundational type theories and, more recently, on ambient-based calculi for distributed systems. Unit T will contribute to all of the reseach themes of the project; furthremore, given its expertise on type-based analyses, it will take the lead on the activities in the workpackage WP1. |
Unit III DE NICOLA Rocco |
This unit, referred to as Unit L in the proposal, will contribute its world-recognized expertise on process semantics, on languages for coordination and mobility, and on specification languages based on modal and temporal logics. In addition to its contribtions to the other project activities, unit L will coordinate the work on WP3 thus taking the lead of the work on specification logics. |
Unit IV SANGIORGI Davide |
This unit, referred to as Unit E in the proposal, has world-known competence on (typed) coinductive techniques and their relationships with spatial logics. In addition to being active on Workpackages 1-3, this unit's most prominent contributions to the project will be on the behavioral equivalences addressed in WP2, of which unit E will take the leadership. |
Unità I | Unità II | Unità III | Unità IV | |
---|---|---|---|---|
Grandi Attrezzature | 0 | 0 | 0 | 0 |
Materiale inventariabile | 4.000 | 4.000 | 9.000 | 2.300 |
Materiale di consumo e funzionamento | 4.000 | 3.500 | 4.000 | 3.600 |
Spese per calcolo ed elaborazione dati | 0 | 0 | 1.000 | 0 |
Personale a contratto | 23.000 | 0 | 0 | 18.000 |
Servizi esterni | 0 | 1.500 | 3.000 | 0 |
Missioni | 12.000 | 14.000 | 10.000 | 9.100 |
Pubblicazioni | 0 | 0 | 1.000 | 0 |
Partecipazione / Organizzazione convegni | 4.000 | 4.000 | 3.000 | 7.000 |
Altro | 3.000 | 6.000 | 2.000 | 5.000 |
TOTALE | 50.000 | 33.000 | 33.000 | 45.000 |
Unità I | Unità II | Unità III | Unità IV | |
---|---|---|---|---|
RD+RA (fondi di Ateneo) | 15.000 | 10.000 | 10.000 | 13.500 |
Cofinanziamento di altre amministrazioni pubbliche, private o fondazioni | 0 | 0 | 0 | 0 |
Cofinanziamento richiesto al MIUR | 35.000 | 23.000 | 23.000 | 31.500 |
Costo totale del programma | 50.000 | 33.000 | 33.000 | 45.000 |
Euro | |
---|---|
Costo complessivo del Programma | 161.000 |
Risorse complessivamente disponibili all'atto della domanda (RD + RA) | 48.500 |
Cofinanziamento di altre amministrazioni pubbliche, private o fondazioni | 0 |
Cofinanziamento richiesto al MIUR | 112.500 |
(per la copia da depositare presso l'Ateneo e per l'assenso alla
diffusione via Internet delle informazioni riguardanti i programmi
finanziati e la loro elaborazione necessaria alle valutazioni; D. Lgs,
196 del 30.6.2003 sulla "Tutela dei dati personali")
Firma _____________________________________ | Data 15/04/2005 ore 18:24 |