Ensuring the compliance of developed software with securit y requirements is a challenging task due to imprecision on the security guidelines definition, and to the l ack of automatic and formal means to lead this verification. In this paper, we present our approach that aim s at integrating the formal specification and verification of security guidelines in early stages of the develo pment life cycle by combining the model checking together with information flow analysis. We formally specif y security guidelines that involve dependent information flows as a basis to lead formal verification through mod el checking, and provide precise feedback to

Ensuring the compliance of developed software with security requirements is a challenging task due to imprecision on the security guidelines definition, and to the lack of automatic and formal means to lead this verification. In this paper, we present our approach that aims at integrating the formal specification and verification of security guidelines in early stages of the development life cycle by combining the model checking together with information flow analysis. We formally specify security guidelines that involve dependent information flows as a basis to lead formal verification through model checking, and provide precise feedback to the developer.

The development and delivery of secure software is a challenging task, that gets even harder when the developer tries to adhere to both application and organization-specific security requirements translated into security guidelines. These guidelines serve as best practices or recommendations that help reduce application exposure to vulnerabilities, and provide hints about the application's adherence to high-level and abstract security requirements. In this paper, we present guidelines we gathered from different sources, and we highlight the main issues related to the interpretation and application of those guidelines. We present a first attempt to classify the requirements with the objective of identifying the analysis that should be performed to verify the adherence of the developed software to each of the categories.

In order to cater for a growing user base that requires varied functionalities and owns multiple devices, software providers are using cloud solutions as the preferred technical means. In fact, all major operating systems come with a tight integration to cloud services. Software solutions that have such integration with cloud services should disclose (transparency) this to the consumer. Furthermore, with mounting concerns over the security of software, consumers are demanding assurance over the software being used. Software certification can address both issues: security and transparency of software, thereby providing comprehensive assurance to consumers. However current software certifications are tailored for human consumption and represented in natural language, a major issue that hinders automated reasoning to be performed on them. Focused research efforts in the past few years have resulted in a Digital Certification concept, a machine process able representation of certifications, that can cater to different software provisioning models. We extend the notion of a Digital Certification by using the Linked Data vocabulary to express general characteristics of software systems that benefits from existing and future knowledge from the Linked Data community. This greatly increases the usability of such Digital Certifications and has a wider impact on the Software certification landscape.

Developing and delivering secure software is a challenging task, that gets even harder when the developer tries to adhere to both application and organization-specific security requirements. Different approaches have been proposed to facilitate this task, such as code analysis that aims at detecting flaws in the developed software before it is released and deployed to customer. This paper discusses a number of static code analysis approaches and presents different code analysis tools adopting each a specific analysis technique. These tools are evaluated against a sample code illustrating different security challenges that can be addressed using an approach that helps detecting security properties. The latter can be transformed into abstract security policies that can be validated against explicit security requirements. This would help the developer throughout the software development lifecycle and to ensure the compliance with security specifications.

Developing and deploying secure software is a difficult task, one that is even harder when the developer has to be conscious of adhering to specific company security requirements. In order to facilitate this, different approaches have been elaborated over the years to varying degrees of success. To better understand the underlying issues, this paper describes and evaluates a number of static code analysis techniques and tools based on an example that illustrates prevalent software security challenges. The latter can be addressed by considering an approach that allows for the detection of security properties and their transformation into security policies that can be validated against security requirements. This would help the developer throughout the software development lifecycle and to insure the compliance with security specifications.

Jakub Sendor: is a research associate working in the Security & Trust research practice at SAP Labs France in Sophia-Antipolis. He is involved in the prototypes development initiatives around declarative authorization policies as well as working in A4Cloud (Accountability for Cloud) EU publicly funded project. His main interest comprise of cloud computing, dynamic programming languages and enterprise Java systems

Cloud- and service-oriented computing paradigms are intrinopaque to their users, as they cannot inspect providers’ implementations, and important concerns about aspects like security, compliance, dependability can arise. Therefore, users have to make trust decisions with respect to software providers, with the hope that there will not be any detrimental consequences. To contrast this situation, the paper proposes a framework to define, assess, monitor and make explicit the elements of a service that render it trustworthy. This paper relies on a number of recent scientific contributions, and aims at supporting informed decisions on obscure service implementations by machine-understandable statements about their objective (trustworthiness) characteristics. Such statements would innovate upon many aspects of service operations, from discovery to composition, deployment and monitoring. To demonstrate this, the paper presents a concept for a Trustworthy Service Marketplace.

In a SOA context, enterprises can use workflow technologies to orchestrate available business processes and their corresponding services and apply business rules or policies to control how they can be used and who can use them. This approach becomes a bit more complex when a set of business processes includes services that derive outside the company's domain and therefore can be difficult to align with existing rules/policies. In the privacy and security domain, access control and policy languages are used to define what actions can be performed on resources, by whom, for what purpose and in what context. In this paper we propose an approach for dealing with the inclusion of internal and/or external services in a business process that contains data handling policies.

This chapter describes requirements for privacy in service-oriented architectures. It collects 39 legal and technical requirements, grouped in the five categories. These requirements are the starting point for a technical framework that brings privacy-enhanced data handling to multi-layered, multi-domain service compositions. We describe an abstract framework that is technology agnostic and allows for late adoption also in already existing SOA applications. We describe the general building blocks that are necessary on a PII provider's side and on a PII consumer's side. Finally, we look at the technical implementation of a very common, yet complicated aspect: the composition of policies when composing information artifacts. We describe how the composition of data influences the composition of policies.

The OASIS eXtensible Access Control Language (XACML) provides an interoperable tool for writing and enforcing access control policies based on attributes, i.e. characteristics of the entities that take part to the access, such as subjects or actions. Unfortunately, the attribute based approach starts to show its limits when entities exhibit complex relationships, such as semantic relations, which would be easily captured using ontologies instead of attributes. This paper integrates the XACML attribute model with an OWL ontology and describes a practical privacy filtering application able to filter out information from XML documents, according to a set of XACML semantic privacy policies.

Security policies exchanged between applications are typically huge, complex and private. A server must publish these policies to permit any client that wants to use the service to match it with its own preferences and assess whether it complies with its security policy. This matching process consists of first verifying whether the client can access the service and then checks if the security policy of the server is compliant with the client's privacy preferences. In this paper we propose a privacy-aware policy matching model, where security policies and user's preferences are represented as binary vectors using bloom filter vectors. These vectors can be published by the server without any risk of disclosing its security policy. When the client wants to match this vector to its preferences vector it just compares the two binary arrays, without disclosing its policy. The binary comparison is also much faster and cost effective than parsing two XML files.