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.

• 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:
  
  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:
  
  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.

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.