Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2013 | Book

Cost-Aware Runtime Enforcement of Security Policies Read chapter Read first chapter

Security and Trust Management

8th International Workshop, STM 2012, Pisa, Italy, September 13-14, 2012, Revised Selected Papers

Editors: Audun Jøsang, Pierangela Samarati, Marinella Petrocchi

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the thoroughly refereed post-conference proceedings of the 8th International Workshop on Security and Trust Management, STM 2012, held in Pisa, Italy, in September 2012 - in conjunction with the 17th European Symposium Research in Computer Security (ESORICS 2012). The 20 revised full papers were carefully reviewed and selected from 57 submissions. The papers are organized into topical sections on policy enforcement and monitoring; access control; trust, reputation, and privacy; distributed systems and physical security; authentication and security policies.

Table of Contents

Frontmatter

Policy Enforcement and Monitoring

Cost-Aware Runtime Enforcement of Security Policies
Abstract
In runtime enforcement of security policies, the classic requirements on monitors in order to enforce a security policy are soundness and transparency. However, there are many monitors that successfully pass this specification but they differ in complexity of both their implementation and the output they produce. In order to distinguish and compare these monitors we propose to associate cost with enforcement.
We present a framework where the cost of enforcement of a trace is determined by the cost of operations the monitor uses to edit the trace. We explore cost-based order relations on sound monitors. We investigate cost-optimality of monitors which allows considering the most cost-efficient monitors that soundly enforce a property.
Peter Drábik, Fabio Martinelli, Charles Morisset
Enforcing More with Less: Formalizing Target-Aware Run-Time Monitors
Abstract
Run-time monitors ensure that untrusted software and system behavior adheres to a security policy. This paper defines an expressive formal framework, based on I/O automata, for modeling systems, policies, and run-time monitors in more detail than is typical. We explicitly model, for example, the environment, applications, and the interaction between them and monitors. The fidelity afforded by this framework allows us to explicitly formulate and study practical constraints on policy enforcement that were often only implicit in previous models, providing a more accurate view of what can be enforced by monitoring in practice. We introduce two definitions of enforcement, target-specific and generalized, that allow us to reason about practical monitoring scenarios. Finally, we provide some meta-theoretical comparison of these definitions and we apply them to investigate policy enforcement in scenarios where the monitor designer has knowledge of the target application and show how this can be exploited to make more efficient design choices.
Yannis Mallios, Lujo Bauer, Dilsun Kaynar, Jay Ligatti
Lazy Security Controllers
Abstract
Security controllers follow the execution of the target systems to prevent security violations. In fact, by proactively observing the target, they are able to catch security violations before they occur and act consequently, such as by interrupting the execution. In this paper we define a novel category of security controllers called lazy controllers, a conservative extension of standard controllers which routinely suspend the observation of the target for different time spans, in order to reduce the cost of monitoring and increase performance, at the expense of the possibility of missing a violation.
We show how a proactive truncation controller can be extended to the lazy setting, and we formally characterize the relation between the length of suspended time spans and the actual violation risk, which constitutes the formal ground of our approach. This allows the actual time of suspension to be determined according to a given maximum bearable risk. Precisely, we formally investigate three classes of systems, namely non-deterministic, probabilistic, and stochastic systems.
Giulio Caravagna, Gabriele Costa, Giovanni Pardini

Access Control

