Fabio Martinelli

LPAR Conference 2017 Conference Paper

A Quantitative Partial Model-Checking Function and Its Optimisation

• Stefano Bistarelli
• Fabio Martinelli
• Ilaria Matteucci
• Francesco Santini 0001

Partial Model-Checking (PMC) is an efficient tool to reduce the combinatorial explosion of a state-space, arising in the verification of loosely-coupled software systems. At the same time, it is useful to consider quantitative temporal-modalities. This allows for checking whether satisfying such a desired modality is too costly, by comparing the final score consisting of how much the system spends to satisfy the policy, to a given threshold. We stir these two ingredients together in order to provide a Quantitative PMC function (QPMC), based on the algebraic structure of semirings. We design a method to extract part of the weight during QPMC, with the purpose to avoid the evaluation of a modality as soon as the threshold is crossed. Moreover, we extend classical heuristics to be quantitative, and we investigate the complexity of QPMC. Keyword: Partial Model Checking, Semirings, Optimisation, Quantitative Modal Logic Quantitative Process Algebra, Quantitative Evaluation of Systems.

FormaliSE Conference 2017 Conference Paper

Model Checking for Mobile Android Malware Evolution

• Aniello Cimitile
• Fabio Martinelli
• Francesco Mercaldo
• Vittoria Nardone
• Antonella Santone
• Gigliola Vaglini

Software engineering researchers have largely demonstrated that newer versions of software make use of previous versions of existing software. No exception to this rule for the so-called malicious software, that frequently evolves in order to evade the detection by antimalware. As matter of fact, mobile malicious programs, such as trojans, are frequently related to previous malware through evolutionary relationships. Discovering those relationships and constructing a phylogenetic model is expected to be helpful for analyzing new malware and for establishing a principled naming scheme. In this paper we propose a model checking based method to infer mobile malware phylogenetic trees. We demonstrate, implementing our approach in the droid-Sapiens tool, that mobile malware families come from an ancestor and they infuence own descendant, basing on the payload that they exhibit.

STOC Conference 2013 Conference Paper

Random lattice triangulations: structure and algorithms

• Pietro Caputo
• Fabio Martinelli
• Alistair Sinclair
• Alexandre Stauffer

FOCS Conference 2011 Conference Paper

Sharp Mixing Time Bounds for Sampling Random Surfaces

• Pietro Caputo
• Fabio Martinelli
• Fabio Lucio Toninelli

We analyze the mixing time of a natural local Markov Chain (Gibbs sampler) for two commonly studied models of random surfaces: (i) discrete monotone surfaces with "almost planar" boundary conditions and(ii) the one-dimensional discrete Solid-on-Solid (SOS)model. In both cases we prove the first almost optimal bounds. Our proof is inspired by the so-called "meancurvature" heuristic: on a large scale, the dynamics should approximate a deterministic motion in which each point of the surface moves according to a drift proportional to the local inverse mean curvature radius. Key technical ingredients are monotonicity, coupling and an argument due to D. Wilson [17] in the framework of lozenge tiling Markov Chains. The novelty of our approach with respect to previous results consists in proving that, with high probability, the dynamics is dominated by a deterministic evolution which follows the mean curvature prescription. Our method works equally well for both models despite the fact that their equilibrium maximal deviations from the average height profile occur on very different scales.

STOC Conference 2009 Conference Paper

Mixing time for the solid-on-solid model

• Fabio Martinelli
• Alistair Sinclair

We analyze the mixing time of a natural local Markov chain (the Glauber dynamics) on configurations of the solid-on-solid model of statistical physics. This model has been proposed, among other things, as an idealization of the behavior of contours in the Ising model at low temperatures. Our main result is an upper bound on the mixing time of O~(n 3.5 ), which is tight within a factor of O~(√n). The proof, which in addition gives insight into the actual evolution of the contours, requires the introduction of several novel analytical techniques that we conjecture will have other applications.

TCS Journal 2005 Journal Article

Theoretical foundations of security analysis and design II

• Roberto Gorrieri
• Fabio Martinelli

SODA Conference 2004 Conference Paper

Fast mixing for independent sets, colorings and other models on trees

• Fabio Martinelli
• Alistair Sinclair
• Dror Weitz

