nach oben

2011 | Buch

Kapitel lesen Erstes Kapitel lesen

Engineering Secure Software and Systems

Third International Symposium, ESSoS 2011, Madrid, Spain, February 9-10, 2011. Proceedings

herausgegeben von: Úlfar Erlingsson, Roel Wieringa, Nicola Zannone

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the Third International Symposium on Engineering Secure Software and Systems, ESSoS 2011, held in Madrid, Italy, in February 2011. The 18 revised full papers presented together with 3 idea papers were carefully reviewed and selected from 63 submissions. The papers are organized in topical sections on model-based security, tools and mechanisms, Web security, security requirements engineering, and authorization.

Inhaltsverzeichnis

Frontmatter

Session 1. Model-Based Security I

Model-Based Refinement of Security Policies in Collaborative Virtual Organisations

Abstract

Policy refinement is the process of deriving low-level policies from high-level policy specifications. A basic example is that of the refinement of policies referring to users, resources and applications at a high level, such as the level of virtual organsiations, to policies referring to user ids, resource addresses and computational commands at the low level of system and network environments. This paper tackles the refinement problem by proposing an approach using model-to-model transformation techniques for transforming XACML-based VO policies to the resource level. Moreover, the transformation results in deployable policies referring to at most a single resource, hence avoiding the problem of cross-domain intereference. The applicability of our approach is demonstrated within the domain of distributed geographic map processing.

Benjamin Aziz, Alvaro E. Arenas, Michael Wilson

Automatic Conformance Checking of Role-Based Access Control Policies via Alloy

Abstract

Access control policies are a crucial aspect of many security-critical software systems. It is generally accepted that the construction of access control policies is not a straightforward task. Further, any mistakes in the process have the potential to give rise both to security risks, due to the provision of inappropriate access, and to frustration on behalf of legitimate end-users when they are prevented from performing essential tasks. In this paper we describe a tool for constructing role-based access control (RBAC) policies, which are automatically checked for conformance with constraints described using predicate logic. These constraints may represent general healthiness conditions that should hold of all policies conforming to a general model, or capture requirements pertaining to a particular deployment.

David Power, Mark Slaymaker, Andrew Simpson

Security Validation of Business Processes via Model-Checking

Abstract

More and more industrial activities are captured through Business Processes (BPs). To evaluate whether a BP under-design enjoys certain security desiderata is hardly manageable by business analysts without tool support, as the BP runtime environment is highly dynamic (e.g., task delegation). Automated reasoning techniques such as model checking can provide the required level of assurance but suffer of well-known obstacles for the adoption in industrial systems, e.g. they require a strong logical and mathematical background. In this paper, we present a novel security validation approach for BPs that employs state-of-the-art model checking techniques for evaluating security-relevant aspects of BPs in dynamic environments and offers accessible user interfaces and apprehensive feedback for business analysts so to be suitable for industry.

Wihem Arsac, Luca Compagna, Giancarlo Pellegrino, Serena Elisa Ponta

Session 2. Tools and Mechanisms

On-Device Control Flow Verification for Java Programs

Abstract

While mobile devices have become ubiquitous and generally multi-application capable, their operating systems provide few high level mechanisms to protect services offered by application vendors against potentially hostile applications coexisting on the device. In this paper, we tackle the issue of controlling application interactions including collusion in Java-based systems running on open, constrained devices such as smart cards or mobile phones. We present a model specially designed to be embedded in constrained devices to verify on-device at loading-time that interactions between applications abide by the security policies of each involved application without resulting in run-time computation overheads; this model deals with application (un)installations and policy changes in an incremental fashion. We sketch the application of our approach and its security enhancements on a multi-application use case for GlobalPlatform/Java Card smart cards.

Arnaud Fontaine, Samuel Hym, Isabelle Simplot-Ryl

Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations

Abstract

The analysis of code that uses cryptographic primitives is unfeasible with current state-of-the-art symbolic execution tools. We develop an extension that overcomes this limitation by treating certain concrete functions, like cryptographic primitives, as symbolic functions whose execution analysis is entirely avoided; their behaviour is in turn modelled formally via rewriting rules. We define concrete and symbolic semantics within a (subset) of the low-level virtual machine LLVM. We then show our approach sound by proving operational correspondence between the two semantics. We present a prototype to illustrate our approach and discuss next milestones towards the symbolic analysis of fully concurrent cryptographic protocol implementations.