Automated Analysis of Scenario-Based Specifications of Distributed Access Control Policies with Non-mechanizable Activities
Abstract
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.
Michele Barletta, Silvio Ranise, Luca Viganò
Labeled Goal-Directed Search in Access Control Logic
Abstract
We describe a sound, complete, and terminating procedure for goal-directed proof search in \(\text{BL}_{\text{sf}}^{\textsf{G}}\), an expressive fragment of a recently presented access control logic, BLsf. \(\text{BL}_{\text{sf}}^{\textsf{G}}\) is more expressive than many other Datalog-based access control logics that also have very efficient decision procedures, and our search procedure finds proofs of authorization quickly in practice. We also extend our search procedure to find missing credentials when a requested authorization does not hold and discuss an implementation of our techniques in an extension of the Unix file synchronization program rsync.
Valerio Genovese, Deepak Garg, Daniele Rispoli
A Use-Based Approach for Enhancing UCON
Abstract
The security related characteristics of entities, the contextual information that describes them and the previous or concurrent usages exercised in the system are the criteria that the Usage CONtrol (UCON) family of models utilizes in the usage decision process. In this paper, a detailed classification of the aforementioned criteria along with a representative usage scenario for each category is presented, unveiling a number of UCON’s limitations. In turn, a Use-based Usage CONtrol (UseCON) model is proposed that provides, for the creation of a usage decision, enhanced handling of information regarding context and previous or current usages exercised in the system. The enhanced capabilities of the proposed approach are demonstrated and discussed with the use of detailed application examples.
Christos Grompanopoulos, Antonios Gouglidis, Ioannis Mavridis
Analysis of Communicating Authorization Policies
Abstract
We present a formal language for specifying distributed authorization policies that communicate through insecure asynchronous media. The language allows us to write declarative authorization policies; the interface between policy decisions and communication events can be specified using guards and policy updates. The attacker, who controls the communication media, is modeled as a message deduction engine. We give trace semantics to communicating authorization policies, and formulate a generic reachability problem. We show that the reachability problem is decidable for a large class of practically-relevant policies specified in our formal language.
Simone Frau, Mohammad Torabi Dashti

Trust, Reputation, and Privacy

Building Trust and Reputation In: A Development Framework for Trust Models Implementation
Abstract
During the last years, many trust and reputation models have been proposed, each one targeting different contexts and purposes, and with their own particularities. While most contributions focus on defining ever-increasing complex models, little attention has been paid to the process of building these models inside applications during their implementation. The result is that models have traditionally considered as ad-hoc and after-the-fact solutions that do not always fit with the design of the application. To overcome this, we propose an object-oriented development framework onto which it is possible to build applications that require functionalities provided by trust and reputation models. The framework is extensible and flexible enough to allow implementing an important variety of trust models. This paper presents the framework, describes its main components, and gives examples on how to use it in order to implement three different trust models.
Francisco Moyano, Carmen Fernandez-Gago, Javier Lopez
Matrix Powers Algorithms for Trust Evaluation in Public-Key Infrastructures
Abstract
This paper deals with the evaluation of trust in public-key infrastructures. Different trust models have been proposed to interconnect the various PKI components in order to propagate the trust between them. In this paper we provide a new polynomial algorithm using linear algebra to assess trust relationships in a network using different trust evaluation schemes. The advantages are twofold: first the use of matrix computations instead of graph algorithms provides an optimized computational solution; second, our algorithm can be used for generic graphs, even in the presence of cycles. Our algorithm is designed to evaluate the trust using all existing (finite) trust paths between entities as a preliminary to any exchanges between PKIs. This can give a precise evaluation of trust, and accelerate for instance cross-certificate validation.
Jean-Guillaume Dumas, Hicham Hossayni
Formal Modelling of (De)Pseudonymisation: A Case Study in Health Care Privacy
Abstract
In recent years, a number of infrastructures have been proposed for the collection and distribution of medical data for research purposes. The design of such infrastructures is challenging: on the one hand, they should link patient data collected from different hospitals; on the other hand, they can only use anonymised data because of privacy regulations. In addition, they should allow data depseudonymisation in case research results provide information relevant for patients’ health. The privacy analysis of such infrastructures can be seen as a problem of data minimisation. In this work, we introduce coalition graphs, a graphical representation of knowledge of personal information to study data minimisation. We show how this representation allows identification of privacy issues in existing infrastructures. To validate our approach, we use coalition graphs to formally analyse data minimisation in two (de)-pseudonymisation infrastructures proposed by the Parelsnoer initiative.
Meilof Veeningen, Benne de Weger, Nicola Zannone

Distributed Systems and Physical Security

