Search

In the security protocols domain, formal verification is more and more highly demanded to guarantee security assurance: humans increasingly depend on the use of connected devices in their daily life, so they must be protected against possible threats and accidents. However, formal verification, and in general the use of formal methods, is slowed by myths and misconceptions, mainly due to their mathematical base, which discourages many designers or engineers from their adoption.

Cyber ranges are virtual environments used in several contexts to enhance the awareness and preparedness of users to cybersecurity threats. Effectiveness of cyber ranges strongly depends on how much realistic are the training scenarios provided to trainees and on an efficient mechanism to monitor and evaluate trainees’ activities.

Cyber ranges for training in threat scenarios are nowadays highly demanded in order to improve people ability to detect vulnerabilities and to react to cyber-threats. Among the other components, scenarios deployment requires a modeling language to express the (software and hardware) architecture of the underlying system, and an emulation platform.

In this paper, we developed an online auction system based on Ethereum smart contracts. A smart contract is executable code that runs on top of the blockchain to facilitate, execute and enforce an agreement between untrusted parties without the involvement of a trusted third party. A decentralised auction guarantees greater transparency and avoids cheating auctioneers. Since in Ethereum computation is expensive as transactions are executed and verified by all the nodes on Ethereum network, we analysed our implementation in terms of cost and time efficiency, obtaining promising results.

Electronic voting is one of the most challenging cryptographic problems, since the developed system should guarantee strong and sometimes contrasting security properties. Blockchain technology can be of help providing for free some important guarantees such as the immutability and transparency of the votes using a distributed ledger. In this paper we propose a blockchain based e-voting system, which is lightweight, since it does not rely on strong cryptographic primitives, and efficient, since it improves over previous proposals in terms of both execution time and associated cost for the required infrastructure. We provide the description of a proof of concept system together with the cost and performance analysis.

mHealth applications are becoming increasingly widespread since they have the potential to reduce the cost of health care by favoring self-management of chronic diseases or to improve fitness activities. By their very nature, health applications collect and manage health sensitive data, therefore several concerns exist about how privacy, security, and confidentiality are handled. In this paper, we analyze the security issues of mHealth apps from two different perspectives: first, we highlight the security and privacy requirements on health data defined by data protection laws such as the General Data Protection Regulation (GDPR) in the EU, or the Health Insurance Portability and Accountability Act (HIPAA) in US. Then, we consider the security issues from a technological point of view, discussing how the app may protect user data. However, by analyzing a fitness app, we show that, at the moment, none of the well-known practices to protect data is followed, thus often mHealth apps are insecure.

After the NSA surveillance revelations in 2013, people became aware of the lack of privacy with respect to the US government. But are users aware that also apps may spy them, collect and even sell their personal data? From their common behavior during their always-connected every day life, it does not seem so: many people use apps that collect and send their browsing habits to third-parties. An example is the Pokemon GO app, a game that in a few months became a worldwide phenomenon, that in its Privacy policy clearly states that the user allows the app to access his emails, address book, location and other very private personal info. In this work, we examined consumers' attitudes and perceptions regarding their privacy by conducting a survey on 208 participants diverse in age, gender and education. Findings suggest that consumers have very low awareness on privacy issues, and that, when downloading apps, they often fail to read the privacy policy, where it is stated who will gather access to their data and which data will be collected by the app.

Privacy has often gained the headlines on the media in the last few years, due to the revelation of appalling invasions of what many citizens perceive as the private space of their own communications, behavior, and lifestyle. Privacy is especially in the spotlight when the online dimension is concerned with the almost endless stream of personal information that travels on the Internet. However, the apparent importance that online privacy has gained in the public discourse should not be taken as a demonstration that privacy problems are going to be solved any time soon. Furthermore, it could not be even taken as a proof of maturity in the comprehension of the problems. In fact, many privacy problems are becoming more intractable now in the modern online ecosystem than decades ago, when privacy emerged as a problem of industrialized societies. Online privacy is enmeshed with the dynamics of technology innovations, and with the shape of today's IT market, it is also entangled with the often fragile economics of the online advertising sector. At present, privacy depends to customers bounded rationality and, to put it simple, to the fact that for an individual, to manage her own online privacy specifically and timely without sacrificing to reap the benefits of the online ecosystem would be just overwhelming in the current setting. In this chapter, we discuss some particularly critical factors contributing to the problem of managing today's online privacy, followed by an introduction to some technical issues. In particular, we present in more details the case of the data broker industry, rather than the much more publicized cases of governmental surveillance and Internet-based data-centric corporations, because of its relatively lesser media exposition combined with an indisputable relevance for citizens' privacy. The problem of the informed consent and the dubbed privacy control paradox is discussed too for its centrality in almost all privacy policies and still underrated weakness. This leads us to show the complex and multidimensional nature of online privacy and the implication on policy making. In the section on privacy and technologies, we address the problem of online privacy both at the application level—by describing the current techniques used to collect a user's browsing history—and at the communication level—by discussing the methods available to defend against traffic analysis. Then, we highlight the security and privacy issues of mobile health applications.

