Skip to main content

Über dieses Buch

This book constitutes the refereed proceedings of the 7th International Symposium on Engineering Secure Software and Systems, ESSoS 2015, held in Milan, Italy, in March 2015. The 11 full papers presented together with 5 short papers were carefully reviewed and selected from 41 submissions. The symposium features the following topics: formal methods; cloud passwords; machine learning; measurements ontologies; and access control.



Formal Methods

Formal Verification of Liferay RBAC

Liferay is the leading opensource portal for the enterprise, implementing a role-based access control (RBAC) mechanism for user and content management. Despite its critical importance, however, the access control system implemented in Liferay is poorly documented and lacks automated tools to assist portal administrators in configuring it correctly. To make matters worse, although strongly based on the RBAC model and named around it, the access control mechanism implemented in Liferay has a number of unconventional features, which significantly complicate verification. In this paper we introduce a formal semantics for Liferay RBAC and we propose a verification technique based on abstract model-checking, discussing sufficient conditions for the soundness and the completeness of the analysis. We then present a tool, called LifeRBAC, which implements our theory to verify the security of real Liferay portals. We show that the tool is effective at proving the absence of security flaws, while efficient enough to be of practical use.
Stefano Calzavara, Alvise Rabitti, Michele Bugliesi

Formal Verification of Privacy Properties in Electric Vehicle Charging

Electric vehicles are an up-and-coming technology that provides significant environmental benefits. A major challenge of these vehicles is their somewhat limited range, requiring the deployment of many charging stations. To effectively deliver electricity to vehicles and guarantee payment, a protocol was developed as part of the ISO 15118 standardization effort. A privacy-preserving variant of this protocol, POPCORN, has been proposed in recent work, claiming to provide significant privacy for the user, while maintaining functionality. In this paper, we outline our approach for the verification of privacy properties of the protocol. We provide a formal model of the expected privacy properties in the applied Pi-Calculus and use ProVerif to check them. We identify weaknesses in the protocol and suggest improvements to address them.
Marouane Fazouane, Henning Kopp, Rens W. van der Heijden, Daniel Le Métayer, Frank Kargl

Idea: Unwinding Based Model-Checking and Testing for Non-Interference on EFSMs

Undesired flows of information between different sensitivity levels or domains can seriously compromise the security of a system. Moreover, even if specifications are secure, unwanted flows can still be present in implementations. In this paper we present a model-based technique to discover unwanted information flows in specifications and to test systems for unwanted flows. We base our approach on an unwinding relation for Extended Finite State Machines. We preliminary validate our approach by means of an implementation that allows us to benchmark the efficiency of our model-checking algorithm.
Martín Ochoa, Jorge Cuéllar, Alexander Pretschner, Per Hallgren

Idea: State-Continuous Transfer of State in Protected-Module Architectures

The ability to copy data effortlessly poses significant security issues in many applications; It is difficult to safely lend out music or e-books, virtual credits cannot be transferred between peers without contacting a central server or co-operation with other network nodes, …
Protecting digital copies is hard because of the huge software and hardware trusted computing base applications have to rely on. Protected-module architectures (PMAs) provide an interesting alternative by relying only on a minimal set of security primitives. Recently it has been proven that such platforms can provide strong security guarantees. However, transferring state of protected modules has, to the best of our knowledge, not yet been studied.
In this paper, we present a protocol to transfer protected modules from one machine to another state-continuously; From a high level point of view, only a single instance of the module exists that executes without interruption when it is transferred from one machine to another. In practice however an attacker may (i) crash the system at any point in time (i.e., a crash attack), (ii) present the system with a stale state (i.e., a rollback attack), or (iii) trick both machines to continue execution of the module (i.e., a forking attack). We also discuss use cases of such a system that go well beyond digital rights management.
Raoul Strackx, Niels Lambrigts

Machine Learning

Are Your Training Datasets Yet Relevant?

An Investigation into the Importance of Timeline in Machine Learning-Based Malware Detection
In this paper, we consider the relevance of timeline in the construction of datasets, to highlight its impact on the performance of a machine learning-based malware detection scheme. Typically, we show that simply picking a random set of known malware to train a malware detector, as it is done in many assessment scenarios from the literature, yields significantly biased results. In the process of assessing the extent of this impact through various experiments, we were also able to confirm a number of intuitive assumptions about Android malware. For instance, we discuss the existence of Android malware lineages and how they could impact the performance of malware detection in the wild.
Kevin Allix, Tegawendé F. Bissyandé, Jacques Klein, Yves Le Traon

Learning How to Prevent Return-Oriented Programming Efficiently