Switchwall: Automated Topology Fingerprinting and Behavior Deviation Identification
Abstract
The continuous improvement of bandwidth, pervasiveness, and functionality of network switching technologies is deeply changing the Internet landscape. Indeed, it has become tedious and sometimes infeasible to manually assure the network integrity on a regular basis: existing hardware and software can be tampered with and new devices can be connected or become nonoperational without any notification. Moreover, changes in the network topology can be introduced by human error, by hardware or software failures, or even by a malicious adversary (e.g. rogue systems).
In this paper, we introduce Switchwall, an Ethernet-based network fingerprinting technique that detects unauthorized changes to the L2/L3 network topology, the active devices, and the availability of an Enterprise network. The network map is generated at an initial known state and is then periodically verified to detect deviations in a fully automated manner. Switchwall leverages a single vantage point and uses only very common protocols (PING and ARP) without any requirements for new software or hardware. Moreover, no previous knowledge of the topology is required, and our approach works on mixed speed, mixed vendors networks. Switchwall is able to identify a wide-range of changes which are validated by our experimental results on both real and simulated networks.
Nelson Nazzicari, Javier Almillategui, Angelos Stavrou, Sushil Jajodia
DOT-COM: Decentralized Online Trading and COMmerce
Abstract
Current financial markets rely on direct trust between trading parties or a common trusted third party (TTP). The Internet enables practically any two possible traders around the world to locate each other, but payments and trading mechanisms are still centralized, inefficient, and require direct trust or trusted intermediaries. We present DOT-COM, a financial trading protocol that supports trades between any trading parties, even when no trust or common TTP exist between them. The proposed system makes sure that the traded financial products are exchanged by both sides while ensuring that neither side is exposed to fraud, default or settlement risks. Trade execution is carried out within a predefined time frame, and may be subject to arbitrary conditions defined by the traders. DOT-COM design allows such trades to be conducted over the Internet, automatically, efficiently, securely and cheaply.
Moti Geva, Amir Herzberg
Formalizing Physical Security Procedures
Abstract
Although the problems of physical security emerged more than 10,000 years before the problems of computer security, no formal methods have been developed for them, and the solutions have been evolving slowly, mostly through social procedures. But as the traffic on physical and social networks is now increasingly expedited by computers, the problems of physical and social security are becoming technical problems. From various directions, many security researchers and practitioners have come to a realization that the areas such as transportation security, public and private space protection, or critical infrastructure defense, are in need of formalized engineering methodologies. Following this lead, we extended Protocol Derivation Logic (PDL) to Procedure Derivation Logic (still PDL). In contrast with a protocol, where some principals send and receive some messages, in a procedure they can also exchange and move some objects. For simplicity, in the present paper we actually focus on the security issues arising from traffic of objects, and leave the data flows, and the phenomena emerging from the interaction of data and objects, for future work. We illustrate our approach by applying it to a flawed airport security procedure described by Schneier.
Catherine Meadows, Dusko Pavlovic

Authentication

A PUF-Based Authentication Protocol to Address Ticket-Switching of RFID-Tagged Items
Abstract
Ticket-switching incidents where customers switch the price tag or bar code in order to pay a lower amount for their ‘purchased item’ is not uncommon in retail stores. Since the item has to pass through a check-out counter before leaving the store, it has a (even if miniscule) positive probability of being identified. However, when item-level RFID tags are used in an automated check-out environment, the probability of such incidents coming to light is estimated to be almost zero. We propose an authentication protocol for this scenario using a pair of item-level RFID tags, one of which is PUF-enabled to resist cloning attacks.
Sjouke Mauw, Selwyn Piramuthu
Authenticating Email Search Results
Abstract
Alice uses a web mail service and searches through her emails by keywords and dates. How can Alice be sure that search results she gets contain all the relevant emails she received in the past? We consider this problem and provide a solution where Alice sends to the server authentication information for every new email. In response to a query, the server augments the results with a cryptographic proof computed using the authentication information. Alice uses the proof and a locally-stored cryptographic digest to verify the correctness of the result. Our method adds a small overhead to the usual interaction between the email client and server.
Olga Ohrimenko, Hobart Reynolds, Roberto Tamassia
Software Authentication to Enhance Trust in Body Sensor Networks
Abstract
This paper studies an approach to enhance the trust in the widespread use of Body Sensor Networks (BSN) in Healthcare. To address the wide variety in medical indications and differences between patients, we assume that such BSNs are programmable and highly flexible in their functionality. Yet this opens a vulnerability to malicious attacks and intrusion of the patient’s privacy. We study the work flow in a typical medical scenario, we map the (implied or evidence-based) trust relations and we use this to propose a scheme for verifying the authenticity and trustworthiness without prohibitively interfering with common practices. Our proposed framework is currently being refined in the VITRUVIUS project, for instance to test the feasibility of its implementation.
Joep de Groot, Vinh Bui, Jean-Paul Linnartz, Johan Lukkien, Richard Verhoeven
YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM
Abstract
The Yubikey is a small hardware device designed to authenticate a user against network-based services. Despite its widespread adoption (over a million devices have been shipped by Yubico to more than 20 000 customers including Google and Microsoft), the Yubikey protocols have received relatively little security analysis in the academic literature. In the first part of this paper, we give a formal model for the operation of the Yubikey one-time password (OTP) protocol. We prove security properties of the protocol for an unbounded number of fresh OTPs using a protocol analysis tool, tamarin.
In the second part of the paper, we analyze the security of the protocol with respect to an adversary that has temporary access to the authentication server. To address this scenario, Yubico offers a small Hardware Security Module (HSM) called the YubiHSM, intended to protect keys even in the event of server compromise. We show if the same YubiHSM configuration is used both to set up Yubikeys and run the authentication protocol, then there is inevitably an attack that leaks all of the keys to the attacker. Our discovery of this attack lead to a Yubico security advisory in February 2012. For the case where separate servers are used for the two tasks, we give a configuration for which we can show using the same verification tool that if an adversary that can compromise the server running the Yubikey-protocol, but not the server used to set up new Yubikeys, then he cannot obtain the keys used to produce one-time passwords.
Robert Künnemann, Graham Steel