This article describes an approach for the automated verification of mobile systems. Mobile systems are characterized by the explicit notion oflocation(e.g., sites where they run) and the ability to execute at different locations, yielding a number of security issues. To this aim, we formalize mobile systems as Labeled Kripke Structures, encapsulating the notion oflocation netthat describes the hierarchical nesting of the threads constituting the system. Then, we formalize a genericsecurity-policy specification languagethat includes rules for expressing and manipulating the code location. In contrast to many other approaches, our technique supports both access control and information flow specification. We developed a prototype framework for model checking of mobile systems. It works directly on the program code (in contrast to most traditional process-algebraic approaches that can model only limited details of mobile systems) and uses abstraction-refinement techniques, based also on location abstractions, to manage the program state space. We experimented with a number of mobile code benchmarks by verifying various security policies. The experimental results demonstrate the validity of the proposed mobile system modeling and policy specification formalisms and highlight the advantages of the model checking-based approach, which combines the validation of security properties with other checks, such as the validation of buffer overflows.

A variant of the Mobile Ambient calculus, called Boundary Ambients, is introduced, supporting the modelling of multi-level security policies. Ambients that may guarantee to properly protect their content are explicitly identified as boundaries: a boundary can be seen as a resource access manager for confidential data. In this setting, absence of direct information leakage is granted as soon as the initial process satisfies some syntactic conditions. We then give a new notion of non-interference for Boundary Ambients aiming at capturing indirect flows, too. We design a Control Flow Analysis that computes an over-approximation of all ambients that may be affected at run-time by high-level data and we show that this static analysis can be used to enforce non-interference, i.e., to statically detect that no (direct or indirect) information leakage is ever possible at run-time.

Role-based access control (RBAC) is increasingly attracting attention because it reduces the complexity and cost of security administration by interposing the notion of role in the assignment of permissions to users. In this paper, we present a formal framework relying on an extension of the $\pi$-calculus to study the behaviour of concurrent systems in a RBAC scenario. We define a type system ensuring that the specified policy is respected during computations, and a behavioural equivalence to equate systems. We then consider a more sophisticated feature that can be easily integrated in our framework, i.e., the possibility of automatically adding role activations and deactivations to processes to be run under a given policy (whenever possible). Finally, we show how the framework can be easily extended to express significant extensions of the core RBAC model, such as roles hierarchies or constraints determining the acceptability of the system components.

In this paper, we present a refinement of a Control Flow Analysis aimed at studying information flow security in the the calculus of Mobile Ambients. The improvements are achieved by making the analysis be flow-sensitive: the analysis is able to keep track of temporal dependencies of capabilities application when computing a safe approximation of the run-time topology of Mobile Ambient processes.

We consider two different approaches to security issues. In the first one bisimulation equivalences (dynamic verifications) are exploited to verify non-interference security properties on a CCS-like process algebra calculus. In the second approach control flow analysis (static analysis) is applied to verify security properties in Mobile Ambient calculus. We analyze how a simple electronic commerce case study can be modeled and its integrity verified using the two techniques. The tools CoPS and Banana are used to perform the computations.

A variant of Mobile Ambient Calculus is introduced, called Boundary Ambient, to model multilevel security policies. Ambients that may guarantee to properly protect their content are explicitly identified as boundaries : a boundary can be seen as a resource access manager for confidential data. In this setting, we define a notion of non-interference which captures the absence of any (both direct and indirect) information leakage. Then, we guarantee non-interference by extending a control flow analysis that computes an over approximation of all ambients and capabilities that may be affected by the actual values of high level data.

In recent years, large-scale computer networks have become an essential aspect of our daily computing environment. We often rely on a global information infrastructure for ebusiness activities such as home banking, ATM transactions, or shopping online. One of the main scientific and technological challenges in this setting has been to provide security to individuals who operate in possibly untrusted and unknown environments. However, beside threats directly related to computer intrusions, epidemic diffusion of malwares, and outright frauds conducted online, a more subtle though increasing erosion of individuals’ privacy has progressed and multiplied. Such an escalating violation of privacy has some direct harmful consequences—for example, identity theft has spread in recent years—and negative effects on the general perception of insecurity that many individuals now experience when dealing with online services. Nevertheless, protecting personal privacy from the many parties—business, government, social, or even criminal—that examine the value of personal information is an old concern of modern society, now increased by the features of the digital infrastructure. In this chapter, we address these privacy issues in the digital society from different points of view, investigating: The various aspects of the notion of privacy and the debate that the intricate essence of privacy has stimulated; the most common privacy threats and the possible economic aspects that may influence the way privacy is (and especially is not, in its current status) managed in most firms; the efforts in the computer science community to face privacy threats, especially in the context of distributed networks; and, the network-based technologies available to date to provide anonymity in user communications over a private network.