Ricardo Corin, Felipe Andrés Manzano

Predictability of Enforcement

Abstract

The current theory of runtime enforcement is based on two properties for evaluating an enforcement mechanism: soundness and transparency. Soundness defines that the output is always good (“no bad traces slip out”) and transparency defines that good input is not changed (“no surprises on good traces”). However, in practical applications it is also important to specify how bad traces are fixed so that the system exhibits a reasonable behavior. We propose a new notion of predictability which can be defined in the same spirit of continuity in real-functions calculus. It defines that there are “no surprises on bad input”. We discuss this idea based on the feedback of an industrial case study on e-Health.

Nataliia Bielova, Fabio Massacci

Session 3. Web Security

SessionShield: Lightweight Protection against Session Hijacking

Abstract

The class of Cross-site Scripting (XSS) vulnerabilities is the most prevalent security problem in the field of Web applications. One of the main attack vectors used in connection with XSS is session hijacking via session identifier theft. While session hijacking is a client-side attack, the actual vulnerability resides on the server-side and, thus, has to be handled by the website’s operator. In consequence, if the operator fails to address XSS, the application’s users are defenseless against session hijacking attacks.

In this paper we present SessionShield, a lightweight client-side protection mechanism against session hijacking that allows users to protect themselves even if a vulnerable website’s operator neglects to mitigate existing XSS problems. SessionShield is based on the observation that session identifier values are not used by legitimate client-side scripts and, thus, need not to be available to the scripting languages running in the browser. Our system requires no training period and imposes negligible overhead to the browser, therefore, making it ideal for desktop and mobile systems.

Nick Nikiforakis, Wannes Meert, Yves Younan, Martin Johns, Wouter Joosen

Security Sensitive Data Flow Coverage Criterion for Automatic Security Testing of Web Applications

Abstract

Common coverage criteria for software testing, such as branch coverage and statement coverage, are often used to evaluate the adequacy of test cases created by automatic security testing methods. However, these criteria were not originally defined for security testing. In this paper, we discuss the limitation of traditional criteria and present a study on a new criterion called security sensitive data flow coverage. This criterion aims to show how well test cases cover security sensitive data flows. We conducted an experiment of automatic security testing of real-world web applications to evaluate the effectiveness of our proposed coverage criterion, which is intended to guide test case generation. The experiment results show that security sensitive data flow coverage helps reduce test cost while keeping the effectiveness of vulnerability detection high.

Thanh Binh Dao, Etsuya Shibayama

Middleware Support for Complex and Distributed Security Services in Multi-tier Web Applications

Abstract

The security requirements of complex multi-tier web applications have shifted from simple localized needs, such as authentication or authorization, to physically distributed but actually aggregated services, such as end-to-end data protection, non-repudiation or patient consent management. Currently, there is no support for integrating complex security services in web architectures, nor are approaches from other architectural models easily portable. In this paper we present the architecture of a security middleware, aimed at providing a reusable solution bringing support for complex security requirements into the application architecture, while addressing typical web architecture challenges, such as the tiered model or the lack of sophisticated client-side logic. We both evaluate the security of the middleware and present a case study and prototype implementation, which show how the complexities of a web architecture can be dealt with while limiting the integration effort.

Philippe De Ryck, Lieven Desmet, Wouter Joosen

Session 4. Model-Based Security II

Lightweight Modeling and Analysis of Security Concepts

Abstract

Modeling results from risk assessment and the selection of safeguards is an important activity in information security management. Many approaches for this activity focus on an organizational perspective, are embedded in heavyweight processes and tooling and require extensive preliminaries. We propose a lightweight approach introducing SeCoML – a readable language on top of an established methodology within an open framework. Utilizing standard tooling for creation, management and analysis of SeCoML models our approach supports security engineering and integrates well in different environments. Also, we report on early experiences of the language’s use.

Jörn Eichler

A Tool-Supported Method for the Design and Implementation of Secure Distributed Applications

Abstract

We describe a highly automated and tool-supported method for the correct integration of security mechanisms into distributed applications. Security functions to establish and release secure connections are provided as self-contained, collaborative building blocks specifying the behavior of several parties. For the security mechanisms to be effective, the application-specific model needs to fulfill certain behavioral properties, for instance, a consistent start and termination. We identify these properties and show how they lead to correct secured applications.