Security Policies

Boosting Model Checking to Analyse Large ARBAC Policies
Abstract
The administration of access control policies is a task of paramount importance for distributed systems. A crucial analysis problem is to foresee if a set of administrators can give a user an access permission. We consider this analysis problem in the context of the Administrative Role-Based Access Control (ARBAC), one of the most widespread administrative models. Given the difficulty of taking into account the effect of all possible administrative actions, automated analysis techniques are needed. In this paper, we describe how a model checker can scale up to handle very large ARBAC policies while ensuring completeness. An extensive experimentation shows that an implementation of our techniques performs significantly better than Mohawk, a recently proposed tool that has become the reference for finding errors in ARBAC policies.
Silvio Ranise, Anh Truong, Alessandro Armando
Constrained Role Mining
Abstract
Role Based Access Control (RBAC) is a very popular access control model, for a long time investigated and widely deployed in the security architecture of different enterprises. To implement RBAC, roles have to be firstly identified within the considered organization. Usually the process of (automatically) defining the roles in a bottom up way, starting from the permissions assigned to each user, is called role mining. In literature, the role mining problem has been formally analyzed and several techniques have been proposed in order to obtain a set of valid roles.
Recently, the problem of defining different kind of constraints on the number and the size of the roles included in the resulting role set has been addressed. In this paper we provide a formal definition of the role mining problem under the cardinality constraint, i.e. restricting the maximum number of permissions that can be included in a role. We discuss formally the computational complexity of the problem and propose a novel heuristic. Furthermore we present experimental results obtained after the application of the proposed heuristic on both real and synthetic datasets, and compare the resulting performance to previous proposals.
Carlo Blundo, Stelvio Cimato
A Datalog Semantics for Paralocks
Abstract
Broberg and Sands (POPL’10) introduced a logic-based policy language, Paralocks, suitable for static information-flow control in programs. Although Paralocks comes with a precise information-flow semantics for programs, the logic-based semantics of policies, describing how policies are combined and compared, is less well developed. This makes the algorithms for policy comparison and computation ad-hoc, and their security guarantees less intuitive. In this paper we provide a new semantics for Paralocks policies based on Datalog. By doing so we are able to show that the ad-hoc semantics from earlier work coincides with the natural Datalog interpretation. Furthermore we show that by having a Datalog-inspired semantics, we can borrow language extensions and algorithms from Datalog for the benefit of Paralocks. We explore how these extensions and algorithms interact with the design and implementation of Paragon, a language combining Paralocks with Java.
Bart van Delft, Niklas Broberg, David Sands
Backmatter
Metadata
Title
Security and Trust Management
Editors
Audun Jøsang
Pierangela Samarati
Marinella Petrocchi
Copyright Year
2013
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-38004-4
Print ISBN
978-3-642-38003-7
DOI
https://doi.org/10.1007/978-3-642-38004-4

Premium Partner

    Image Credits