arXiv subjects

Luca Viganò

Publications and source records attributed to Luca Viganò.

31 records · Page 2Linked to original sources

arXiv2017

A Formal Approach to Exploiting Multi-Stage Attacks based on File-System Vulnerabilities of Web Applications (Extended Version)

Web applications require access to the file-system for many different tasks. When analyzing the security of a web application, secu- rity analysts should thus consider the impact that file-system operations have on the security of the whole application. Moreover, the analysis should take into consideration how file-system vulnerabilities might in- teract with other vulnerabilities leading an attacker to breach into the web application. In this paper, we first propose a classification of file- system vulnerabilities, and then, based on this classification, we present a formal approach that allows one to exploit file-system vulnerabilities. We give a formal representation of web applications, databases and file- systems, and show how to reason about file-system vulnerabilities. We also show how to combine file-system vulnerabilities and SQL-Injection vulnerabilities for the identification of complex, multi-stage attacks. We have developed an automatic tool that implements our approach and we show its efficiency by discussing several real-world case studies, which are witness to the fact that our tool can generate, and exploit, complex attacks that, to the best of our knowledge, no other state-of-the-art-tool for the security of web applications can find.

cs.CR↗

arXiv2017

A Formal Approach to Cyber-Physical Attacks

We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and cyber-physical attacks. We focus on %a formal treatment of both integrity and DoS attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are threefold: (1) we define a hybrid process calculus to model both CPSs and cyber-physical attacks; (2) we define a threat model of cyber-physical attacks and provide the means to assess attack tolerance/vulnerability with respect to a given attack; (3) we formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. We illustrate definitions and results by means of a non-trivial engineering application.

cs.CR↗

arXiv2016

Formal Analysis of Vulnerabilities of Web Applications Based on SQL Injection (Extended Version)

We present a formal approach that exploits attacks related to SQL Injection (SQLi) searching for security flaws in a web application. We give a formal representation of web applications and databases, and show that our formalization effectively exploits SQLi attacks. We implemented our approach in a prototype tool called SQLfast and we show its efficiency on real-world case studies, including the discovery of an attack on Joomla! that no other tool can find.

cs.CR↗

arXiv2014

Non-collaborative Attackers and How and Where to Defend Flawed Security Protocols (Extended Version)

Security protocols are often found to be flawed after their deployment. We present an approach that aims at the neutralization or mitigation of the attacks to flawed protocols: it avoids the complete dismissal of the interested protocol and allows honest agents to continue to use it until a corrected version is released. Our approach is based on the knowledge of the network topology, which we model as a graph, and on the consequent possibility of creating an interference to an ongoing attack of a Dolev-Yao attacker, by means of non-collaboration actuated by ad-hoc benign attackers that play the role of network guardians. Such guardians, positioned in strategical points of the network, have the task of monitoring the messages in transit and discovering at runtime, through particular types of inference, whether an attack is ongoing, interrupting the run of the protocol in the positive case. We study not only how but also where we can attempt to defend flawed security protocols: we investigate the different network topologies that make security protocol defense feasible and illustrate our approach by means of concrete examples.

cs.CR↗

arXiv2012

Automated Analysis of Scenario-based Specifications of Distributed Access Control Policies with Non-Mechanizable Activities (Extended Version)

The advance of web services technologies promises to have far-reaching effects on the Internet and enterprise networks allowing for greater accessibility of data. The security challenges presented by the web services approach are formidable. In particular, access control solutions should be revised to address new challenges, such as the need of using certificates for the identification of users and their attributes, human intervention in the creation or selection of the certificates, and (chains of) certificates for trust management. With all these features, it is not surprising that analyzing policies to guarantee that a sensitive resource can be accessed only by authorized users becomes very difficult. In this paper, we present an automated technique to analyze scenario-based specifications of access control policies in open and distributed systems. We illustrate our ideas on a case study arising in the e-government area.

cs.LO↗

arXiv2011

Attack Interference in Non-Collaborative Scenarios for Security Protocol Analysis [Extended Version]

In security protocol analysis, the traditional choice to consider a single Dolev-Yao attacker is supported by the fact that models with multiple collaborating Dolev-Yao attackers have been shown to be reducible to models with one Dolev-Yao attacker. In this paper, we take a fundamentally different approach and investigate the case of multiple non-collaborating attackers. After formalizing the framework for multi-attacker scenarios, we show with a case study that concurrent competitive attacks can interfere with each other. We then present a new strategy to defend security protocols, based on active exploitation of attack interference. The paper can be seen as providing two proof-of-concept results: (i) it is possible to exploit interference to mitigate protocol vulnerabilities, thus providing a form of protection to protocols; (ii) the search for defense strategies requires scenarios with at least two attackers.

cs.CR↗

arXiv2011