TCS Journal 2003 Journal Article

A comparison of three authentication properties

• Riccardo Focardi
• Roberto Gorrieri
• Fabio Martinelli

Authentication is a slippery security property that has been formally defined only recently; among the recent definitions, two rather interesting ones have been proposed for the spi-calculus by (Abadi and Gordon (in: Proc. CONCUR’97, Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 59–73; Inform. and Comput. 148(1) (1999) 1–70) and for CSP by Lowe (in: Proc. 10th Computer Security Foundation Workshop, IEEE Press, 1997, pp. 31–43). On the other hand, in a recent paper (in: Proc. World Congr. on Formal Methods (FM’99), Lecture Notes in Computer Science, Vol. 1708, Springer, Berlin, 1999, pp. 794–813), we have proved that many existing security properties can be seen uniformly as specific instances of a general scheme based on the idea of non-interference. The purpose of this paper is to show that, under reasonable assumptions, spi-authentication can be recast in this general framework as well, by showing that it is equivalent to the non-interference property called NDC of Focardi and Gorrieri (J. Comput. Security 3(1) (1994/1995) 5–33; IEEE Trans. Software Eng. 23(9) (199) 550–571). This allows for the comparison between such a property and the one based on CSP, which was already recast under the general scheme of Focardi and Martinelli (1999).

TCS Journal 2003 Journal Article

Analysis of security protocols as open systems

• Fabio Martinelli

We propose a methodology for the formal analysis of security protocols. This originates from the observation that the verification of security protocols can be conveniently treated as the verification of open systems, i. e. systems which may have unspecified components. These might be used to represent a hostile environment wherein the protocol runs and whose behavior cannot be predicted a priori. We define a language for the description of security protocols, namely Crypto-CCS, and a logical language for expressing their properties. We provide an effective verification method for security protocols which is based on a suitable extension of partial model checking. Indeed, we obtain a decidability result for the secrecy analysis of protocols with a finite number of sessions, bounded message size and new nonce generation.

MFCS Conference 2003 Invited Paper

Process Algebraic Frameworks for the Specification and Analysis of Cryptographic Protocols

• Roberto Gorrieri
• Fabio Martinelli

Abstract Two process algebraic approaches for the analysis of cryptographic protocols, namely the spi calculus by Abadi and Gordon and CryptoSPA by Focardi, Gorrieri and Martinelli, are surveyed and compared. We show that the two process algebras have comparable expressive power, by providing an encoding of the former into the latter. We also discuss the relationships among some security properties, i. e. , authenticity and secrecy, that have different definitions in the two approaches.

FOCS Conference 2003 Conference Paper

The Ising Model on Trees: Boundary Conditions and Mixing Time

• Fabio Martinelli
• Alistair Sinclair
• Dror Weitz

We give the first comprehensive analysis of the effect of boundary conditions on the mixing time of the Glauber dynamics for the Ising model. Specifically, we show that the mixing time on an n-vertex regular tree with (+) boundary remains O(n log n) at all temperatures (in contrast to the free boundary case, where the mixing time is not bounded by any fixed polynomial at low temperatures). We also show that this bound continues to hold in the presence of an arbitrary external field. Our results are actually stronger, and provide tight bounds on the log-Sobolev constant and the spectral gap of the dynamics. In addition, our methods yield simpler proofs and stronger results for the mixing time in the regime where it is insensitive to the boundary condition. Our techniques also apply to a much wider class of models, including those with hard constraints like the antiferromagnetic Potts model at zero temperature (colorings) and the hard-core model (independent sets).

MFCS Conference 2002 Conference Paper

Symbolic Semantics and Analysis for Crypto-CCS with (Almost) Generic Inference Systems

• Fabio Martinelli

Abstract Crypto-CCS is a formal description language for distributed protocols which is suitable to abstractly model the cryptographic ones. Indeed, this language adopts a message-manipulating rule which may be used to mimic some features of cryptographic functions. We equip the Crypto-CCS calculus with a symbolic operational semantics. Moreover, we provide a mechanized method to analyze the security properties of cryptographic protocols (with finite behaviour), symbolically. Our work extends the previous one on symbolic verification techniques for cryptographic protocols modeled with process algebras since it deals with (almost) generic inference systems instead of fixed ones.