Return-oriented programming (ROP) is the most dangerous and most widely used technique to exploit software vulnerabilities. However, the solutions proposed in research often lack viability for real-life deployment.
In this paper, we take a novel, statistical approach on detecting ROP programs. Our approach is based on the observation that ROP programs, when executed, produce different micro-architectural events than ordinary programs produced by compilers. Therefore, special registers of modern processors (hardware performance counters) that track these events can be leveraged to detect ROP attacks. We use machine learning techniques to generate a model of this different behavior, and develop a kernel module that detects and prevents ROP at runtime via the learned model. Our evaluation on real-world programs and attacks shows that the runtime overhead of this technique and the number false positives are very low, while preventing all known types of ROP attacks, including recently developed evasion techniques.
David Pfaff, Sebastian Hack, Christian Hammer

Cloud and Passwords

Re-thinking Kernelized MLS Database Architectures in the Context of Cloud-Scale Data Stores

We re-evaluate the kernelized, multilevel secure (MLS) relational database design in the context of cloud-scale distributed data stores. The transactional properties and global integrity properties for schema-less, cloud-scale data stores are significantly relaxed in comparison to relational databases. This is a new and interesting setting for mandatory access control policies, and has been unexplored in prior research. We describe the design and implementation of a prototype MLS column-store following the kernelized design pattern. Our prototype is the first cloud-scale data store using an architectural approach for highassurance; it enforces a lattice-based mandatory information flow policy, without any additional trusted components.We highlight several promising avenues for practical systems research in secure, distributed architectures implementing mandatory policies using Java-based untrusted subjects.
Thuy D. Nguyen, Mark Gondree, Jean Khosalim, Cynthia Irvine

Idea: Optimising Multi-Cloud Deployments with Security Controls as Constraints

The increasing number of cloud service providers (CSP) is creating opportunities for multi-cloud deployments, where components are deployed across different CSP, instead of within a single CSP. Selecting the right set of CSP for a deployment then becomes a key step in the deployment process. This paper argues that deployment should take security into account when selecting CSP. This paper makes two contributions in this direction. First the paper describes how industrial standard security control frameworks may be integrated into the deployment process to select CSP that provide sufficient levels of security. It also argues that ability to monitor CSP security should also be considered. The paper then describes how security requirements may be modelled as constraints on deployment objectives to find optimal deployment plans. The importance of using cloud security standards as a basis for reasoning on required and provided security features is discussed.
Philippe Massonet, Jesus Luna, Alain Pannetrat, Ruben Trapero

Idea: Towards an Inverted Cloud

In this paper we propose the concept of an inverted cloud infrastructure. The traditional view of a cloud is turned upside down: instead of having services or infrastructure offered by a single provider, the same can be achieved by an aggregation of a multitude of mini providers. Even though the contribution of an individual mini provider in an inverted cloud can be limited, the combination would nevertheless be significant. We propose an architecture for an implementation of an inverted cloud infrastructure to allow mini providers to offer processor time. Security and efficiency can be achieved by building upon Intel’s new SGX technology.
Raoul Strackx, Pieter Philippaerts, Frédéric Vogels

OMEN: Faster Password Guessing Using an Ordered Markov Enumerator

Passwords are widely used for user authentication, and will likely remain in use in the foreseeable future, despite several weaknesses. One important weakness is that human-generated passwords are far from being random, which makes them susceptible to guessing attacks. Understanding the adversaries capabilities for guessing attacks is a fundamental necessity for estimating their impact and advising countermeasures.
This paper presents OMEN, a new Markov model-based password cracker that extends ideas proposed by Narayanan and Shmatikov (CCS 2005). The main novelty of our tool is that it generates password candidates according to their occurrence probabilities, i.e., it outputs most likely passwords first. As shown by our extensive experiments, OMEN significantly improves guessing speed over existing proposals.
In particular, we compare the performance of OMEN with the Markov mode of John the Ripper, which implements the password indexing function by Narayanan and Shmatikov. OMEN guesses more than 40% of passwords correctly with the first 90 million guesses, while JtR-Markov (for T = 1 billion) needs at least eight times as many guesses to reach the same goal, and OMEN guesses more than 80% of passwords correctly at 10 billion guesses, more than all probabilistic password crackers we compared against.
Markus Dürmuth, Fabian Angelstorf, Claude Castelluccia, Daniele Perito, Abdelberi Chaabane

Measurements and Ontologies

The Heavy Tails of Vulnerability Exploitation

In this paper we analyse the frequency at which vulnerabilities are exploited in the wild by relying on data collected worldwide by Symantec’s sensors. Our analysis comprises 374 exploited vulnerabilities for a total of 75.7 Million recorded attacks spanning three years (2009-2012). We find that for some software as little as 5% of exploited vulnerabilities is responsible for about 95% of the attacks against that platform. This strongly skewed distribution is consistent for all considered software categories, for which a general take-away is that less than 10% of vulnerabilities account for more than 90% of the attacks (with the exception of pre-2009 Java vulnerabilities). Following these findings, we hypothesise vulnerability exploitation may follow a Power Law distribution. Rigorous hypothesis testing results in neither accepting nor rejecting the Power Law Hypothesis, for which further data collection from the security community may be needed. Finally, we present and discuss the Law of the Work-Averse Attacker as a possible explanation for the heavy-tailed distributions we find in the data, and present examples of its effects for Apple Quicktime and Microsoft Internet Explorer vulnerabilities.
Luca Allodi

