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.
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.
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.
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.
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 plugin 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.
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.
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.
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.
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-assecurity solution--patching software and automatic updates--might not work, and that vulnerabilities will have to be mitigated by other means.
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.
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.
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.
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.
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 systemand 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.
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.
