firenze.bib
@COMMENT{{This file has been generated by bib2bib 1.65}}
@COMMENT{{Command line: /usr/bin/bib2bib -oc firenze -ob firenze.bib -c 'sites : ".*FI.*"' allbib.bib}}
@INPROCEEDINGS{Bettini.Bono.Denicola.Ferrari.alt.03,
AUTHOR = {L.Bettini and V.Bono and R.De Nicola and G.Ferrari
and D.Gorla and M.Loreti and E.Moggi and R.Pugliese
and E.Tuosto and B.Venneri},
TITLE = {The KLAIM Project: Theory and Practice},
BOOKTITLE = {Global Computing: Programming Environments,
Languages, Security and Analysis of Systems},
YEAR = 2003,
PUBLISHER = {Springer-Verlag},
NOTE = {to appear},
SERIES = {{Lecture Notes in Computer Science}},
NUMBER = 2874,
EDITOR = {C.~Priami},
PAGES = {},
ABSTRACT = {Klaim (Kernel Language for Agents Interaction and
Mobility) is an experimental language specifically
designed to program distributed systems consisting
of several mobile components that interact through
multiple distributed tuple spaces. Klaim primitives
allow programmers to distribute and retrieve data
and processes to and from the nodes of a
net. Moreover, localities are first-class citizens
that can be dynamically created and communicated
over the network. Components, both stationary and
mobile, can explicitly refer and control the spatial
structures of the network. This paper reports the
experiences in the design and development of
Klaim. Its main purpose is to outline the
theoretical foundations of the main features of
Klaim and its programming model. We also present a
modal logic that permits reasoning about behavioural
properties of systems and various type systems that
help in controlling agents movements and
actions. Extensions of the language in the direction
of object oriented programming are also discussed
together with the description of the implementation
efforts which have lead to the current prototypes. },
SITES = {FI,GE,PI,TO},
THEMES = {TH1,TH2,TH3,TH4,TH5}
}
@INCOLLECTION{Bettini.Bono.Likavec.2003,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {A Core Calculus of Higher-Order Mixins and Classes},
BOOKTITLE = {Types 2003 },
PUBLISHER = {Springer-Verlag },
YEAR = {2004 },
SERIES = {{Lecture Notes in Computer Science} },
PDF = {http://www.di.unito.it/~bono/papers/mixin-high.pdf},
ABSTRACT = {This work presents an object-oriented calculus based
on higher-order mixin construction via mixin
composition, where some software engineering
requirements are modeled in a formal setting
allowing to prove the absence of
message-not-understood run-time errors. Mixin
composition is shown to be a valuable language
feature enabling a cleaner object-oriented design
and development. In what we believe being quite a
general framework, we give directions for designing
a programming language equipped with higher-order
mixins, although our study is not based on any
already existing object-oriented language.},
NOTE = {To appear in Types 2003},
SITES = {PO,FI},
THEMES = {TH3}
}
@INPROCEEDINGS{Bettini.Bono.Likavec.2004,
AUTHOR = {L. Bettini and V. Bono and S. Likavec},
TITLE = {A Core Calculus of Mixin-Based Incomplete Objects},
YEAR = {2004},
BOOKTITLE = {Proceedings of FOOL 11},
PDF = {http://www.di.unito.it/~bono/papers/inc-obj.pdf},
ABSTRACT = {We design a calculus that combines class-based
features with object-based ones, with the aim of
fitting into a unifying setting the ``best of both
worlds''. In a mixin-based approach, mixins are seen
incomplete classes from which incomplete objects can
be instantiated. In turn, incomplete objects can be
completed in an object-based fashion. Our hybrid
calculus is shown to be useful in some real world
scenarios that we present as examples.},
NOTE = {To appear in the informal proceeedings of the
workshop},
SITES = {PO,FI},
THEMES = {TH3}
}
@INPROCEEDINGS{Bettini.Bono.Venneri.2002,
AUTHOR = {L.~Bettini and V.~Bono and B.~Venneri},
TITLE = {{Coordinating Mobile Object-Oriented Mobile Code}},
BOOKTITLE = {Proc.\ of Coordination Models and Languages},
YEAR = 2002,
EDITOR = {F.~Arbarb and C.~Talcott},
NUMBER = 2315,
SERIES = {{Lecture Notes in Computer Science}},
PUBLISHER = {Springer},
PAGES = {56--71},
URLPS = {http://music.dsi.unifi.it/papers/coord2002-mob-OO-code.ps.gz},
SITES = {FI,PO},
THEMES = {TH1},
ABSTRACT = {Standard class-based inheritance mechanisms, which
are often used to implement distributed systems, do
not seem to scale well to a distributed context with
mobility. In this paper, a mixin-based approach is
proposed for structuring mobile object-oriented code
and it is shown to fit in the dynamic and open
nature of a mobile code scenario. We introduce MoMi
(Mobile Mixins), a coordination language for mobile
processes that communicate and exchange
object-oriented code in a distributed context. MoMi
is equipped with a type system, based on
polymorphism by subtyping, in order to guarantee
safe code communications.}
}
@INPROCEEDINGS{Bettini.Bono.Venneri.2002a,
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
TITLE = {Subtyping Mobile Classes and Mixins},
BOOKTITLE = {Proc. of Int. Workshops on Foundations of
Object-Oriented Languages, FOOL 10},
YEAR = {2003},
ABSTRACT = {MoMi (Mobile Mixins) is a coordination language for
mobile processes that communicate and exchange object-oriented
code in a distributed context. MoMi's key idea is structuring mobile
object-oriented code by using mixin-based inheritance. Mobile code
is compiled and typed locally, and can successfully interact with
code present on foreign sites only if its type is
subtyping-compliant with what is expected by the receiving site.
In this paper, we study a subtyping relation for MoMi that includes
both subtyping-in-width and subtyping-in-depth, in order to achieve
a significantly more flexible, yet still simple, communication
pattern. Technical problems arising from this extension are solved
by a static annotation procedure.},
SITES = {FI,PO},
THEMES = {TH1},
URLPS = {http://www.dsi.unifi.it/~bettini/papers/momitype.ps.gz}
}
@INPROCEEDINGS{Bettini.Bono.Venneri.2004,
AUTHOR = {L. Bettini and V. Bono and B. Venneri},
TITLE = {O'{K}laim: a coordination language with mobile
mixins},
YEAR = {2004},
BOOKTITLE = {Proceedings of COORDINATION 2004},
SERIES = {Lecture Notes in Computer Science},
PDF = {http://www.di.unito.it/~bono/papers/oklaim.pdf},
ABSTRACT = {This paper presents O'Klaim{} (Object-Oriented
Klaim), a linguistic extension of the higher-order
calculus for mobile processes Klaim with
object-oriented features. Processes interact by an
asynchronous communication model: they can
distribute and retrieve resources, sometimes
structured as incomplete classes, i.e., mixins, to
and from distributed tuple spaces. This mechanism is
coordinated by providing a subtyping relation on
classes and mixins, which become polymorphic items
during communication. We propose a static typing
system for: (i) checking locally each process in its
own locality; (ii) decorating object-oriented code
that is sent to remote sites with its type. This
way, tuples can be dynamically retrieved only if
they match by subtyping with the expected type. If
this pattern matching succeeds, the so retrieved
code can be composed with local code, dynamically
and automatically, in a type-safe way. Thus a global
safety condition is guaranteed without requiring any
additional information on the local reconfiguration
of local and foreign code, and, in particular,
without any further type checking. Finally, we
present main issues concerning the implementation of
O'Klaim.},
NOTE = {To appear},
SITES = {PO,FI},
THEMES = {TH2}
}
@INPROCEEDINGS{Bettini.Capecchi.Venneri.2003,
AUTHOR = {L. Bettini and S. Capecchi and B. Venneri},
TITLE = {Extending Java to dynamic object behaviors},
BOOKTITLE = {Proc. of WOOD 2003},
YEAR = 2003,
VOLUME = 82,
SERIES = {ENTCS},
ABSTRACT = {Class inheritance and dynamic binding are the key features of object-oriented programming and they permit designing and developing complex systems. However, standard class inheritance is essentially static and cannot be directly employed for modeling dynamic object behaviors. In this paper we propose a linguistic extension of Java, called Dec-Java, that is partially inspired by the decorator design pattern. This extension permits easily separating the basic features of objects (that are likely not to change during the application) from their behaviors (that, instead, can be composed dynamically at run-time). Thus, Dec-Java enables a dynamic extension and specialization of object responsibilities.},
SITES = {FI},
THEMES = {TH3}
}
@INPROCEEDINGS{Bettini.DeNicola.2002,
AUTHOR = {L. Bettini and R. {De Nicola}},
EDITOR = {Nicolas Guelfi and
Egidio Astesiano and
Gianna Reggio},
BOOKTITLE = {Scientific Engineering for Distributed Java Applications, International
Workshop, FIDJI 2002, Luxembourg-Kirchberg, Luxembourg, November
28-29, 2002, Revised Papers},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 2604,
YEAR = 2003,
ISBN = {3-540-00679-6},
TITLE = {A Java Middleware for Guaranteeing Privacy of
Distributed Tuple Spaces},
NOTE = {to appear},
ABSTRACT = {The tuple space communication model, such as the one
used in Linda, provides great flexibility for
modeling concurrent, distributed and mobile
processes. In a distributed setting with mobile
agents, particular attention is needed for
protecting sites and information. We have designed
and developed a Java middleware, Klava, for
implementing distributed tuple spaces and operations
to support agent interaction and mobility. In this
paper, we extend the Klava middleware with
cryptographic primitives that enable encryption and
decryption of tuple fields. We describe the actual
implementation of the new primitives and provide a
few examples. The proposed extension is general
enough to be applied to similar Java frameworks
using multiple distributed tuples spaces possibly
dealing with mobility.},
SITES = {FI},
THEMES = {TH5},
URLPS = {http://music.dsi.unifi.it/papers/cryptoklava.ps.gz}
}
@INPROCEEDINGS{Bettini.DeNicola.Loreti.2002,
AUTHOR = {L.~Bettini and R.~{De Nicola} and M.~Loreti},
TITLE = {{Software Update via Mobile Agent Based
Programming}},
BOOKTITLE = {Proc. of ACM SAC 2002, Special Track on Agents,
Interactions, Mobility, and Systems},
PAGES = {32--36},
YEAR = 2002,
PUBLISHER = {ACM Press},
SITES = {FI},
THEMES = {TH1},
ABSTRACT = {We describe a system that permits maintaining the
software installed on several heterogeneous
computers distributed over a network by taking
advantage of the mobile agent paradigm. The
applications are installed and updated only on the
central server. When a new release of an application
is installed on the server, agents are scattered
along the network to update the application on the
clients. To build a prototype system we use X-Klaim,
a programming language specifically designed to
program distributed systems composed of several
components interacting through multiple tuple spaces
and mobile code.},
URLPS = {http://music.dsi.unifi.it/papers/SAC02-software-update.ps.gz}
}
@ARTICLE{Bettini.DeNicola.Loreti.2003,
AUTHOR = {Lorenzo Bettini and Rocco {De Nicola} and Michele
Loreti},
TITLE = {Formulae meet Programs over the Net: a Framework for
Reliable Network Aware Programming},
JOURNAL = {Annals of Software Engineering},
NOTE = {Accepted for publication},
YEAR = 2003,
ABSTRACT = {A general framework for network aware programming is
presented that consists of a language for
programming mobile applications, a logic for
specifying properties of the applications and an
automatic tool for verifying such properties. The
framework is based on XKlaim, \emph{eXtended Klaim},
an experimental programming language specifically
designed to program distributed systems composed of
several components interacting through multiple
tuple spaces and mobile code. The proposed logic is
a modal logic inspired by Hennessy-Milner logic and
is interpreted over the same labelled structures
used for the operational semantics of XKlaim. The
automatic verification tool is based on a complete
proof system that has been previously developed for
the logic.},
SITES = {FI},
THEMES = {TH1}
}
@ARTICLE{Bettini.DeNicola.Pugliese.2002,
AUTHOR = {L. Bettini and R. DeNicola and R. Pugliese},
TITLE = {{KLAVA}: a {Java} package for distributed and mobile
applications},
JOURNAL = {Soft\-ware Prac\-tice and Experience},
VOLUME = 32,
NUMBER = 14,
PAGES = {1365--1394},
YEAR = 2002,
CODEN = {SPEXBL},
ISSN = {0038-0644},
SITES = {FI},
THEMES = {TH5},
ABSTRACT = {Highly distributed networks have now become a common
infrastructure for a new kind of wide-area
distributed applications whose key design principle
is network awareness, namely the ability of dealing
with dynamic changes of the network
environment. Network-aware computing has called for
new programming languages that exploit the mobility
paradigm as a basic interaction mechanism. In this
paper we present the architecture of Klava, an
experimental Java package for distributed
applications and code mobility. We explain how Klava
implements code mobility by relying on Java and show
a few distributed applications that exploit mobile
code and are programmed in Klava. },
URLPS = {http://music.dsi.unifi.it/papers/DRAFT-klava.ps.gz}
}
@INPROCEEDINGS{Bettini.Denicola.Loreti01b,
AUTHOR = {L.~Bettini and R.~{De Nicola} and M.~Loreti},
TITLE = {{Formalizing Properties of Mobile Agent Systems}},
BOOKTITLE = {Proc.\ of Coordination Models and Languages},
YEAR = 2002,
EDITOR = {F.~Arbarb and C.~Talcott},
NUMBER = 2315,
SERIES = {{Lecture Notes in Computer Science}},
PUBLISHER = {Springer},
PAGES = {72--87},
SITES = {FI},
THEMES = {TH1},
ABSTRACT = {The wide-spreading of Internet has stimulated the
introduction of new programming paradigms and
languages that model interactions among hosts by
means of mobile agents, and that are centered around
the notions of location awareness. In this paper we
show how to use formal tools, specifically a modal
logic, for formalizing properties for mobile agent
systems. We concentrate on one of these new
languages, Klaim, and we use it to specify a system
that permits maintaining the software installed on
several heterogeneous computers distributed over a
network by taking advantage of the mobile agent
paradigm.},
URLPS = {http://music.dsi.unifi.it/papers/coord2002-agentprop.ps.gz}
}
@INPROCEEDINGS{Bettini.Loreti.Puglese.2002,
AUTHOR = {L.~Bettini and M.~Loreti and R.~Pugliese},
TITLE = {{An Infrastructure Language for Open Nets}},
BOOKTITLE = {Proc. of ACM SAC 2002, Special Track on Coordination
Models, Languages and Applications},
PAGES = {373--377},
YEAR = 2002,
PUBLISHER = {ACM},
SITES = {FI},
THEMES = {TH1},
ABSTRACT = {The structure of open nets, like the Internet, is
highly dynamic, as the topology of component
networks continuously evolves. In this context, node
connectivity is a key aspect and a language for
distributed network-aware mobile applications should
provide explicit mechanisms to handle it. In this
paper, we address the problem of expressing dynamic
changes of node connectivity at linguistic level
and, in particular, we focus on a slight extension
of the language Klaim, that is targeted to this
aim. The extension consists of the introduction of a
new category of processes that, in addition to the
standard process operations, can execute a few new
coordination operations for establishing new
connections, accepting connection requests and
removing connections. Our extension puts forward a
clean separation between the coordinator level and
the user level and, hence, it is modular enough to
be easily applicable also to other network-aware
languages. We will also show that our approach can
be used as a guide for actual distributed
(i.e. without a single centralized server)
implementations of mobile systems.},
URLPS = {http://music.dsi.unifi.it/papers/SAC02-open-nets.ps.gz}
}
@INPROCEEDINGS{Boreale.Buscemi.02,
AUTHOR = {Michele Boreale, Maria Grazia Buscemi},
TITLE = {Experimenting with STA, a Tool for Automatic
Analysis of Cryptographic Protocols},
BOOKTITLE = {Proc. of ACM Symposium on Applied Computing
(SAC'02)},
YEAR = 2002,
PUBLISHER = {ACM Press},
ABSTRACT = {We present STA ({\em Symbolic Trace Analyzer}), a
tool for the analysis of security protocols. STA
relies on symbolic techniques that avoid explicit
construction of the whole, possibly infinite,
state-space of protocols. This results in accurate
protocol modeling, increased efficiency and more
direct formalization, when compared to finite-state
techniques. We illustrate the use of STA by
analyzing two well-known protocols, asymmetric
Needham Schroeder and Kerberos. We discuss the
results of this analysis, and contrast them with
previous work based on finite-state model checking.},
THEMES = {TH4},
SITES = {FI}
}
@INPROCEEDINGS{Boreale.Buscemi.03,
AUTHOR = {M. Boreale, M.Buscemi },
TITLE = {Symbolic analysis of crypto-protocols based on
modular exponentiation},
BOOKTITLE = {Proc. of MFCS 2003 },
YEAR = {2003},
EDITOR = {B. Rovan, P. Vojt\'{a}s},
VOLUME = {2747},
SERIES = {Lecture Notes in Computer Science },
PUBLISHER = {Springer},
ABSTRACT = { Automatic methods developed so far for analysis of
security protocols only model a limited set of
cryptographic primitives (often, only encryption and
concatenation) and abstract from low-level features
of cryptographic algorithms. This paper is an
attempt towards closing this gap. We propose a
symbolic technique and a decision method for
analysis of protocols based on modular
exponentiation, such as Diffie-Hellman key
exchange. We introduce a protocol description
language along with its semantics. Then, we propose
a notion of symbolic execution and, based on it, a
verification method. We prove that the method is
sound and complete with respect to the language
semantics. },
SITES = {FI},
THEMES = {TH4}
}
@UNPUBLISHED{Boreale.Buscemi.Montanari03,
AUTHOR = {M. Boreale and M.Buscemi and U. Montanari},
TITLE = {D-Fusion, a distinctive Fusion calculus},
YEAR = {2003},
NOTE = {Submitted.},
ABSTRACT = { Fusion calculus is commonly regarded as a
generalisation of pi-calculus. Actually, we prove
that there is no uniform fully abstract embedding of
pi-calculus into Fusion. This fact motivates the
introduction of a new calculus, D-Fusion, with two
binders, $\lambda$ and $\nu$. We show that D-Fusion
is strictly more expressive than both pi-calculus
and Fusion. The expressiveness gap is further
clarified by the existence of a fully abstract
encoding of mixed guarded choice into the
choice-free fragment of D-Fusion. },
SITES = {FI},
THEMES = {TH4}
}
@ARTICLE{Boreale.DeNicola.Pugliese.2002,
AUTHOR = {M. Boreale and R. De Nicola and R. Pugliese},
TITLE = {Trace and Testing Equivalence on Asynchronous Processes},
JOURNAL = {Information and Computation},
YEAR = 2002,
VOLUME = 172,
NUMBER = 2,
PAGES = {139-164},
ABSTRACT = {We study trace and may-testing equivalences in
the asynchronous versions of CCS and pi-calculus. We start from
the operational definition of the may-testing preorder and provide
for it finitary and fully abstract trace-based characterizations,
along with a complete in-equational proof system. We also touch upon
two variants of this theory, by first considering a more demanding
equivalence notion (must-testing) and then a richer version of
asynchronous CCS. The results throw light on the difference between
synchronous and asynchronous communication and on the weaker testing
power of asynchronous observations.},
THEMES = {TH3},
SITES = {FI}
}
@INPROCEEDINGS{Boreale.Gadducci.03,
AUTHOR = {M. Boreale, F. Gadducci },
TITLE = {Denotational Testing Semantics in Coinductive Form },
BOOKTITLE = {Proc. of MFCS 2003 },
YEAR = 2003,
EDITOR = {B. Rovan, P. Vojt\'{a}s},
VOLUME = 2747,
SERIES = {Lecture Notes in Computer Science },
PUBLISHER = {Springer},
ABSTRACT = {Building on recent work by Rutten on coinduction and
formal power series, we define a denotational
semantics for the {\sc csp} calculus and prove it
fully abstract for testing equivalence. The proposed
methodology allows for abstract definition of
operators in terms of {\em behavioural differential
equations} and for coinductive reasoning on them,
additionally dispensing with continuous
order-theoretic structures. },
SITES = {FI},
THEMES = {TH4}
}
@INPROCEEDINGS{Boreale.Gorla.2002a,
AUTHOR = {Michele Boreale and Daniele Gorla},
TITLE = {On Compositional Reasoning in the Spi-calculus},
BOOKTITLE = {FOSSACS: International Conference on Foundations of
Software Science and Computation Structures},
PUBLISHER = {{Lecture Notes in Computer Science}},
YEAR = {2002},
SITES = {FI},
THEMES = {TH4},
ABSTRACT = {Observational equivalences can be used to reason
about the correctness of security protocols
described in the spi-calculus. Unlike in CCS or in
pi-calculus, these equivalences do not enjoy a
simple formulation in spi-calculus. The present
paper aims at enriching the set of tools for
reasoning on processes by providing a few equational
laws for a sensible notion of spi-bisimilarity. We
discuss the difficulties underlying compositional
reasoning in spi-calculus and show that, in some
cases and with some care, the proposed laws can be
used to build compositional proofs. A selection of
these laws forms the basis of a proof system that we
show to be sound and complete for the strong version
of bisimilarity.},
PDF = {http://gdn.dsi.unifi.it/~gorla/papers/FoSSaCS02.pdf}
}
@ARTICLE{Boreale.Gorla.2002b,
AUTHOR = {Michele Boreale and Daniele Gorla},
TITLE = {Process Calculi and the Verification of Security
Protocols},
JOURNAL = {Journal of Telecommunication and Information
Technology},
YEAR = 2002,
NOTE = {to appear},
SITES = {FI},
THEMES = {TH4},
ABSTRACT = { Recently there has been much interest towards using
formal methods in the analysis of security
protocols. Some recent approaches take advantage of
concepts and techniques from the field of process
calculi. Process calculi can be given a formal yet
simple semantics, which permits rigorous definitions
of such concepts as `attacker', `secrecy' and
`authentication'. This feature has led to the
development of solid reasoning methods and
verification techniques, a few of which we outline
in this paper.},
PDF = {http://gdn.dsi.unifi.it/~gorla/papers/JTIT02.pdf}
}
@ARTICLE{Corradini.DeNicola.Labella.2002,
AUTHOR = {F. Corradini and R. De Nicola and A. Labella},
TITLE = {An Equational Axiomatization of Bisimulation over Regular Expressions},
JOURNAL = {Journal of Computational Logic},
YEAR = 2002,
VOLUME = 12,
NUMBER = 2,
PAGES = {301-320},
SITES = {FI},
THEMES = {TH3}
}
@ARTICLE{DeNicola.Labella.2003,
AUTHOR = {R. De Nicola and A. Labella},
TITLE = {Nondeterministic regular expressions as solutions of equational systems},
JOURNAL = {Theoretical Computer Science},
YEAR = 2003,
VOLUME = 302,
NUMBER = {1-3},
PAGES = {179-189},
THEMES = {TH3},
SITES = {FI}
}
@ARTICLE{DeNicola.Loreti.2004,
AUTHOR = {Rocco~{De Nicola} and Michele~Loreti},
TITLE = {{A Modal Logic for Mobile Agents}},
JOURNAL = {ACM Transactions on Computational Logic},
YEAR = 2004,
VOLUME = 5,
NUMBER = 1,
SITES = {FI},
THEMES = {TH1},
ABSTRACT = {Klaim is an experimental programming language that
supports a programming paradigm where both processes
and data can be moved across different computing
environments. The language relies on the use of
explicit localities, and on allocation environments
that associate logical localities to physical
sites. This paper presents a temporal logic for
specifying properties of Klaim programs. The logic
is inspired by Hennessy-Milner Logic (HML) and the
mu-calculus, but has novel features that permit
dealing with state properties to describe the effect
of actions over the different sites. The logic is
equipped with a consistent and complete proof system
that enables one to prove properites of mobile
systems.},
URLPS = {http://music.dsi.unifi.it/papers/fullMLMA.ps.gz}
}
@INPROCEEDINGS{Ferrari.Moggi.Pugliese.2002,
AUTHOR = {Gianluigi Ferrari and Eugenio Moggi and Rosario Pugliese },
TITLE = { Guardians for ambient-based monitoring},
BOOKTITLE = {Proc. Foundations of Wide Area Network Programming},
YEAR = {2002},
VOLUME = {66(3)},
SERIES = {{Electronic Notes in Theoretical Computer Science}},
PUBLISHER = {Elsevier},
SITES = {FI,GE,PI},
THEMES = {TH1},
ABSTRACT = {In the Mobile Ambients of Cardelli and Gordon an ambient is a unit
for mobility,
which may contain processes (data) and sub-ambients. Since the
seminal work of Cardelli and Gordon, several ambient-based calculi have been proposed
(Seal, Box-Pi, Safe Ambients, Secure Safe Ambients, Boxed Ambients), mainly for
supporting security. At the operational level these (box- and) ambient-based
calculi differ only in the capabilities of processes. We propose a way of extending
ambient-based calculi, which embodies two principles: an ambient is a unit for
monitoring and coordination, the name of an ambient determines its (monitoring
and coordination) policy. More specifically, to each ambient we attach a
guardian, which monitors the activity of sub-components (i.e. processes and
sub-ambients) and the interaction with the external environment. In our proposal,
guardians and processes play a dual role: guardians are centralized entities
monitoring and inhibiting actions, while processes are decentralized entities
performing actions. We exemplify the use of guardians for enforcing security properties.
}
}
@ARTICLE{Ferrari.Moggi.Pugliese.MetaKlaim-02-11,
AUTHOR = {G. Ferrari and E. Moggi and R. Pugliese},
TITLE = {{MetaKlaim}: A Type Safe Multi-stage Language for
Global Computing},
PDF = {http://www.disi.unige.it/person/MoggiE/ftp/FMP02-sub.pdf},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = 2004,
NOTE = {To appear},
SITES = {FI,GE,PI},
THEMES = {TH2},
ABSTRACT = { This paper describes the design and the semantics
of MetaKlaim, an higher order distributed process
calculus equipped with staging mechanisms. MetaKlaim
integrates MetaML (an extension of SML for
multi-stage programming) and Klaim (a Kernel
Language for Agents Interaction and Mobility), to
permit interleaving of meta-programming activities
(like assembly and linking of code fragments),
dynamic checking of security policies at
administrative boundaries and ``traditional''
computational activities on a wide area network
(like remote communication and code
mobility). MetaKlaim exploits a powerful type system
(including polymorphic types a la system F) to deal
with highly parameterized mobile components and to
dynamically enforce security policies: types are
metadata which are extracted from code at run-time
and are used to express trustiness guarantees. The
dynamic type checking ensures that the trustiness
guarantees of wide are network applications are
maintained whenever computations interoperate with
potentially untrusted components. }
}
@UNPUBLISHED{Gorla.Pugliese.2002a,
AUTHOR = {Daniele Gorla and Rosario Pugliese},
TITLE = {Resource Access and Mobility Control with Dynamic
Privileges Acquisition},
NOTE = {sbmitted},
YEAR = 2002,
SITES = {FI},
THEMES = {TH4},
ABSTRACT = { microKLAIM is a process language that permits
programming distributed systems made up of several
components interacting through multiple distributed
tuple spaces. We present the language and a type
system for controlling the activities, e.g. access
to resources and mobility, of the processes in a
net. By dealing with privileges acquisition and
consumption, the type system enables dynamic
variations of security policies. We exploit a
combination of static and dynamic type checking, and
of in-lined reference monitoring, to guarantee the
absence of run-time errors due to lack of privileges
and show two type safety results: one involves whole
nets, the other is relative to subnets of larger
nets. },
PDF = {http://gdn.dsi.unifi.it/~gorla/papers/muklaim.pdf}
}
@UNPUBLISHED{Gorla.Pugliese.2002b,
AUTHOR = {Daniele Gorla and Rosario Pugliese},
TITLE = {Enforcing Security Policies via Types},
NOTE = {sbmitted},
YEAR = 2002,
SITES = {FI},
THEMES = {TH4},
ABSTRACT = {Security is a key issue for distributed
systems/applications with code mobility, like, e.g.,
e-commerce and on-line bank transactions. In a
scenario with code mobility, traditional solutions
based on cryptography cannot deal with all security
issues and additional mechanisms are necessary. In
this paper, we present a flexible and expressive
type system for security for a calculus of
distributed and mobile processes. By using a
combination of static and dynamic checks, type
safety and well-typedness preservation can be
guaranteed, thus enforcing specific security
policies on the use of resources. The usefulness of
our approach will be shown by modeling the
simplified behaviour of a bank account management
system.},
PDF = {http://gdn.dsi.unifi.it/~gorla/papers/GP-espt.pdf}
}
@INPROCEEDINGS{denicola.ferrari.montanari.pugliese.tuosto.2003,
AUTHOR = {R. {De Nicola} and G.-L. Ferrari and U. Montanari
and R. Pugliese and E. Tuosto},
TITLE = {A Formal Basis for Reasoning on Programmable QoS},
BOOKTITLE = {Proc. of the International Symposium on Verification
(Theory and Practice) -- Celebrating Zohar Manna's
64-th Birthday},
YEAR = {2003},
EDITOR = {N. Dershowitz},
NUMBER = {2772},
SERIES = {Lectures Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
NOTE = {to appear},
ABSTRACT = {The explicit management of Quality of Service (QoS)
of network connectivity, such as, e.g., working
cost, transaction support, and security, is a key
requirement for the development of the novel wide
area network applications. In this paper, we
introduce a foundational model for specification of
QoS attributes at application level. The model
handles QoS attributes as semantic constraints
within a graphical calculus for mobility. In our
approach QoS attributes are related to the
programming abstractions and are exploited to
select, configure and dynamically modify the
underlying system oriented QoS mechanisms.},
SITES = {FI,PI},
THEMES = {TH1}
}
@ARTICLE{ferrari.moggi.pugliese.2003,
AUTHOR = {G.~Ferrari and E.~Moggi and R.~Pugliese},
TITLE = {Higher-Order Types and Meta-Programming for Global
Computing},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = {2003},
NOTE = {to appear},
ABSTRACT = {This paper describes the design and the semantics of
MetaKlaim, an higher order distributed process
calculus equipped with staging mechanisms. MetaKlaim
integrates MetaML (an extension of SML for
multi-stage programming) and Klaim (a Kernel
Language for Agents Interaction and Mobility), to
permit interleaving of meta-programming activities
(like assembly and linking of code fragments),
dynamic checking of security policies at
administrative boundaries and ``traditional''
computational activities on a wide area network
(like remote communication and code
mobility). MetaKlaim exploits a powerful type system
(including polymorphic types \'a la system F) to
deal with highly parameterized mobile components and
to dynamically enforce security policies: types are
metadata which are extracted from code at run-time
and are used to express trustiness guarantees. The
dynamic type checking ensures that the trustiness
guarantees of wide are network applications are
maintained whenever computations interoperate with
potentially untrusted components.},
SITES = {FI,GE,PI},
THEMES = {TH3}
}
@INPROCEEDINGS{gorla.pugliese.2003.01,
AUTHOR = {D. Gorla and R. Pugliese},
TITLE = {Enforcing Security Policies via Types},
BOOKTITLE = {Proc. of International Conference on Security in
Pervasive Computing (SPC'03)},
PAGES = {88-103},
YEAR = 2003,
EDITOR = {D. Hutter and G. Muller and W. Stephan and
M. Ullmann},
NUMBER = 2802,
SERIES = {Lectures Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {Security is a key issue for distributed
systems/applications with code mobility, like, e.g.,
e-commerce and on-line bank transactions. In a
scenario with code mobility, traditional solutions
based on cryptography cannot deal with all security
issues and additional mechanisms are necessary. In
this paper, we present a flexible and expressive
type system for security for a calculus of
distributed and mobile processes. The type system
has been designed to supply real systems security
features, like the assignment of different
privileges to users over different
data/resources. Type soundness is guaranteed by
using a combination of static and dynamic checks,
thus enforcing specific security policies on the use
of resources. The usefulness of our approach is
shown by modeling the simplified behaviour of a bank
account management system.},
SITES = {FI},
THEMES = {TH4}
}
@INPROCEEDINGS{gorla.pugliese.2003.02,
AUTHOR = {D. Gorla and R. Pugliese},
TITLE = {Resource Access and Mobility Control with Dynamic
Privileges Acquisition},
BOOKTITLE = {Proc. of International Colloquium on Automata,
Languages and Programming (ICALP'03)},
PAGES = {119-132},
YEAR = {2003},
EDITOR = {J.C.M. Baeten and J.K. Lenstra and J. Parrow and
G.J. Woeginger},
NUMBER = {2719},
SERIES = {Lectures Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {muKlaim is a process language that permits
programming distributed systems made up of several
mobile components interacting through multiple
distributed tuple spaces. We present the language
and a type system for controlling the activities,
e.g. access to resources and mobility, of the
processes in a net. By dealing with privileges
acquisition, the type system enables dynamic
variations of security policies. We exploit a
combination of static and dynamic type checking, and
of in-lined reference monitoring, to guarantee
absence of run-time errors due to lack of privileges
and state two type soundness results: one involves
whole nets, the other is relative to subnets of
larger nets.},
SITES = {FI},
THEMES = {TH4}
}
@INPROCEEDINGS{gorla.pugliese.2003.03,
AUTHOR = {D. Gorla and R. Pugliese},
TITLE = {Controlling Data Movement in Global Computing
Applications},
BOOKTITLE = {Proc. of the 2004 ACM Symposium on Applied Computing
(SAC'04), Special Track on Programming Languages},
YEAR = {2004},
PUBLISHER = {ACM Press},
NOTE = {to appear},
ABSTRACT = {We present a programming notation aiming at
protecting the secrecy of both host and agent data
in global computing applications. The approach
exploits annotations with sets of node addresses,
called regions. A datum can be annotated with a
region that specifies the network nodes that are
allowed to interact with it. Network nodes come
equipped with two region annotations specifying the
nodes that can send data and spawn processes over
them. The language semantics guarantees that
computation proceeds according to these region
constraints. To minimize the overhead of runtime
checks, a static compilation phase is exploited. The
proposed approach is largely independent of a
specific programming language; however, to put it in
concrete form, here we focus on its integration
within the process language muKlaim. We prove that
in compiled muKlaim nets, data can be manipulated
only by authorized users. We also give a more local
formulation of this property, where only a subnet is
compiled. Finally, we use our theory to model the
secure behaviour of a UNIX-like multiuser system.},
SITES = {FI},
THEMES = {TH4}
}
This file has been generated by
bibtex2html 1.65