Riccardo Focardi, Roberto Gorrieri, Ruggero Lanotte, Andrea Maggiolo-Schettini, Fabio Martinelli, Simone Tini, and Enrico Tronci. "Formal Models of Timing Attacks on Web Privacy." Electronic Notes in Theoretical Computer Science 62 (2002): 229–243. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types. DOI: 10.1016/S1571-0661(04)00329-9.
Abstract: We model a timing attack on web privacy proposed by Felten and Schneider by using three different approaches: HL-Timed Automata, SMV model checker, and tSPA Process Algebra. Some comparative analysis on the three approaches is derived.
|
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivano Salvo, and Vladimiro Sassone. "A Type Inference Algorithm for Secure Ambients." Electronic Notes in Theoretical Computer Science 62 (2002): 83–101. Elsevier. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types. DOI: 10.1016/S1571-0661(04)00321-4.
Abstract: We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottom-up algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario.
|
"Charme." In Lecture Notes in Computer Science, edited by D. Geist and E. Tronci. Vol. 2860. Springer, 2003. ISSN: 3-540-20363-X. DOI: 10.1007/b93958.
|
Ester Ciancamerla, Michele Minichino, Stefano Serro, and Enrico Tronci. "Automatic Timeliness Verification of a Public Mobile Network." In 22nd International Conference on Computer Safety, Reliability, and Security (SAFECOMP), edited by S. Anderson, M. Felici and B. Littlewood, 35–48. Lecture Notes in Computer Science 2788. Edinburgh, UK: Springer, 2003. ISSN: 978-3-540-20126-7. DOI: 10.1007/978-3-540-39878-3_4.
Abstract: This paper deals with the automatic verification of the timeliness of Public Mobile Network (PMN), consisting of Mobile Nodes (MNs) and Base Stations (BSs). We use the Mur$\varphi$ Model Checker to verify that the waiting access time of each MN, under different PMN configurations and loads, and different inter arrival times of MNs in a BS cell, is always below a preassigned threshold. Our experimental results show that Model Checking can be successfully used to generate worst case scenarios and nicely complements probabilistic methods and simulation which are typically used for performance evaluation.
|
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, and Marisa Venturini Zilli. "Synchronized regular expressions." Acta Inf. 39, no. 1 (2003): 31–70.
Abstract: Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday also increases the need of more powerful tools to interact with texts. Indeed, much work has been done to provide simple and versatile tools that can be useful for the most common text manipulation tasks. Regular Expressions (RE), introduced by Kleene, are well known in the formal language theory. RE have been extended in various ways, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [15] UNIX command, or the Perl [20] language pattern matching constructs) we find backreferences, i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. In this paper we introduce the Synchronized Regular Expressions (SRE) as an extension of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are dealing with formalisms that should have a practical utility and be used in real applications, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user-friendly syntax for SRE to be used in implementations of SRE-powered search algorithms.
|
Marco Gribaudo, Andras Horváth, Andrea Bobbio, Enrico Tronci, Ester Ciancamerla, and Michele Minichino. "Fluid Petri Nets and hybrid model checking: a comparative case study." Int. Journal on: Reliability Engineering & System Safety 81, no. 3 (2003): 239–257. Elsevier. DOI: 10.1016/S0951-8320(03)00089-9.
Abstract: The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out. Our approach is illustrated by means of a ’real world’ hybrid system: the temperature control system of a co-generative plant.
|
Antonio Bucciarelli, Adolfo Piperno, and Ivano Salvo. "Intersection types and λ-definability." Mathematical Structures in Computer Science 13, no. 1 (2003): 15–53. Cambridge University Press. ISSN: 0960-1295. DOI: 10.1017/S0960129502003833.
Abstract: This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.
|
Mario Coppo, Mariangiola Dezani-Ciancaglini, Elio Giovannetti, and Ivano Salvo. "Mobility Types for Mobile Processes in Mobile Ambients." Electr. Notes Theor. Comput. Sci. 78 (2003). DOI: 10.1016/S1571-0661(04)81011-9.
Abstract: We present an ambient-like calculus in which the open capability is dropped, and a new form of “lightweight  process mobility is introduced. The calculus comes equipped with a type system that allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the “minimal  requirements to accept a system or a component as well typed. This gives a kind of principal typing. As an expressiveness test, we show that some well known calculi of concurrency and mobility can be encoded in our calculus in a natural way.
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier." In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings, edited by D. Geist and E. Tronci, 394–409. Lecture Notes in Computer Science 2860. Springer, 2003. ISSN: 3-540-20363-X. DOI: 10.1007/978-3-540-39724-3_34.
Abstract: In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Integrating RAM and Disk Based Verification within the Mur$\varphi$ Verifier." In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings, edited by D. Geist and E. Tronci, 277–282. Lecture Notes in Computer Science 2860. Springer, 2003. ISSN: 3-540-20363-X. DOI: 10.1007/978-3-540-39724-3_25.
Abstract: We present a verification algorithm that can automatically switch from RAM based verification to disk based verification without discarding the work done during the RAM based verification phase. This avoids having to choose beforehand the proper verification algorithm. Our experimental results show that typically our integrated algorithm is as fast as (sometime faster than) the fastest of the two base (i.e. RAM based and disk based) verification algorithms.
|