Idea: Benchmarking Indistinguishability Obfuscation – A Candidate Implementation

We present the results of preliminary experiments implementing the Candidate Indistinguishability Obfuscation algorithm recently proposed by Garg et al. [1]. We show how different parameters of the input circuits impact the performance and the size of the obfuscated programs. On the negative side, our benchmarks show that for the time being the algorithm is far away from being practical. On the positive side, there is still much room for improvement in our implementation. We discuss bottlenecks encountered and optimization possibilities. In order to foster further improvements by the community, we make our implementation public.
Sebastian Banescu, Martín Ochoa, Nils Kunze, Alexander Pretschner

A Security Ontology for Security Requirements Elicitation

Security is an important issue that needs to be taken into account at all stages of information system development, including early requirements elicitation. Early analysis of security makes it possible to predict threats and their impacts and define adequate security requirements before the system is in place. Security requirements are difficult to elicit, analyze, and manage. The fact that analysts’ knowledge about security is often tacit makes the task of security requirements elicitation even harder. Ontologies are known for being a good way to formalize knowledge. Ontologies, in particular, have been proved useful to support reusability. Requirements engineering based on predefined ontologies can make the job of requirement engineering much easier and faster. However, this very much depends on the quality of the ontology that is used. Some security ontologies for security requirements have been proposed in the literature. None of them stands out as complete. This paper presents a core and generic security ontology for security requirements engineering. Its core and generic status is attained thanks to its coverage of wide and high-level security concepts and relationships. We implemented the ontology and developed an interactive environment to facilitate the use of the ontology during the security requirements engineering process. The proposed security ontology was evaluated by checking its validity and completeness compared to other ontologies. Moreover, a controlled experiment with end-users was performed to evaluate its usability.
Amina Souag, Camille Salinesi, Raúl Mazo, Isabelle Comyn-Wattiau

Access Control

Producing Hook Placements to Enforce Expected Access Control Policies

Many security-sensitive programs manage resources on behalf of mutually distrusting clients. To control access to resources, authorization hooks are placed before operations on those resources. Manual hook placements by programmers are often incomplete or incorrect, leading to insecure programs. We advocate an approach that automatically identifies the set of locations to place authorization hooks that mediates all security-sensitive operations in order to enforce expected access control policies at deployment. However, one challenge is that programmers often want to minimize the effort of writing such policies. As a result, they may remove authorization hooks that they believe are unnecessary, but they may remove too many hooks, preventing the enforcement of some desirable access control policies.
In this paper, we propose algorithms that automatically compute a minimal authorization hook placement that satisfies constraints that describe desirable access control policies. These authorization constraints reduce the space of enforceable access control policies; i.e., those policies that can be enforced given a hook placement that satisfies the constraints. We have built a tool that implements this authorization hook placement method, demonstrating how programmers can produce authorization hooks for real-world programs and leverage policy goal-specific constraint selectors to automatically identify many authorization constraints. Our experiments show that our technique reduces manual programmer effort by as much as 58% and produces placements that reduce the amount of policy specification by as much as 30%.
Divya Muthukumaran, Nirupama Talele, Trent Jaeger, Gang Tan

Improving Reuse of Attribute-Based Access Control Policies Using Policy Templates

Access control is key to limiting the actions of users in an application and attribute-based policy languages such as XACML allow to express a wide range of access rules. As these policy languages become more widely used, policies grow both in size and complexity. Modularity and reuse are key to specifying and managing such policies effectively. Ideally, complex or domain-specific policy patterns are defined once and afterwards instantiated by security experts in their application-specific policies. However, current policy languages such as XACML provide only limited features for modularity and reuse. To address this issue, we introduce policy templates as part of a novel attribute-based policy language called STAPL. Policy templates are policies containing unbound variables that can be specified when instantiating the template in another policy later on. STAPL supports four types of policy templates with increasing complexity and expressiveness. This paper illustrates how these policy templates can be used to define reusable policy patterns and validates that policy templates are an effective means to simplify the specification of large and complex attribute-based policies.
Maarten Decat, Jasper Moeys, Bert Lagaisse, Wouter Joosen

Monitoring Database Access Constraints with an RBAC Metamodel: A Feasibility Study

Role-based access control (RBAC) is widely used in organizations for access management. While basic RBAC concepts are present in modern systems, such as operating systems or database management systems, more advanced concepts like history-based separation of duty are not. In this work, we present an approach that validates advanced organizational RBAC policies using a model-based approach against the technical realization applied within a database. This allows a security officer to examine the correct implementation – possibly across multiple applications – of more powerful policies on the database level. We achieve this by monitoring the current state of a database in a UML/OCL validation tool. We assess the applicability of the approach by a non-trivial feasibility study.
Lars Hamann, Karsten Sohr, Martin Gogolla


Weitere Informationen

Premium Partner