FRANCESCO SPEGNI

Pubblicazioni

FRANCESCO SPEGNI

 

17 pubblicazioni classificate nel seguente modo:

Nr. doc. Classificazioni
12 4 Contributo in Atti di Convegno (Proceeding)
4 1 Contributo su Rivista
1 8 Tesi di dottorato
Anno
Risorse
2020
Parameterized model checking of networks of timed automata with Boolean guards
THEORETICAL COMPUTER SCIENCE
Autore/i: Spalazzi, L.; Spegni, F.
Classificazione: 1 Contributo su Rivista
Abstract: Parameterized model checking is a formal verification technique for verifying that some specifications hold in systems consisting of many similar cooperating but indistinguishable processes. The problem is known to be undecidable in general, even when restricted to reachability properties. To overcome this limitation, several techniques have been explored to address specific system families, logical formulas or topologies of process networks. Some use the notion of cutoff, i.e. if a certain property is verified for systems up to a certain size (the cutoff) then it is verified for systems of any size. Here we analyze the case of networks consisting of an arbitrary number of timed automata that can synchronize by looking at which state the neighbors are currently. We show that cutoffs exist independently from the checked formula, with or without a distinguished process acting as controller. We show how, exploiting the cutoffs, we can obtain upper bounds on complexity of the parameterized model-checking problem. Finally, we show how to use the theoretical results in order to model and verify a distributed algorithm for clock synchronization based on gossip techniques.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/275520 Collegamento a IRIS

2020
Verifying temporal specifications of Java programs
SOFTWARE QUALITY JOURNAL
Autore/i: Spegni, F.; Spalazzi, L.; Liva, G.; Pinzger, M.; Bollin, A.
Classificazione: 1 Contributo su Rivista
Abstract: Many Java programs encode temporal behaviors in their source code, typically mixing three features provided by the Java language: (1) pausing the execution for a limited amount of time, (2) waiting for an event that has to occur before a deadline expires, and (3) comparing timestamps. In this work, we show how to exploit modern SMT solvers together with static analysis in order to produce a network of timed automata approximating the temporal behavior of a set of Java threads. We also prove that the presented abstraction preserves the truth of MTL and ATCTL formulae, two well-known logics for expressing timed specifications. As far as we know, this is the first feasible approach enabling the user to automatically model check timed specifications of Java software directly from the source code.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/282888 Collegamento a IRIS

2019
High-Performance Computing for Formal Security Assessment
2019 International Conference on High Performance Computing and Simulation, HPCS 2019
Autore/i: Spalazzi, L.; Spegni, F.
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Assessing the degree of security of a given system w.r.t. some attacker model and security policy can be done by means of formal methods. For instance, the system can be described as a Markov Decision Process, the security policy by means of a modal logic formula, PCTL∗, and then a probabilistic model checker can return the probability with which the policy holds in the system. This methodology suffices when all the system parameters and their values are known a priori. On the other side, in case the degree of security of the system depends on the values of the system parameters, the formally security assessment task must output a probability function which takes the system parameters and returns the probability of a successful attack to the security of the system. One simple way to describe such function involves solving many instances of the probabilistic model checking problem, one for each combination of the parameter values. In this scenario, probabilistic model checking, which suffers from the state explosion problem, may become an unfeasible task for traditional workstations or even servers.In this work we introduce the tool SecMC which drives the user in the task of modeling the system under analysis and the required security policies, together with the parameters that affect them. Next, the user can specify the range of values assumed by the parameters, and the tool can take care of iterating the probabilistic model checking task, distributing the computations among different local or remote nodes of a cluster, and collect the results to produce a combined picture of how the level of security varies w.r.t. the parameter values.In this paper we show how the tool can be used in order to formally assess security of probabilistic systems known from the literature, viz. a probabilistic cryptographic protocol, a synchronization algorithm for wireless devices inspired by fireflies in nature, and the privacy of dispersed cloud storages.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/290379 Collegamento a IRIS

2019
Verification-as-a-Service for Parameter Assessment
2019 International Conference on High Performance Computing and Simulation, HPCS 2019
Autore/i: Spalazzi, L.; Spegni, F.
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: When a professional or researcher faces the task of analyzing some real-world IT system, being it a security protocol, a piece of software, or something else, it comes the moment when the system parameters are enumerated and for each of them he/she has to define its possible values.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/290378 Collegamento a IRIS

