43308

Vetting Single Sign-On SDK Implementations via Symbolic Reasoning

Source code available in GitHub


Introduction


S3KVetter is designed to check the logical correctness and identify vulnerabilities of Single Sign-On (SSO) Software Development Kits (SDKs). Single Sign-On protocols like OAuth2.0 and OpenID Connect have been widely adopted to simplify user authentication and service authorization for third-party applications. Mainstream identity providers, such as Facebook and Google, have developed SDKs to facilitate the implementation of SSO for 3rd-party application developers. These SDKs have become a critical foundation for web services. Despite its importance, little effort has been devoted to a systematic testing on the implementations of SSO SDKs, especially in the public domain. To this end, S3KVetter leverages dynamic symbolic execution to track feasible execution paths and the associated predicates of the SSO SDK.

Although S3KVetter was originally designed to test SSO SDKs, it’s relatively straightforward to use it to test other SDKs.

Architecture


S3KVetter contains three components: an extended concolic (dynamic symbolic) execution engine, a predicate translator and a theorem prover. The concolic execution engine aims to explore the target SSO SDK exhaustively and output all the feasible program paths in the form of a predicate tree. To support formal reasoning, the predicate translator then expresses this predicate tree using a precise syntax that lends itself to precise semantics. Finally, taking the translated predicate tree and our manually developed list of security properties as inputs, the theorem prover reasons about each program path for security property violation.

S3KVetter architecture

  • Extracting Program Predicates: S3KVetter use the symbolic execution engine PyExZ3 to explore as many paths as possible. Based on dynamic symbolic execution, S3KVetter can track how the operations on specific symbolic fields/ variables affect the final computation result. We leverage these messages to build a so-called symbolic predicate tree.
  • Translating the Predicate Tree: To support formal reasoning, we should translate the extracted tree from the previous step to a set of Boolean logic formulae. We use SMT-Lib v2.0 as the logic language. A program path can be represented as the conjunction of all the node logic formulae along this path. And the disjunction of all the path logic formulae to represent the entire predicate tree.
  • Reasoning Predicates: We first define the correct logic that should be enforced by the SDK. For example, for SSO SDKs, we have one key observation to secure the Single Sign-On service: An RP server should login a user if and only if the exact user has actually authorized this specific RP. We use SMT-Lib v2.0 to define the logic, and then check whether the SDK under test follows these logical conditions or not.

Highlighted Features


  • Flexibility to define security properties: We use SMT-Lib v2.0 to define the logic. The logic language provided by SMT-Lib is not only expressive enough but also widely accepted by most theorem provers. Since the predicate tree is represented using the first-order logic with quantifier of SMT-Lib v2.0, we can directly use CVC4 to verify whether there are cases violating the defined security properties.
  • Embedding Complex Functions to the Predicate Tree: When encounter complex functions, like hash function or crypto related functions, the concolic execution engine will use concrete value to execute the function. The issue is the concrete value of the symbolic variable is not shown in the predicate tree. And if there is boolean condition check related to the complex function, the concolic execution engine may miss a branch of the code.
    Let’s use the hash function md5 as an example. For the following code:
    from symbolic.args import *
    		import hashlib
    
    		@symbolic(v='mini2')
    		def hashtestV1(v):
    		    if 'mini' in v:
    		        if hashlib.md5(v.encode()).hexdigest() == '44c6c370fd1859325f7119e96a81584e':
    		            return 1
    		        elif v == 'mining':
    		            return 2
    		        elif v == 'mining2':
    		            return 3
    		    return False
    		
    A typical concolic execution engine will export the following tree:
    Sample Predicate Tree
    It didn’t explore the branch that leads to return 1. The value of v that leads to this branch is “mini”. In order to cover as many branches as possible, S3KVetter takes a configuration file, in which user needs to specify the concrete value of the symbolic variable that can leads satisfy the boolean condition. With the configuration file, S3KVetter exports the following tree:
    Sample Predicate Tree
    We can see it not only covers the previously missing branch, but also add a new variable v_hashlib_md5. You can use this newly created variable to define your security properties.
  • Extendable to Testing Other SDKs: What S3KVetter does is to explore the SDK source code and export all covered paths in the format of predicate tree. Then it compares the tree with user defined security properties to see whether there is any branch that can lead to a violation of these security properties. During the whole process, nothing is limited to SSO protocols, except user defined security properties. This makes it relatively straightforward to apply S3KVetter to other types of SDKs. Here is an example about how we use it to test mobile payment SDKs.

