Vérification de la sécurité des services Web:

politiques de contrôle d'accès et firewalls XML

Ce projet est financé par le programme STIC Tunisie, DGRSRT et INRIA.

Summary

XML and Web services (WS) are major and widely adopted standards for the automatic management of distributed information and web transactions. Web services provide a standardised way that support interoperable machine to machine interaction over the Internet, based on XML messages, between various applications and data sources [Booth et al 04].

While providing advanced business functionality over the Internet, Web services introduce significant security consideration and challenges that need to be managed, as intruders attacks and other threats becomes more important [Mysore 03]. Security is a critical issue for Web services, because the Internet is an insecure and untrustablepublic network infrastructure, where the information available has different levels of confidentiality. A service consumer may invoke web services using false identity, access Web services with insufficient permissions, or corrupt web services by attacking the service providers (e.g., using an XML message based denial of service attack). Thus, security consideration becomes very critical for the successful deployment of service-oriented systems.

In this project, we focus on two important aspects of Web services security: XML Access Control Policies (ACP) and XML Firewalling. XML ACP specify the authorizations to access some parts of XML documents, and XML firewalls are network appliances that filter XML messages targeted to Web Services, according to their contents.

Our goal is to provide users and administrators some methods and tools to assist them in the development, the validation and the maintenance of XML ACPs and XML firewall configurations. One argument generally agreed is that these tasks are highly error prone and that entirely manual management is impossible. We are planing to address this problem by the development of automatic solutions based on formal models and formal methods for the analysis and error correction of XML ACP and XML firewall configurations.

XML and Web Services

XML is a format proposed by the W3C which has developed into the standard for the exchange and manipulation of data on the Web [AbiteboulBunemanSuciu]. A XML document can be seen as a labeled ordered tree. XML documents can be typed using a language called XML schema, A schema mainly enforces structural relationships between labels of elements in the document tree. The presence of structure in XML documents enables the use of queries beyond keyword search, using query languages such as XPath or XQuery.

Web services are XML based software components that can be dynamically incorporated into different applications using remote method invocation mechanisms. A web service is designed as a loosely coupled software component that can be described using WSDL (Web Services Description Language), registered in an UDDI directory (Universal Description, Discovery and Integration), and invoked using standard protocols, such as SOAP (Simple Object Access Protocol), an XML-based lightweight protocol that is bound to standard underlying protocols, e.g., HTTP.

Verification of XML Access Control Policies

Access control policies are sets of rules specifying which principal (e.g. a nurse in an hospital) can access which resources (e.g. a patients file) in what manner (read or write...). The eXtensible Access Control Markup Language (XACML) [XACML] is an XML-based language standardized by the Organization for the Advancement of Structured Information Standards (OASIS) which has become the de facto standard for specifying access control policies for various applications, in particular Web services.

XACML was designed to replace application-specific and proprietary access-control policy languages. Prior to XACML, every application vendor had to create its own proprietary method for specifying access control policies, and these applications could not understand each other’s language. It has been widely supported by all the main platform vendors and extensively used in a variety of applications.

With the explosive growth of web applications deployed on the Internet, XACML policies grow rapidly in size and complexity, and automatic solutions are needed for modeling, verifying or testing of XACML policies.

Our purpose is to develop formal methods for analyzing XACML policies, with a focus on policies specifying the access to some parts of XML documents. For this purpose, we are planing to use the experience that we have gained in the domain of the formal verification of firewall configurations, in particular during the works conducted in a former INRIA STIC Tunisie project on that topics [Ben Youssef et al. 09] and [Ben Neji and Bouhoula 08] .

We want to develop formal methods to address several problems on XACML ACPs, including:

One challenge is that in the XACML access control rules for XML documents, the resources (to be accessed) are specified by Xpath expressions, and are not simply values in finite domains, like IP addresses or port numbers for conventional firewalls, or constant values in other work on XACML policy verification, like e.g. [Kolovski et al 07]. Therefore, we will need to develop analysis techniques other simple finite state exploration.

Another challenge is the complexity of XACML specifications. XACML policies consist in policy sets, each policy set being a sequence of access control rules, and these sets and rules are combined according to a specified policy combining algorithm. XACML support several combining algorithms, including "first applicable" (the first matching rule is applied, this is the strategy in use in conventional firewalls), "deny overrides" (access is denied if any rule or set returns "deny") and "accept overrides". This algorithmic complexity implies the development of a flexible and general enough framework for the verification of XACML specifications.

Automatic Generation and Analysis of XML Firewalls

Conventional firewalls have been designed as a major component to protect a network or a server from being attacked. A conventional firewall typically resides between the Internet and a network server or a business private network, and monitors the data traffic entering and exiting the private network to prevent unauthorised access to the server or the network.

