Author name cluster

Chiara Bodei

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

I&C Journal 2020 Journal Article

The link-calculus for open multiparty interactions

Chiara Bodei
Linda Brodo
Roberto Bruni

We present the link-calculus, an extension of π-calculus, that models interactions that are multiparty, i. e. that may involve more than two processes, mutually exchanging data. Communications are seen as chains of suitably combined links (which record the source and the target ends of each hop of interactions), each contributed by one party. Values are exchanged by means of message tuples, still provided by each party. We develop semantic theories and proof techniques for link-calculus and apply them in reasoning about complex distributing computing scenarios, where more than two participants need to synchronise in order to perform a task. In particular, we introduce the notion of linked bisimilarity in analogy with the early bisimilarity of the π-calculus. Differently from the π-calculus case, we can show that it is a congruence with respect to all the link-calculus operators and that is also closed under name substitution.

Details DOI

TCS Journal 2019 Journal Article

A formal approach to open multiparty interactions

Chiara Bodei
Linda Brodo
Roberto Bruni

We present a process algebra aimed at describing interactions that are multiparty, i. e. that may involve more than two processes and that are open, i. e. the number of the processes they involve is not fixed or known a priori. Here we focus on the theory of a core version of a process calculus, without message passing, called Core Network Algebra (CNA). In CNA communication actions are given not in terms of channels but in terms of chains of links that record the source and the target ends of each hop of interactions. The operational semantics of our calculus mildly extends the one of CCS. The abstract semantics is given in the style of bisimulation but requires some ingenuity. Remarkably, the abstract semantics is a congruence for all operators of CNA and also with respect to substitutions, which is not the case for strong bisimilarity in CCS. As a motivating and running example, we illustrate the model of a simple software defined network infrastructure.

Details DOI

TCS Journal 2019 Journal Article

Measuring security in IoT communications

Chiara Bodei
Stefano Chessa
Letterio Galletta

More smart objects and more applications on the Internet of Things (IoT) mean more security challenges. In IoT security is crucial but difficult to obtain. On the one hand the usual trade-off between highly secure and usable systems is more impelling than ever; on the other hand security is considered a feature that has a cost often unaffordable. Therefore, IoT designers not only need tools to assess possible risks and to study countermeasures, but also methodologies to estimate their costs. Here, we present a methodology, based on the process calculus IoT-LySa, to infer quantitative measures on evolution of systems. The derived quantitative evaluation is exploited to establish the cost of the possible security countermeasures, in terms of time and energy.

Details DOI

LOPSTR Conference 2015 Conference Paper

A Global Occurrence Counting Analysis for Brane Calculi

Chiara Bodei
Linda Brodo
Roberta Gori
Diana Hermith
Francesca Levi

Abstract We propose a polynomial static analysis for Brane Calculi [ 6 ], based on Abstract Interpretation [ 8 ] techniques. The analysis provides a description of the possible hierarchical structure of membranes and of the processes possibly associated to each membrane, together with global occurrence counting information. Our analysis can be applied in the biological setting to investigate systems in which the information on the number of membranes occurring in the system plays a crucial role.

Details

TCS Journal 2015 Journal Article

Causal static analysis for Brane Calculi

Chiara Bodei
Roberta Gori
Francesca Levi

We present here a static analysis, based on Abstract Interpretation [8], obtained by defining an abstract version of the causal semantics for the Mate/Bud/Drip (MBD) version of Brane Calculi [7], proposed by Busi [6]. Our analysis statically approximates the dynamic behaviour of MBD systems. More precisely, the analysis is able to describe the essential behaviour of the represented membranes, in terms of their possible interactions. Furthermore, our analysis is able to statically capture the possible causal dependencies among interactions, whose determination can be exploited to better understand the modelled biological phenomena. Finally, we apply our analysis to an abstract specification of the receptor-mediated endocytosis mechanism.

Details DOI

TCS Journal 2009 Journal Article

A Control Flow Analysis for Beta-binders with and without static compartments

Chiara Bodei

We introduce a Control Flow Analysis, that statically approximates the dynamic behaviour of processes, expressed in the Beta-binders calculus and in an extended version of the calculus modelling static compartments. Our analysis of a system is able to describe the essential behaviour of each box, tracking all the possible bindings of variables, all the possible intra- and inter-boxes communications, and, finally, all the possible movements across compartments. The analysis offers a basis for establishing static checks of biological dynamic properties. We apply our analysis to an abstract specification of the interaction between a virus and cells of the immune system and to a model of the c A M P -signaling Pathway in Olfactory Sensory Neurons.

Details DOI

TCS Journal 2002 Journal Article

Primitives for authentication in process algebras

Chiara Bodei
Pierpaolo Degano
Riccardo Focardi
Corrado Priami

We extend the π-calculus and the spi-calculus with two primitives that guarantee authentication. They enable us to abstract from various implementations/specifications of authentication, and to obtain idealized protocols which are “secure by construction”. The main underlying idea, originally proposed in Focardi (Proc. Sixth Italian Conf. on Theoretical Computer Science, November 1998) for entity authentication, is to use the locations of processes in order to check who is sending a message (authentication of a party) and who originated a message (message authentication). The theory of local names, developed in Bodei et al. (Theoret. Comput. Sci. 253(2) (2001) 155) for the π-calculus, gives us almost for free both the partner authentication and the message authentication primitives.

Details DOI

TCS Journal 2001 Journal Article

Names of the π-calculus agents handled locally

Chiara Bodei
Pierpaolo Degano
Corrado Priami

We address the problem of handling names in concurrent and distributed systems made up of mobile processes. We equip processes with local environments. Our structural operational semantics handles these environments so that captures of names are never possible. Our semantics includes the specification of a distributed name manager that conservatively extends standard operational semantics. Bisimulation-based equivalences can be checked on our transition systems. They yield the same equivalence relations as those based on standard interleaving semantics. Finally, we show that our development scales up smoothly to higher-order calculi.

Details DOI

I&C Journal 2001 Journal Article

Static Analysis for the π-Calculus with Applications to Security

Chiara Bodei
Pierpaolo Degano
Flemming Nielson
Hanne Riis Nielson

Control Flow Analysis is a static technique for predicting safe and computable approximations to the set of values that the objects of a program may assume during its execution. We present an analysis for the π-calculus that shows how names will be bound to actual channels at run time. The result of our analysis establishes a super-set of the set of channels to which a given name may be bound and of the set of channels that may be sent along a given channel. Besides a set of rules that permits one to validate a given solution, we also offer a constructive procedure that builds solutions in low polynomial time. Applications of our analysis include establishing two simple security properties of processes. One example is that P has no leaks: P offers communication to the external environment through public channels only and confines its secret channels within itself. The other example is connected to the no read-up/no write-down property of Bell and LaPadula: once processes are given levels of security clearance, we check that a process at a high level never sends channels to processes at a lower level.

Details DOI