The binary perfect phylogeny model is too restrictive to model biological events such as back mutations. In this paper we consider a natural generalization of the model that allows a special type of back mutation. We investigate the problem of reconstructing a near perfect phylogeny over a binary set of characters where characters are persistent: characters can be gained and lost at most once. Based on this notion, we define the problem of the Persistent Perfect Phylogeny (referred as P-PP). We restate the P-PP problem as a special case of the Incomplete Directed Perfect Phylogeny, called Incomplete Perfect Phylogeny with Persistent Completion, (refereed as IP-PP), where the instance is an incomplete binary matrix M having some missing entries, denoted by symbol ?, that must be determined (or completed) as 0 or 1 so that M admits a binary perfect phylogeny. We show that the IP-PP problem can be reduced to a problem over an edge colored graph since the completion of each column of the input matrix can be represented by a graph operation. Based on this graph formulation, we develop an exact algorithm for solving the P-PP problem that is exponential in the number of characters and polynomial in the number of species., Comment: 13 pages, 3 figures

Objectives Ovarian cancer is the fourth leading cause of death among neoplastic diseases in women. In spite of constant improvement in surgical, chemotherapeutic and immunologic techniques, which can induce long remission periods, the five-year survival rate has not really changed over the past thirty years. We tried to create a sonographic scoring system, called PMS, that could be helpful in diagnosis of pelvic masses. Study design The three most commonly used and validated indexes – Sassone score, Ovarian Tumor Index (OTI), and Risk of Malignancy Index 3 (RMI3) – were applied to a population of 102 women with adnexal masses. We developed a new scoring system, named Pelvic Masses Score (PMS), that takes into account the ultrasound morphological pattern, the Doppler flowmetry of the pelvic mass, the CA125 serum level and the menopausal status. We then applied this scoring system to a population of 160 women for validation of the score. Results Statistical analysis of the data obtained from the new scoring system reveals that sensitivity, specificity, positive and negative predictive values (PPV and NPV) are higher than in the case of data separately derived from the Sassone score, OTI index or RMI index. Conclusions Our preliminary data showed good results in term of sensivity, specify and predictive values compared to other old scoring systems. A larger prospective study is required to confirm these preliminary data. The number of cases will be expanded to permit a better evaluation of PMS.

To evaluate the efficacy and safety of the minimally invasive Ajust™ system in the treatment of stress urinary incontinence. This was a prospective multicentre study. All patients with primary urodynamic stress urinary incontinence were prospectively selected to receive the Ajust™ procedure. The International Consultation on Incontinence-Short Form (ICI-SF), Women Irritative Prostate Symptoms Score (W-IPSS), PGI-S, and PGI-I questionnaires were used to evaluate the impact of incontinence and voiding dysfunction on QoL and to measure patient's perception of incontinence severity and improvement. From January 2009 to October 2009, 111 consecutive subjects were enrolled in the study. At 6 months, 102 were available for outcomes analysis. The subjective and objective cure rates were 85.7% and 91.4%, respectively. The ICI-SF and W-IPSS questionnaires showed a statistical significant improvement in symptom scores. In the short-term follow-up, the Ajust™ system was effective in restoring continence in more than 85% of subjects with a highly significant improvement in QoL.

Publisher Summary This chapter discusses net privacy from different viewpoints, from historical to technological. The very nature of the concept of privacy requires such an enlarged perspective because it often appears indefinite, being constrained into the tradeoff between the undeniable need of protecting personal information and the evident utility, in many contexts, of the availability of the same information. The digital society and the global interconnected infrastructure eased accessing and spreading of personal information; therefore, developing technical means and defining norms and fair usage procedures for privacy protection are now more demanding than in the past. This chapter also presents some of the more advanced solutions that research has developed to date, either for anonymizing stored data, hiding sensitive information in artificially inaccurate clusters, or introducing third parties and middleware in charge of managing online transactions and services in a privacy-aware fashion. Location privacy is a topic that has gained importance in recent years with the advent of mobile devices. Privacy over the Net and in the digital society does not look to be in good shape; the augmented sensibility of individuals to its erosion, the many scientific and technological efforts to introduce novel solutions, and a better knowledge of the problem with the help of fresh data contribute to stimulating the need for better protection and fairer use of personal information.