2019
Automatic Repair of Timestamp Comparisons
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING
Autore/i: Liva, Giovanni; Khan, Muhammad Taimoor; Pinzger, Martin; Spegni, Francesco; Spalazzi, Luca
Classificazione: 1 Contributo su Rivista
Abstract: Automated program repair has the potential to reduce the developers' effort to fix errors in their code. In particular, modern programming languages, such as Java, C, and C#, represent time as integer variables that suffer from integer overflow, introducing subtle errors that are hard to discover and repair. Recent researches on automated program repair rely on test cases to discover failures to correct, making them suitable only for regression errors. We propose a new strategy to automatically repair programs that suffer from timestamp overflows that are manifested in comparison expressions. It unifies the benefits of static analysis and automatic program repair avoiding dependency on testing to identify and correct defected code. Our approach performs an abstract analysis over the time domain of a program using a Time Type System to identify the problematic comparison expressions. The repairing strategy rewrites the timestamp comparisons exploiting the binary representation of machine numbers to correct the code. We have validated the applicability of our approach with 20 open source Java projects. The results show that it is able to correctly repair all 246 identified errors. To further validate the reliability of our approach, we have proved the soundness of both, type system and repairing strategy. Furthermore, several patches for three open source projects have been acknowledged and accepted by their developers.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/275521 Collegamento a IRIS

2018
Towards model checking security of real time Java software
Proceedings - 2018 International Conference on High Performance Computing and Simulation, HPCS 2018
Autore/i: Spalazzi, Luca; Spegni, Francesco; Liva, Giovanni; Pinzger, Martin
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: More and more software libraries and applications in high-performance computing and distributed systems are coded using the Java programming language. The correctness of such pieces of code w.r.t. a given set of security policies often depends on the correct handling of timing between concurrent or recurrent events. Model-checking has proven to be an effective tool for verifying the correctness of software. In spite of the growing importance of this application area of formal methods, though, no approach exists that targets the problem of verifying the correctness of real-Time software w.r.t.Timed specifications. The few existing works focus on very different problems, such as schedulability analysis of Java tasks. In this paper we present an approach combining rule-based static analysis together with symbolic execution of Java code to extract networks of timed automata from existing software and then use Uppaal to model-check them against timed specifications. We show through a real-world case study that this approach can be helpful in model-checking security policies of real-Time Java software.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/265853 Collegamento a IRIS

2018
Modeling Time in Java Programs for Automatic Error Detection
Proceedings - 2018 ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018
Autore/i: Liva, Giovanni; Khan, Muhammad Taimoor; Spalazzi, Luca; Spegni, Francesco; Bollin, Andreas; Pinzger, Martin
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Modern programming languages, such as Java, represent time as integer variables, called timestamps. Timestamps allow developers to tacitly model incorrect time values resulting in a program failure because any negative value or every positive value is not necessarily a valid time representation. Current approaches to automatically detect errors in programs, such as Randoop and FindBugs, cannot detect such errors because they treat timestamps as normal integer variables and test them with random values verifying if the program throws an exception. In this paper, we present an approach that considers the time semantics of the Java language to systematically detect time related errors in Java programs. With the formal time semantics, our approach determines which integer variables handle time and which statements use or alter their values. Based on this information, it translates these statements into an SMT model that is passed to an SMT solver. The solver formally verifies the correctness of the model and reports the violations of time properties in that program. For the evaluation, we have implemented our approach in a prototype tool and applied it to the source code of 20 Java open source projects. The results show that our approach is scalable and it is capable of detecting time errors precisely enough allowing its usability in real-world applications.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/265851 Collegamento a IRIS

2017
Disjunctive timed networks
CEUR Workshop Proceedings
Autore/i: Spalazzi, Luca; Spegni, Francesco
Editore: CEUR-WS
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/255501 Collegamento a IRIS