Meaning Negotiation as Inference

Meaning negotiation (MN) is the general process with which agents reach an agreement about the meaning of a set of terms. Artificial Intelligence scholars have dealt with the problem of MN by means of argumentations schemes, beliefs merging and information fusion operators, and ontology alignment but the proposed approaches depend upon the number of participants. In this paper, we give a general model of MN for an arbitrary number of agents, in which each participant discusses with the others her viewpoint by exhibiting it in an actual set of constraints on the meaning of the negotiated terms. We call this presentation of individual viewpoints an angle. The agents do not aim at forming a common viewpoint but, instead, at agreeing about an acceptable common angle. We analyze separately the process of MN by two agents (\emph{bilateral} or \emph{pairwise} MN) and by more than two agents (\emph{multiparty} MN), and we use game theoretic models to understand how the process develops in both cases: the models are Bargaining Game for bilateral MN and English Auction for multiparty MN. We formalize the process of reaching such an agreement by giving a deduction system that comprises of rules that are consistent and adequate for representing MN.

cs.AI↗

arXiv2010

Blocking Underhand Attacks by Hidden Coalitions (Extended Version)

Similar to what happens between humans in the real world, in open multi-agent systems distributed over the Internet, such as online social networks or wiki technologies, agents often form coalitions by agreeing to act as a whole in order to achieve certain common goals. However, agent coalitions are not always a desirable feature of a system, as malicious or corrupt agents may collaborate in order to subvert or attack the system. In this paper, we consider the problem of hidden coalitions, whose existence and the purposes they aim to achieve are not known to the system, and which carry out so-called underhand attacks. We give a first approach to hidden coalitions by introducing a deterministic method that blocks the actions of potentially dangerous agents, i.e. possibly belonging to such coalitions. We also give a non-deterministic version of this method that blocks the smallest set of potentially dangerous agents. We calculate the computational cost of our two blocking methods, and prove their soundness and completeness.

cs.CR↗

arXiv2010

Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version)

We formalize automated analysis techniques for the validation of web services specified in BPEL and a RBAC variant tailored to BPEL. The idea is to use decidable fragments of first-order logic to describe the state space of a certain class of web services and then use state-of-the-art SMT solvers to handle their reachability problems. To assess the practical viability of our approach, we have developed a prototype tool implementing our techniques and applied it to a digital contract signing service inspired by an industrial case study.

cs.CR↗

arXiv2009

A History of Until

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A until B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and w'. This "ambivalent" nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until to provide well-behaved natural deduction rules for linear-time logics by introducing a new temporal operator that allows us to formalize the "history" of until, i.e., the "internal" universal quantification over the time instants between the current one and w'. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system for a linear-time logic endowed with the new operator and show that, via a proper translation, such a system is also sound and complete with respect to the linear temporal logic LTL with until.

cs.LO↗

arXiv2009

Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version)

A widespread design approach in distributed applications based on the service-oriented paradigm, such as web-services, consists of clearly separating the enforcement of authorization policies and the workflow of the applications, so that the interplay between the policy level and the workflow level is abstracted away. While such an approach is attractive because it is quite simple and permits one to reason about crucial properties of the policies under consideration, it does not provide the right level of abstraction to specify and reason about the way the workflow may interfere with the policies, and vice versa. For example, the creation of a certificate as a side effect of a workflow operation may enable a policy rule to fire and grant access to a certain resource; without executing the operation, the policy rule should remain inactive. Similarly, policy queries may be used as guards for workflow transitions. In this paper, we present a two-level formal verification framework to overcome these problems and formally reason about the interplay of authorization policies and workflow in service-oriented architectures. This allows us to define and investigate some verification problems for SO applications and give sufficient conditions for their decidability.

cs.CR↗

arXiv2008

Labeled Natural Deduction Systems for a Family of Tense Logics

We give labeled natural deduction systems for a family of tense logics extending the basic linear tense logic Kl. We prove that our systems are sound and complete with respect to the usual Kripke semantics, and that they possess a number of useful normalization properties (in particular, derivations reduce to a normal form that enjoys a subformula property). We also discuss how to extend our systems to capture richer logics like (fragments of) LTL.

cs.LO↗

arXiv2008

A Qualitative Modal Representation of Quantum Register Transformations

We introduce two modal natural deduction systems that are suitable to represent and reason about transformations of quantum registers in an abstract, qualitative, way. Quantum registers represent quantum systems, and can be viewed as the structure of quantum data for quantum operations. Our systems provide a modal framework for reasoning about operations on quantum registers (unitary transformations and measurements), in terms of possible worlds (as abstractions of quantum registers) and accessibility relations between these worlds. We give a Kripke--style semantics that formally describes quantum register transformations and prove the soundness and completeness of our systems with respect to this semantics.

cs.LO↗