Typical types of conventional firewalls filter incoming and outgoing packets by considering only the packets IP and TCP headers (source and destination addresses, protocol, port number) and not the packet contents. That makes them not suitable for Web services security. Indeed, Web services normally use the SOAP protocol over HTTP, whose port, the default Web port number 80, is generally not blocked by conventional firewalls.

A potential intruder can include malicious SOAP attachments, insert harmful SQL code or executable commands into an XML message, or send an extremely large XML message to overload the XML parser on the service provider side [Moradian and Hakansson 06]. A conventional firewall usually does not examine the content of a packet; thus, it is not able to identify threats such as SQL injection, denial of service, schema poisoning, and XML parameter poisoning. For example, an XML message tampered with an XML injection attack (insertion of tags altering the structure of the message) can erase a whole database or insert unauthorized information in a database. Such a message cannot be detected using packet filtering techniques; instead, it can only be detected by content filtering approaches. Hence, conventional firewalls are not sufficient to provide security for web services. In order to protect Web services from being attacked, a specialized firewall, placed between a conventional firewall and a network server, and called XML firewall, enforces access restrictions for web services invocation. by filtering the entire content of XML messages (not TCP packets).

Typical components used for the configuration of XML firewalls include: Access control enforcement (authentication, authorization, accountability), Filtering of incoming and outgoing XML messages using Xpath content filters, Validation of XML messages for well-formed structure, using XML schemas.

We are interested in providing methods for assisting and automating the developments of such components. One example of related work on that matter is [Gruschka, Luttenberger 06] which proposes a technique for protecting Web services against Denial-of-Service (DoS) attacks with the automatic generation of an XML Schema used for filtering incoming XML messages.

One other relevant security problem in this context is XML injection: injection of XML tags in an XML document, changing the structure of the document in order to alter the behavior of the service that is going to treat the document.

The related problem of command injection attacks was addressed in [Su Wassermann 06]. In this paper, the authors propose an algorithm for the analysis of SQL requests to a back-end database, generated by web applications (from some user input). The purpose of the algorithm is the detection of SQL injection attacks, and it is based on parsing techniques, using a context-free grammar automatically generated for that purpose. We are willing to adapt this idea to the detection of XML injection attacks, where the objects to be analysed are XML messages, i.e. Trees, whereas SQL requests are words. Therefore, our intention is to develop some techniques based on formal language theory for trees (instead of formal language theory for words in [Su Wassermann 06]).

Besides providing assisted methods for configuring XML firewalls, another challenge can be their static analysis. For instance, it can be interesting to verify wether a XML firewall (given by Xpath filters and an XML schema) will block XML injection attacks. The formal language theoretic framework described above could be useful in this context, for instance, the above problem could be reduced to the problem of equivalence of languages of trees.

Another challenge is to be able to deal with stateful XML firewall model like [Xu et al 04].

References

[AbiteboulBunemanSuciu]
Serge Abiteboul and Peter Buneman and Dan Suciu. Data on the Web: From Relations to Semistructured Data and XML Morgan Kaufmann, 1999.
[Booth et al. 04]
Booth, D., Haas, H., McCabe, F., Newcomer, E., Champion, I.M., Ferris, C. and Orchard, D. Web services architecture W3C Working Group Note http://www.w3.org/TR/2004/NOTE-ws-arch-20040211/.
[Kolovski et al 07]
V. Kolovski and J. Hendler and B. Parsia. Analyzing Web Access Control Policies Int. WWW Conference, ACM, 2007.
[Mysore 03]
S. Mysore. Securing web services, concepts, standards, and requirements White paper, Sun Microsystems, October 2003.
[Moradian and Hakansson 06]
Moradian, E. and Hakansson, A. Possible attacks on XML web services IJCSNS International Journal of Computer Science and Network Security, Vol. 6, No. 1B, pages 154-170, 2006.
[Xu et al 04]
Haiping Xu, Mihir Ayachit and Abhinay Reddyreddy Formal modelling and analysis of XML firewall for service-oriented systems Int. J. Security and Networks, Vol. 3, No. 3, 2008.
[XACML]
OASIS eXtensible Access Control Markup Language (XACML) V2.0 Specification Set http://www.oasis-open.org/committees/xacml/. 2007.
[Su Wassermann 06]
Su and Wasserman .The essence of Command Injection Attacks in Web Applications POPL 2006.
[Gruschka, Luttenberger 06]
Nils Gruschka and Norbert Luttenberger Protecting Web Services from DoS Attacks by SOAP Message Validation in Security and Privacy in Dynaminc Environments, vol. 201 of IFIP international Federation for Information Processing, 2006.
[Ben Youssef et al. 09]
N. Ben Youssef, A. Bouhoula and F. Jacquemard. Automatic Verification of Conformance of Firewall Configurations to Security Policies.(ISCC09).
[Ben Neji and Bouhoula 08]
N. Ben Neji and A. Bouhoula . Dynamic Scheme for Packet Classification Using Splay Trees.(CISIS08).