2017
A probabilistic small model theorem to assess confidentiality of dispersed cloud storage (extended abstract)
Proc. ICTCS 2017 and CILC 2017
Autore/i: Baldi, Marco; Bartocci, Ezio; Chiaraluce, Franco; Cucchiarelli, Alessandro; Senigagliesi, Linda; Spalazzi, Luca; Spegni, Francesco
Editore: CEUR-WS
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Recent developments in cloud architectures and security concerns have originated new models of online storage clouds based on data dispersal algorithms. According to these lgorithms the data is divided into several slices that are distributed among remote and independent storage nodes. Ensuring confidentiality in this context is crucial: only legitimate users should access any part of information they distribute among storage nodes. We use parameterized Markov Decision Processes to model such a class of systems and Probabilistic Model Checking to assess the likelihood of breaking the confidentiality.We showed that a Small Model Theorem can be proven for a specific types of models, preserving PCTL formulae. Finally, we report the result of applying our methodology to feasibly assess the security of existing dispersed cloud storage solutions.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/252391 Collegamento a IRIS

2017
Accuracy of message counting abstraction in fault-tolerant distributed algorithms
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Autore/i: Konnov, Igor; Widder, Josef; SPEGNI, FRANCESCO; SPALAZZI, Luca
Editore: Springer Verlag
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/247855 Collegamento a IRIS

2017
A probabilistic small model theorem to assess confidentiality of dispersed cloud storage
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) - 14th International Conference on Quantitative Evaluation of Systems, QEST 2017
Autore/i: BALDI, Marco; Bartocci, Ezio; CHIARALUCE, FRANCO; CUCCHIARELLI, ALESSANDRO; SENIGAGLIESI, LINDA; SPALAZZI, Luca; SPEGNI, FRANCESCO
Editore: Springer Verlag
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Recent developments in cloud architectures have originated new models of online storage clouds based on data dispersal algorithms. According to these algorithms the data is divided into several slices that are distributed among remote and independent storage nodes. Ensuring confidentiality in this context is crucial: only legitimate users should access any part of information they distribute among storage nodes. To the best of our knowledge, the security analysis and assessment of existing solutions always assumes of homogeneous networks and honestbut-curious nodes as attacker model.We analyze more complex scenarios with heterogeneous network topologies and a passive attacker eavesdropping the channel between user and storage nodes. We use parameterized Markov Decision Processes to model such a class of systems and Probabilistic Model Checking to assess the likelihood of breaking the confidentiality. Even if, generally speaking, the parameterized model checking is undecidable, in this paper, however, we proved a Small Model Theorem that makes such a problem decidable for the class of models adopted in this work. We discovered that confidentiality is highly affected by parameters such as the number of slices and the number of write and read requests. At design-time, the presented methodology helps to determine the optimal values of parameters affecting the likelihood of a successful attack to confidentiality.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/250578 Collegamento a IRIS

2017
Security in heterogeneous distributed storage systems: a practically achievable information-theoretic approach
Proc. ISCC 2017
Autore/i: BALDI, Marco; CHIARALUCE, FRANCO; SENIGAGLIESI, LINDA; SPALAZZI, Luca; SPEGNI, FRANCESCO
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Distributed storage systems and caching systems are becoming widespread, and this motivates the increasing interest on assessing their achievable performance in terms of reliability for legitimate users and security against malicious users. While the assessment of reliability takes benefit of the availability of well established metrics and tools, assessing security is more challenging. The classical cryptographic approach aims at estimating the computational effort for an attacker to break the system, and ensuring that it is far above any feasible amount. This has the limitation of depending on attack algorithms and advances in computing power. The information-theoretic approach instead exploits capacity measures to achieve unconditional security against attackers, but often does not provide practical recipes to reach such a condition. We propose a mixed cryptographic/information theoretic approach with a twofold goal: estimating the levels of information-theoretic security and defining a practical scheme able to achieve them. In order to find optimal choices of the parameters of the proposed scheme, we exploit an effective probabilistic model checker, which allows us to overcome several limitations of more conventional methods.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/250053 Collegamento a IRIS

2016
Parametric and probabilistic model checking of confidentiality in data dispersal algorithms
2016 International Conference on High Performance Computing and Simulation, HPCS 2016
Autore/i: BALDI, Marco; CUCCHIARELLI, ALESSANDRO; SENIGAGLIESI, LINDA; SPALAZZI, Luca; SPEGNI, FRANCESCO
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Recent developments in cloud storage architectures have originated new models of online storage as cooperative storage systems and interconnected clouds. Such distributed environments involve many organizations, thus ensuring confidentiality becomes crucial: only legitimate clients should recover the information they distribute among storage nodes. In this work we present a unified framework for verifying confidentiality of dispersal algorithms against probabilistic models of intruders. Two models of intruders are given, corresponding to different types of attackers: one aiming at intercepting as many slices of information as possible, and the other aiming at attacking the storage providers in the network. Both try to recover the original information, given the intercepted slices. By using probabilistic model checking, we can measure the degree of confidentiality of the system exploring exhaustively all possible behaviors. Our experiments suggest that dispersal algorithms ensure a high degree of confidentiality against the slice intruder, no matter the number of storage providers in the system. On the contrary, they show a low level of confidentiality against the provider intruder in networks with few storage providers (e.g. interconnected cloud storage solutions).
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/239606 Collegamento a IRIS

