114 research outputs found
A P2P-based Infrastructure for Virtual-Enterprise ́s Supply-Chain Management
No full textThis paper proposes and describes a prototype of a peer-to-peer based infrastructure to support virtual enterprise’s supply chain management. Because of a virtual enterprise is composed of autonomous, distributed, and continuously evolving entities, we have naturally modelled each business entity like a peer’s agent platform that can play several roles according to the task to be fulfilled. To this end, we describe and apply such roles, required to the organizational architecture, into a virtual storehouse scenari
Verification-as-a-Service for Parameter Assessment
No full textWhen 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
Intelligent Planning: A Decomposition and Abstraction Based Approach
No full textThis is a review of the book `Intelligent Planning: A Decomposition and Abstraction Based Approach` by Qiang Yang [Yang, 1997], a book focused on classical planning. Why classical planning? In the last years, the classical approach to planning has been challenged by many authors (e.g. [Agree and Chapman, 1987; Agree and Chapman, 1989; Brooks, 1991; Chapman, 1989; Georgeff, 1991; Ginsberg, 1989]). The question is whether its fundamental assumptions and complexity make it of any use in real world applications. The opponents of classical planning (e.g., reactive planning [Brooks, 1986; Kaelbling, 1987]) are important in a number of domains. Nevertheless, in our opinion, there are applications where classical planning is still the only reasonable approach, e.g. logistics, process planning, scheduling. Furthermore, in the last years, many new approaches have been proposed which are elaborations of classical planning, e.g., case-based planning [Hammond, 1990b; Hanks and Weld, 1995; Ihrig and Kambhampati, 1997; Koehler, 1996; Veloto et al., 1996], multi-agent planning [Durfee, 1988, Genesereth and Ketchpel, 1994; Jenning and Wooldridge, 1998], non-STRIPS style planning [Blum and Furst, 1995; Kautz and Selman, 1996], and model checking based planning [Cimatti et al., 1997]. Yang`s book provides a set of basic techniques for generating plans and a set of formal and empirical tools for evaluating and comparing them. The book is divided in three parts. The first part is devoted to the fundamentals of planning. Its title is Representation, Basic, Algorithms, and Analytical Techniques. The second describes the `divide et impera` approach and is titled Problem Decomposition and Solution Combination. The third is a titled Hierarchical Abstraction and it is devoted to the use of abstraction in plannin
Parameterized model checking of networks of timed automata with Boolean guards
No full textParameterized 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
High-Performance Computing for Formal Security Assessment
No full textAssessing 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
An offline parallel architecture for forensic multimedia classification
No full textNowadays, the volume of the multimedia heterogeneous evidence presented for digital forensic analysis has significantly increased, thus requiring the application of big data technologies, cloud-based forensics services, as well as Machine Learning (ML) techniques. In digital forensics domain, ML algorithms have been applied for cybercrime investigation such as child abuse investigations, malware classification, and image forensics. This paper addresses this issues and deals with forensic analysis of digital images and videos. In particular, this work aims at proposing a multimedia classification tool with a parallel software architecture for a fast inspection, which is easy to use (to be used by officers during a search), requires limited hardware resources and it is built on an open-source software to limit its costs. Moreover, this tool must be able to quickly inspect multiple devices at a time. When positives are found in a device, such device will be seized for a deeper analysis later in the lab. It will not be seized otherwise, reducing the inconvenience for the suspect as well as the time required for the next analysis phase. As a case study, we focus on the identification of child pornography images. Experimental results show that the proposed architecture is capable of guaranteeing a high recall, a fast process and high performances in real scenarios
- …