Linda Ariani Gunawan, Frank Alexander Kraemer, Peter Herrmann

An Architecture-Centric Approach to Detecting Security Patterns in Software

Abstract

Today, software security is an issue with increasing importance. Developers, software designers, end users, and enterprises have their own needs w.r.t. software security. Therefore, when designing software, security should be built in from the beginning, for example, by using security patterns. Utilizing security patterns already improves the security of software in early software development stages. In this paper, we show how to detect security patterns in code with the help of a reverse engineering tool-suite Bauhaus. Specifically, we describe an approach to detect the Single Access Point security pattern in two case studies using the hierarchical reflexion method implemented in Bauhaus.

Michaela Bunke, Karsten Sohr

Session 5. Security Requirements Engineering

The Security Twin Peaks

Abstract

The feedback from architectural decisions to the elaboration of requirements is an established concept in the software engineering community. However, pinpointing the nature of this feedback in a precise way is a largely open problem. Often, the feedback is generically characterized as additional qualities that might be affected by an architect’s choice. This paper provides a practical perspective on this problem by leveraging architectural security patterns. The contribution of this paper is the Security Twin Peaks model, which serves as an operational framework to co-develop security in the requirements and the architectural artifacts.

Thomas Heyman, Koen Yskout, Riccardo Scandariato, Holger Schmidt, Yijun Yu

Evolution of Security Requirements Tests for Service–Centric Systems

Abstract

Security is an important quality aspect of open service–centric systems. However, it is challenging to keep such systems secure because of steady evolution. Thus, security requirements testing, considering system changes is crucial to provide a certain level of reliability in a service–centric system. In this paper, we present a model–driven method to system level security testing of service–centric systems focusing on the aspect of requirements, system and test evolution. As requirements and the system may change over time, regular adaptations to the tests of security requirements are essential to retain, or even improve, system quality. We attach state machines to all model elements of our system- and test model to obtain consistent and traceable evolution of the system and its tests. We highlight the specifics for the evolution of security requirements, and show by a case study how changes of the attached tests are managed.

Michael Felderer, Berthold Agreiter, Ruth Breu

After-Life Vulnerabilities: A Study on Firefox Evolution, Its Vulnerabilities, and Fixes

Abstract

We study the interplay in the evolution of Firefox source code and known vulnerabilities in Firefox over six major versions (v1.0, v1.5, v2.0, v3.0, v3.5, and v3.6) spanning almost ten years of development, and integrating a numbers of sources (NVD, CVE, MFSA, Firefox CVS). We conclude that a large fraction of vulnerabilities apply to code that is no longer maintained in older versions. We call these after-life vulnerabilities. This complements the Milk-or-Wine study of Ozment and Schechter—which we also partly confirm—as we look at vulnerabilities in the reference frame of the source code, revealing a vulnerabilitiy’s future, while they looked at its past history. Through an analysis of that code’s market share, we also conclude that vulnerable code is still very much in use both in terms of instances and as global codebase: CVS evidence suggests that Firefox evolves relatively slowly.

This is empirical evidence that the software-evolution-as-security solution—patching software and automatic updates—might not work, and that vulnerabilities will have to be mitigated by other means.

Fabio Massacci, Stephan Neuhaus, Viet Hung Nguyen

Session 6. Authorization

Authorization Enforcement Usability Case Study

Abstract

Authorization is a key aspect in secure software development of multi-user applications. Authorization is often enforced in the program code with enforcement statements. Since authorization is present in numerous places, defects in the enforcement are difficult to discover. One approach to this challenge is to improve the developer usability with regard to authorization. We analyze how software development is affected by authorization in a real-world case study and particularly focus on the loose-coupling properties of authorization frameworks that separate authorization policy from enforcement. We show that authorization is a significant aspect in software development and that the effort can be reduced through appropriate authorization frameworks. Lastly, we formulate advice on the design of enforcement APIs.

Steffen Bartsch

Scalable Authorization Middleware for Service Oriented Architectures

Abstract