Examples


In this section, we will demonstrate how to use S3KVetter to test OAuthLib - Python Framework for OAuth1 & OAuth2. Note that the test was done in 2017, and the code version of OAuthLib is different from the latest one in its GitHub repository. You can find the version of source code we use here.
OAuthLib is used for the OAuth request-signing logic. As the data used during the test, like user ID, app ID, app key, etc. are not real, we need to modify the SDK source code to handle these exceptions. The modified source code of OAuthLib is available here.

We use the following code as the client side (client.py):

#! /usr/bin/python
		# -*- coding:utf-8 -*-

		# ----- Import Section -----
		from oauthlib.oauth2 import WebApplicationClient
		from symbolic.args import *
		import urllib.request
		# ----- End of Import Section -----


		# ----- Constant Declaration -----
		client = WebApplicationClient('your_id')
		coordination= 0
		# ----- End of Constant Declaration -----

		@symbolic(Req0Flag=1, Req1Flag=1, isHttps=1, useState=1, params={'code':'wrongcodeval','state':'sfetw45','access_token':"1234",'refresh_token':"4321", 'mac_key':"abcdef"})
		def client_app(Req0Flag, Req1Flag, isHttps, useState, params):
		    
		    #Redirect user to IdP for authorization
		    if useState:
		        stateVal = 'sfetw45'
		    else:
		        stateVal = ''
		    if isHttps:
		        auth_url = 'https://example.com'
		    else:
		        auth_url = 'http://example.com'

		    if Req0Flag == 1:
		        try:
		            auth_url = client.prepare_request_uri(auth_url, scope=['profile', 'pictures'], state=stateVal)
		        except:
		            return {'refresh_token':None, 'code':None, 'token':None, 'mac_key':None}

		    #Get the access token
		    if Req1Flag == 1:
		        client.my_parse_request_uri_response(auth_url, params, state=stateVal)
		        para = client.prepare_request_body()

		        if 'code' in params and params['code'] =='correctcodeval':
		            body = '{\
		                "access_token":"2YotnFZFEjr1zCsicMWpAA",\
		                "token_type":"example",\
		                "expires_in":3600,\
		                "refresh_token":"tGzv3JOkF0XG5Qx2TlKWIA",\
		                "example_parameter":"example_value"\
		            }'
		        else:
		            body = '{\
		                "error":"error msg",\
		                "access_token":"",\
		                "token_type":"example",\
		                "expires_in":3600,\
		                "refresh_token":"",\
		                "example_parameter":"example_value"\
		            }'
		        client.my_parse_token_response(body)

		    #Shuffle the request order
		    if Req0Flag == 2:
		        try:
		            auth_url = client.prepare_request_uri(auth_url, scope=['profile', 'pictures'], state='sfetw45')
		        except:
		            return {'refresh_token':None, 'code':None, 'token':None, 'mac_key':None}

		    #Retrieve User Info
		    #if Req2Flag != 0:
		    return {'refresh_token':client.refresh_token, 'code':client.code, 'token':client.access_token, 'mac_key':client.mac_key}
		

We also simulate cases of sending out of order requests during OAuth process. We define the following security properties (oauth.expected):

;Access Token Injection
		(=> (= code "wrongcodeval") (= returnVal.token "None"))
		;Refresh Token Injection
		(=> (= code "wrongcodeval") (= returnVal.refresh_token "None"))
		;Use before assignment state
		(=> (= Req0Flag 0) (= returnVal.token "None"))
		;Bypass Mac_key protection
		(=> (= code "wrongcodeval") (not (= returnVal.mac_key "abcdef")))
		;HTTPS Check
		(=> (= isHttps 0) (= returnVal.token "None"))
		;Misuse or no use of state
		(=> (= useState 0) (= returnVal.token "None"))
		

Each security property is designed to reveal one vulnerability, and all properties are written using SMT-Lib v2.0. Then run the command below to test if this SDK has any paths violating these security properties.

