Project topics and materials
Get Complete Project Material File(s) Now! »
Collaboration in Modern Business
Collaboration between organizations is fundamental for modern businesses to remain competitive [Xu07, KMR05, DHL01]. It can be implemented by meshing the business processes of an organization with the business processes of its customers, suppliers, and other business partners [XB05]. Figure 1.1 shows an example of the procurement process. This process is used throughout this manuscript as a running example. In general, the term procurement refers to the purchase of goods and services from external entities for satisfying a need of the buyer. The process involves several steps, e.g., the identification of the need of the buyer, the identification of the supplier, ordering, payment, and billing. In our example we consider a simplified version with three steps: ordering goods, payment, and billing. The procurement process of Figure 1.1 involves three business partners.
They are Buyer Inc., Seller Inc., and Bank Inc.. The scenario originates from the need of Buyer to purchase goods and services. Seller is a supplier specialized in business-to-business provisioning, and Bank Inc. manages the monetary transaction between Buyer and Seller. The process is described from the point of view of Buyer Inc. and proceeds as follows. First, the employee U of Buyer Inc. accesses the store of Seller Inc. and chooses the good to purchase in the catalogue of Seller Inc.. Then, U authorizes the bank to transfer the amount of money of the goods to the account of the Seller Inc. Finally, U receives a notification from Seller confirming the purchase As shown in Figure 1.1, the procurement process can be implemented as a collection of services. Seller owns a platform implementing an onlinecatalog, a virtual shopping cart, and a customer care service. The platform is available on the Internet as a service, say S. The Bank Inc. offers an online
payment service P for performing monetary transactions and payment via credit cards. Finally, Buyer uses a web application that composes these services together implementing the process in Figure 1.1. The logic of the application in Figure 1.1 can be defined in terms of expectations of the business partners. For example, at the end of the execution, the parties involved have the following expectations:
1. Seller Inc. and Buyer Inc. agreed on the goods of the purchase and on their price;
2. The bank transferred the amount of money from an account of Buyer Inc. to the account of Seller Inc.;
3. Seller Inc. delivers the goods to Buyer Inc. Moreover, Buyer Inc. has additional security requirements, i.e., only authorized employees working for the procurement department can create orders at S and authorize payments at P. These type of requirements can be satisfied by using security protocols.
The Role of Security Protocols
Prior to computer networks, security of business applications was achieved by restricting physical access to the mainframes [MCJ97]. Physical restriction was then replaced by authentication schemes in which a user provides username and password over a terminal [MCJ97]. This mechanism was sufficient to access the computer via secure communication channels [MCJ97].
In 1980s, the need of sharing data and computational resources led to the creation of computer networks in which organizations connected computers to each other over insecure communication channels. As a result, attackers could intercept and reuse user credentials to gain unauthorized access. Exchanging credentials in clear-text over these links was no longer a secure practice [MCJ97]. This led to the development of user authentication protocols and other security protocols based on cryptographic primitives (See the Security Protocols Open Repository [spo02]).
Security protocols play two roles in modern business applications. First, they provide the security guarantees that business applications need in order to carry out the business functions, e.g., user authentication and confidential message exchange. Second, they are enabling technology for business collaborations. For example, security protocols allow business partners to set up federated identity management, or enable an organization to share resources with partners keeping the ownership and the access control. With reference to Figure 1.1, let us consider the following two securityrelevant requirements. First, Buyer Inc. would like that only authorized employees of the procurement department can create orders at S, and authorize payments at P. Second, Buyer Inc. would like that its employees are authenticated only once to access the services S and P.
These two requirements are satisfied by security protocols. For example, Figure 1.2 shows a detailed description of the procurement process that extends Figure 1.1 by adding two new services IdP and AS. IdP is the identity management provider in charge of authenticating users of the organization of Buyer Inc.. AS is the authorization service that grants or denies the access to resources to the employees of Buyer Inc.. The user authentication and authorization are performed upon a request issued by a service called initiator. Then, IdP, or AS, issues a signed token for the initiator that proves that the user is authenticated, or authorized, respectively. For the sake of simplicity, in Figure 1.2 we omit the token generation and exchange. The process is the following. First, U accesses S for making an order for the item I. S does not known the identity of U nor whether U is authorized to make orders. Thus, S asks U to be authenticated by IdP, the identity provider of his own company, and to be authorized by AS to make an order at S. U shows to S two messages signed by IdP and AS to prove that she is authenticated and authorized. Afterwards, U confirms the order and visits P for transferring money to the account of the store. Similarly as seen before, P does not know the identity of U nor whether U is authorized to access P.
White-box Security Testing
In this section, we review relevant white-box testing techniques that can be applied when the source code of the application is available. White-box testing tools combine together different code-based analysis techniques. The analysis begins by creating a model of the source code. The model can contain different aspects of a software program such as control flow, data flow, or both. Then, the model is analyzed by using different techniques. The choice of the technique mainly depends on the class of vulnerabilities to be detected.
To detect input validation vulnerabilities, white-box tools check whether the source code contains paths that allow untrusted input to reach databases or the output for the user. This can be done via model checking or taintbased analysis. Alternatively, the source code can be scanned to find SQL queries whose syntactical structure can be modified by the user inputs. To detect logic flaws, white-box tools use model checking or custom algorithms looking for predefined patterns in the code. When a model checker is used, the security properties to be checked can be extracted in the form of code invariants via dynamic code analysis.
Table of contents :
Acknowledgements
Abstract
Table of Contents
List of Figures
List of Tables
List of Publications
1 Introduction
1.1 Multi-party Business Applications
1.1.1 Historical Outline
1.1.2 Collaboration in Modern Business
1.1.3 The Role of Security Protocols
1.2 Security Risks of Multi-party Business Applications
1.2.1 Threats to Multi-party Business Applications and Economical Impact
1.2.2 The Rise of Logic Flaws
1.3 Objectives and Challenges
1.4 Contribution
1.5 Structure
2 Related Work
2.1 White-box Security Testing
2.1.1 Detection of Input Validation Vulnerabilities
2.1.2 Detection of Application Logic Vulnerabilities
2.1.3 Discussion
2.2 Design Verification
2.2.1 Design Verification
2.2.2 Model checking and Testing
2.2.3 Discussion
2.3 Black-box Security Testing
2.3.1 Detection of Input Validation Vulnerabilities
2.3.2 Detection of Application Logic Vulnerabilities
2.3.3 Discussion
2.4 Model Inference
2.4.1 Active learning
2.4.2 Passive learning
2.4.3 Discussion
2.5 Conclusions
3 Case Studies
3.1 Case Study 1: Web-based Single Sign-On Protocols
3.1.1 The SAML 2.0 Web browser Single Sign-On
3.1.2 The OpenID Authentication Protocol
3.1.3 Security Goals
3.2 Case Study 2: eCommerce Applications
3.2.1 Application Logic
3.3 Conclusions
4 Model Checking
4.1 Formalization
4.1.1 AVANTSSAR Specification Language
4.1.2 Formalization of SAML SSO
4.1.3 Formalization of OpenID
4.2 Formal Analysis
4.2.1 The AVANTSSAR Platform
4.2.2 SAML SSO
4.2.3 OpenID
4.3 Logic Flaws
4.3.1 SAML SSO
4.3.2 OpenID
4.4 Testing Real Implementations
4.4.1 Exploitations in SAML SSO
4.4.2 Exploitation in OpenID
4.5 Conclusions
5 From Model Checking to Security Testing
5.1 Architecture
5.2 Model Checking
5.2.1 Specification of the rules of the honest agents
5.2.2 Specification of the rules of the intruder
5.2.3 Specification of the authentication property
5.3 Instrumentation
5.3.1 Instrumentation of the rules of the honest agents
5.3.2 Instrumentation of the rules of the intruder
5.4 Test Case Execution
5.4.1 Error Handling
5.5 Experimental Results
5.5.1 Protocol Implementations Under Test
5.5.2 Experiments
5.6 Conclusions
6 Black-Box Detection of Logic Flaws
6.1 Overview
6.2 Model inference
6.2.1 Resource abstraction
6.2.2 Resource clustering
6.3 Behavioral Patterns
6.3.1 Execution Patterns
6.3.2 Model Patterns
6.3.3 Data Propagation Patterns
6.4 Test Case Generation
6.4.1 Multiple execution of repeatable singletons
6.4.2 Breaking Multi-Steps Operations
6.4.3 Breaking server-generated propagation chains
6.4.4 Waypoints Detour
6.5 Test Case Execution
6.6 Test Oracle
6.7 Experiments
6.7.1 Shopping carts
6.7.2 Testing Oracle
6.7.3 Test Case Execution
6.8 Results
6.8.1 Vulnerabilities
6.9 Limitations
6.10 Conclusions
7 From Academia to Industry
7.1 Formal Analysis of SAP NW NGSSO
7.1.1 SAP NetWeaver New Generation Single Sign-On
7.1.2 Analysis
7.2 A Formal Analysis and Security Testing Tool
7.2.1 Design Verification
7.2.2 Model-based Security Testing
7.2.3 Configuration and Implementation decisions
7.2.4 Verification and Test Campaign
7.3 Conclusions
8 Conclusions and Future Work
8.1 Contributions
8.2 Future Work
References