2014
Parameterized model-checking of timed systems with conjunctive guards
Verified Software: Theories, Tools and Experiments
Autore/i: Spalazzi, Luca; Spegni, Francesco
Editore: Springer Verlag
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/225667 Collegamento a IRIS

2013
Model Checking Grid Security
FUTURE GENERATION COMPUTER SYSTEMS
Autore/i: F. Pagliarecci; F. Spegni; L. Spalazzi
Classificazione: 1 Contributo su Rivista
Abstract: Grid computing is one of the leading forms of high performance computing. Security in the grid environment is a challenging issue that can be characterized as a complex system involving many subtleties that may lead designers into error. This is similar to what happens with security protocols where automatic verification techniques (specially model checking) have been proved to be very useful at design time. This paper proposes a formal verification methodology based on model checking that can be applied to host security verification for grid systems. The proposed methodology must take into account that a grid system can be described as a parameterized model, and security requirements can be described as hyperproperties. Unfortunately, both parameterized model checking and hyperproperty verification are, in general, undecidable. However, it has been proved that this problem becomes decidable when jobs have some regularities in their organization. Therefore, this paper presents a verification methodology that reduces a given grid system model to a model to which it is possible to apply a ‘‘cutoff’’ theorem (i.e., a requirement is satisfied by a system with an arbitrary number of jobs if and only if it is satisfied by a system with a finite number of jobs up to a cutoff size). This methodology is supported by a set of theorems, whose proofs are presented in this paper. The methodology is explained by means of a case study: the Condor system.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/87601 Collegamento a IRIS

2012
Formal methods for practical reverse engineering and software verification
Editore: Università Politecnica delle Marche
Classificazione: 8 Tesi di dottorato
Abstract: Software development processes are committed at producing high quality software system. Traditionally, this goal is reached through systematic testing. This thesis project analyzes the possibility of applying mathematical logic and so-called formal methods into the software development process. In fact software testing has two major limitations with respect to verification by means of software testing: every test can show correctness for one possible behavior, while formal methods verification shows that correctness, if proved, holds for all the executions of the system. Furthermore, testing can be used to stress the system implementation, while formal verification can be done also during earlier stages of software development, when abstract models of the system are first sketched. In this work we present an integrated working environment that aims at guiding the software engineer along some of the most relevant moments of a software system lifetime: its development, its verification, its maintenance up to a complete re-structuring. The core of the proposed environment is the language XAL , a parametric extension of the theory of networks of timed automata. After defining its syntax and semantics, we show a novel cutoff theorem for it, proving that systems that are both parametric and timed can be model checked. We then describe two methodologies: the former helps in restructuring existing applications using XAL , extracting parameterized finite-state models from legacy code. The latter is about conducting a formal verification using XAL and its cutoff theorem, if needed. A few case-studies are described that uses the proposed language and methodologies. These case-studies are real-world software systems analyzed in a joint effort with Computer VAR ITT and BINT, two Italian ITC companies.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/242049 Collegamento a IRIS

2012
A modular environment for software development and re-engineering
2012 Second International Workshop on Developing Tools as Plug-Ins (TOPI)
Autore/i: Salvatore Campana; Andrea Poli; Luca Spalazzi; Francesco Spegni
Editore: IEEE COMPUTER SOCIETY
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Traditional software development processes are designed to deal with the construction of new software systems. We believe the software development methodologies should include from the beginning the possibility of a re-engineering phase. With our work we identify the main characteristics that make software (re)engineering tools useful and usable Developing them in a modular architecture allows for a better integration with the developer’s working habits.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/87612 Collegamento a IRIS




Università Politecnica delle Marche

P.zza Roma 22, 60121 Ancona
Tel (+39) 071.220.1, Fax (+39) 071.220.2324
P.I. 00382520427