python3 pyexz3.py client_app.py --expected oauthlib.expected 
		

If find any violations, S3KVetter will output the set of values of all symbolic variables that can trigger the issue.

Following inputs violate security rule: (=> (= isHttps 0) (= returnVal.token "None"))

		Req0Flag(Int): 0
		Req1Flag(Int): 1
		isHttps(Int): 0
		useState(Int): 1
		mac_key(String): ""
		refresh_token(String): ""
		access_token(String): ""
		state(String): ""
		code(String): "correctcodeval"
		returnVal.mac_key(String): "abcdef"
		returnVal.token(String): "2YotnFZFEjr1zCsicMWpAA"
		returnVal.code(String): "correctcodeval"
		returnVal.refresh_token(String): "tGzv3JOkF0XG5Qx2TlKWIA"
		

Using S3KVetter to test Mobile Payment SDKs


In this section, we will discuss how to extend S3KVetter to test third-party mobile payment SDKs, e.g., alipay-sdk-python. The extension relies on two new features, including Cashier Behavior Simulation and Dynamic Symbolic Variable Injection.

  • Cashier Behavior Simulation: Unlike SSO, mobile payment protocols involve complicated cryptographic operations on the server side, i.e., both the Cashier Server and Merchant Server. Though S3KVetter may send requests to the Cashier Server directly, the online method is usually time-consuming and setting up the merchant account on the Cashier is tricky. Thus, we try to understand the logic within the Cashier Server by reading documents and develop a library to simulate its behavior in the payment process. Then, the client script for symbolic execution can simply import the library to get the desired response from the Cashier Server. At the moment, the library is general enough to test all the SDKs for both Alipay and Wechat Pay and we plan to extend it for other Cashiers later.
  • Dynamic Symbolic Variable Injection: As mentioned above, SDKs for mobile payment protocols tend to contain complicated functions for parsing and verifying the signature within the incoming request, e.g., cryptographic functions. Unfortunately, the functions cannot be translated into the standard SMT language and the extracted program predicates are incomplete, causing false negatives. Thus, we develop the feature of Dynamic Symbolic Variable Injection, to hook the complicated functions and replace their parameters or return values (including the variables that we are interested in, e.g., the total price of the order) with symbolic variables. Then, the symbolic variables will enter the verification block within the SDKs and may lead to the discovery of vulnerabilities, e.g., lack of checking on key parameters. The figure below gives an example of the hooking configurations, where five variables within the parameter of a signature verification function (from an Alipay SDK) are replaced by the pre-defined symbolic variables.
  • The following testing result presents one detected vulnerability in an official payment SDK, where the checking of app_id is missed and may be exploited by the attacker to buy things for free.

    Following inputs violate security rule: (=> (and (= sequential_notification 1) (not (= app_id2 "2014072300007148"))) (= returnVal 0))
    
    		fbsr_156258847901639(String): ""
    		value(String): ""
    		state(String): ""
    		access_token.uid(String): ""
    		total_amount2(String): ""
    		app_id2(String): ""
    		out_trade_no2(String): "201800000001201"
    		total_amount1(String): ""
    		out_trade_no3(String): ""
    		returnVal(Int): 1
    		total_amount3(String): "A"
    		sequential_handling(Int): 1
    		seller_id2(String): "2088301194649043"
    		trade_no3(String): ""
    		seller_id3(String): ""
    		sequential_notification(Int): 1
    		app_id3(String): ""
    		trade_no2(String): ""
    		

    In the situation, the app_id within the payment notification (from the Alipay server) is not parsed out, such that the merchant server cannot get the data. Then, the attacker may inject a forged notification that was originally generated for another merchant (with a different app_id) that shares the same out_trade_no (order id) and total_amount (the amount of money). As the key used for verifying the signature is the same among different merchants in some scenarios, the forged notification can pass the checking on the merchant server and can cheat the server that the payment is settled. Thus, the attacker can get the products from the vulnerable merchants for free.

    .: TOP :.
    Last Updated on Jun 6 2019.
    Copyright © 2019. All Rights Reserved. MobiTeC, The Chinese University of Hong Kong.
    Disclaimer Privacy Statement