The correct deployment and enforcement of expressive attribute-based access control (ABAC) policies in large distributed systems is a significant challenge. The enforcement of such policies requires policy-dependent collaborations between many distributed entities. In existing authorization systems, such collaborations are static and must be configured and verified manually by administrators. This approach does not scale to large and more dynamic application infrastructures in which frequent changes to policies and applications occur. As such, configuration mistakes or application changes might suddenly make policies unenforceable, which typically leads to severe service disruptions.

We present a middleware for distributed authorization. The middleware provides a single administration point that enables the configuration and reconfiguration of application- and policy-dependent interactions between policy enforcement points (PEPs), policy decision points (PDPs) and policy information points (PIPs). Using lifecycle and dependency management, the architecture guarantees that configurations are consistent with respect to deployed policies and applications, and that they remain consistent as reconfigurations occur. Extensive performance evaluation shows that the runtime and configuration overhead of the middleware scale with the size and complexity of the infrastructure and that reconfigurations cause minimal disruption to the involved applications.

Tom Goovaerts, Lieven Desmet, Wouter Joosen

Adaptable Authentication Model: Exploring Security with Weaker Attacker Models

Abstract

Most methods for protocol analysis classify protocols as “broken” if they are vulnerable to attacks from a strong attacker, e.g., assuming the Dolev-Yao attacker model. In many cases, however, exploitation of existing vulnerabilities may not be practical and, moreover, not all applications may suffer because of the identified vulnerabilities. Therefore, we may need to analyze a protocol for weaker notions of security. In this paper, we present a security model that supports such weaker notions. In this model, the overall goals of an authentication protocol are broken into a finer granularity; for each fine level authentication goal, we determine the “least strongest-attacker” for which the authentication goal can be satisfied. We demonstrate that this model can be used to reason about the security of supposedly insecure protocols. Such adaptability is particularly useful in those applications where one may need to trade-off security relaxations against resource requirements.

Naveed Ahmed, Christian D. Jensen

Session 7. Ideas

Idea: Interactive Support for Secure Software Development

Abstract

Security breaches are often caused by software bugs, which may frequently be due to developers’ memory lapses, lack of attention/focus, and knowledge gaps. Developers have to contend with heavy cognitive loads to deal with issues such as functional requirements, deadlines, security, and runtime performance. We propose to integrate secure programming support seamlessly into Integrated Development Environments (IDEs) in order to help developers cope with their heavy cognitive load and reduce security errors. As proof of concept, we developed a plug-in for Eclipse’s Java development environment. Developers will be alerted to potential secure programming concerns, such as input validation, data encoding, and access control as well as encouraged to comply with secure coding standards.

Jing Xie, Bill Chu, Heather Richter Lipford

Idea: A Reference Platform for Systematic Information Security Management Tool Support

Abstract

The ISO 27001 standard specifies an information security management system (ISMS) as a means to implement security best practices for IT systems. Organisations that implement an ISMS typically experience various challenges such as enforcing a common vocabulary, limiting human errors and integrating existing management tools and security mechanisms. However, ISO 27001 does not provide guidance on these issues because tool support is beyond its scope, leaving organisations to start “from scratch” with manual and usually paper document-driven approaches. We propose a novel reference platform for security management that provides the foundation for systematic and automated ISMS tool support. Our platform consists of a unified information model, an enterprise-level repository and an extensible application and integration platform that aid practitioners in tackling the aforementioned challenges. This paper motivates and outlines the key elements of our approach and presents a first proof-of-concept prototype implementation.

Ingo Müller, Jun Han, Jean-Guy Schneider, Steven Versteeg

Idea: Simulation Based Security Requirement Verification for Transaction Level Models

Abstract

Verification of security requirements in embedded systems is a crucial task - especially in very dynamic design processes like a hardware/software codesign flow. In such a case the system’s modules and components are continuously modified and refined until all constraints are met and the system design is in a stable state. A transaction level model can be used for such a design space exploration in this phase. It is essential that security requirements are considered from the very first beginning. In this work we demonstrate a novel approach how to use meta-information in transaction level models to verify the consistent application of security requirements in embedded systems.

Johannes Loinig, Christian Steger, Reinhold Weiss, Ernst Haselsteiner

Backmatter

Titel: Engineering Secure Software and Systems
herausgegeben von: Úlfar Erlingsson
Roel Wieringa
Nicola Zannone
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-19125-1
Print ISBN: 978-3-642-19124-4
DOI: https://doi.org/10.1007/978-3-642-19125-1