Android 应用内第三方支付协议的形式化分析*

李 晖, 范立岩, 潘雪松, 冯皓楠

北京邮电大学网络空间安全学院, 北京 100876

1 引言

随着计算机、通信和互联网等多种技术的发展, 第三方支付手段逐渐被人们接受和普遍使用, 以支付宝[1]、Paypal[2]、微信支付[3]和Apple Pay[4]为代表的应用内第三方支付蓬勃发展. 通过在移动终端应用中嵌入第三方支付平台的SDK, 使得用户可以在应用内直接实现支付账单功能, 而不需要切换到其他应用或web 浏览器, 目前这种支付方式已成为了主流的支付方式[5].

应用内第三方支付协议是用户、商家和支付方为完成应用内支付功能进行的交互协议, 一般建立在密码体制基础上, 其安全性直接关系到支付能否安全顺利地完成[6]. 分析表明, 集成应用内第三方支付的App 面临伪造付款、隐私泄露等威胁[7].特别是Android 平台因其开放的特性, 以及大量的针对Android平台的HOOK 框架和易用的攻击工具, 使基于Android 平台的支付协议运行环境更具风险[8].

目前针对应用内第三方支付协议的安全性分析工作大多依赖经验的直接观察法、根据已知的攻击方法对协议进行攻击测试和验证[5,7]. 截止目前, 尚未发现采用形式化分析方法来对应用内第三方支付协议进行分析的成果. 而形式化分析方法基于数学定理和形式推理, 可以更全面的分析协议的安全性[9,10], 如通过对TLS1.3 协议[11]的分析, 发现攻击者能够在握手期间成功的模仿客户端, 通过对5G-AKA 协议[12–14]分析, 发现协议在密钥保护方面未达到预定的安全目标, 通过对EAP-AKA[15,16]协议的分析,发现存在中间人攻击等.

通过分析发现, 应用内第三方支付协议的形式化分析存在两个方面的困难:

(1) 应用内第三方支付协议缺乏明确的协议标准, 研究者难以对协议流程进行准确地建模. 与很多基于标准化的安全协议, 如OAuth[17]、5G-AKA[12–14]不同, 目前应用内第三方支付的的支付协议尚未标准化;

(2) 协议的安全目标模糊, 缺乏可量化的标准. 各个厂商提供的文档往往只规定了开发者需使用API接口和签名算法, 没有规定明确的安全目标.

本文提供了以下贡献:

(1) 本文选择了五个在中国使用广泛的第三方支付平台[18]: 支付宝、微信支付、银联支付[19]、京东支付[20]和招行一卡通[21], 深入分析这些平台提供的开发文档和样例代码, 通过归纳和抽象的方法, 给出了应用内第三方支付的协议流程, 同时提出了协议的安全假设和安全目标.

(2) 本文对协议流程和安全目标进行形式化建模, 采用ProVerif 工具对应用内第三方支付协议进行形式化分析, 分析表明在安全假设无法全部满足的情况下, 存在订单篡改、订单替换和通知伪造三种类型的攻击.

(3) 在对210 个不同类别的App 进行实际攻击验证后, 发现近13.8% 的App 存在被攻击的隐患.

接下来将在第2 节描述应用内第三方支付协议的架构和流程; 在第3 节分析协议的安全假设和安全目标; 在第4 节对协议流程、协议的安全目标进行建模, 并对协议进行形式化分析; 在第5 节根据形式化分析的结果, 寻找现实中的攻击实例, 并提出了提高应用内支付协议安全的建议, 最后也就是第6 节, 将给出结论.

2 应用内第三方支付协议

在从架构和协议流程两个方面介绍应用内第三方支付协议之前, 为方便阅读, 表1 列出术语表.

表1 术语表Table 1 Term list

2.1 架构

如图1 所示,共有四个实体参与应用内第三方支付协议流程,分别是商家的应用(merchant app,MA)、第三方支付SDK (third-party payment SDK, TP-SDK)、商家服务器(merchant server, MS) 和第三方支付服务器(cashier server, CS). 其中, MA 是安装在用户移动终端上的某商家应用客户端软件, 用户通过使用MA 浏览、选择和购买商家的商品; TP-SDK 是集成在MA 中的软件开发工具包, 实现了支持应用内第三方支付的各种签名及验证算法, 并完成在线付款流程; MS 维护存储与用户、商品及交易相关信息的数据库, 并完成与MA 和CS 的交互; CS 记录支付信息和状态, 并通知MS 支付完成. MA 不具备抵抗攻击者攻击的能力; TP-SDK 具备抵抗攻击者攻击的能力; MS 和CS 具有较强的实体安全性. MA 和MS、TP-SDK 和CS 通过无线方式进行交互, 存在被攻击的隐患; MA 和TP-SDK 通过进程间通信进行交互, 同样存在被攻击的隐患, MS 和CS 通过服务器间的数据专线进行交互, 安全性较高.

图1 应用内第三方支付架构图Figure 1 Architecture of in-app third-party payment

2.2 协议流程

在用户使用应用内第三方支付协议之前, 用户需要完成新用户注册及绑定第三方支付账号的相关流程, 从而使得用户具有在MA 中购买并支付商品的能力. 随后, 用户在下订单后启动第三方支付协议流程.

应用内第三方支付协议可分为四个阶段: (1) 生成订单; (2) 绑定订单; (3) 在线付款; (4) 通知结果.如图2 所示.

(1) 生成订单: MA 向MS 提交订单申请(order information, odi), 包含商品名和商品数量信息.

(2) 绑定订单: MS 收到订单申请后, 进入绑定订单流程, 微信支付、银联支付和京东支付需要完成可选流程(图2 中用虚线框表示), 而支付宝和招行一卡通则无需执行可选流程. 在可选流程中,MS 采用自己的私钥对tri 进行签名后传至CS; CS 验签并校验后, 生成支付流水号(prepay id number, pidn) 和随机数(nonce number,n), 之后再对上述信息进行签名后传给MS. MS 收到可选流程中传过来的信息, 先验签, 再将pidn 和n合并成tri, 重新签名后传给MA. 不执行可选流程的协议在MS 收到订单后直接确认MA 提交的新订单申请, 生成订单号(trade number, tn)以及订单详细信息(transaction information, tri), MS 采用自己的私钥生成对tri 的签名S后,将tri 和S传给MA. MA 对收到的信息进行签名验证后, 向用户展示交易详细信息, 并将tri 和签名S传至TP-SDK.

图2 支付流程Figure 2 Diagram of payment

(3) 在线付款: TP-SDK 收到信息后, 先进行tri 信息校验, 成功后, TP-SDK 调应用内第三方支付收银台功能, 由用户输入支付密码(pay pass-word, ppw), 完成付款.

(4) 通知结果: 付款成功后, CS 分别使用同步通知和异步通知两种方式通知付款结果. 其中同步通知流程为: CS 向TP-SDK 返回由自己私钥签名后的付款详细结果(result information, ri). TPSDK 将消息传至MA. MA 向用户展示ri 后, 再将ri 传至MS, MS 进行签名验证、解析ri 且核对正确后, 同步通知结束; 而异步通知流程为: CS 向MS 返回由自己私钥签名后的ri, MS 进行签名验证、解析ri 且核对正确后, MS 完全校验ri, 本次交易完成.

3 安全假设与安全目标

在对第三方支付平台提供的开发文档进行充分分析后, 本节将描述确定的威胁模型和明确的安全目标, 这些都是采用形式化方法分析安全协议的前提和关键要素.

3.1 安全假设和威胁模型

参考微信支付给出的最佳安全实现范例[22], 本文从密码算法、信道、数据保护和参与实体四个方面描述安全假设.

密码算法假设: 在应用内第三方支付协议采用的密码算法, 仅包括签名算法, 假设攻击者在不知道正确密钥的情况下, 无法伪造签名或者解密消息.

信道假设: 协议运行时的信道分成两类: (1) 公开信道: 攻击者可以在其中窃听, 拦截, 删除, 修改并且传输消息. (2) 私有信道: 攻击者无法将消息发送到此信道的任何参与实体, 也无法在该信道上窃听或者修改消息. 由于MA 和MS 之间的通讯没有采取任何保护措施, 因此, 假设其信道为公开信道; 而MS 和CS 通过数据专线交互, TP-SDK 和MA 的通信采用了进程间通信的方式通讯, 由操作系统保证通信安全性, TP-SDK 和CS 之间通讯的安全性由第三方支付平台采用HTTPS 协议或私有协议、服务器防刷和SO 加密等技术来保证, 因此, 假设MA 和MS、MS 和CS、TP-SDK 和CS 的通信信道为私有信道.

数据保护假设: 假设签名公钥是公开的, 而签名私钥是用户自己保存的秘密密钥, 不能被泄露.

参与实体假设: 下面通过分析实体可能被实际攻击的情况给出实体假设. 首先, TP-SDK 具备抵抗攻击者攻击的能力, 攻击者不能通过攻击实体获取信息或实施假冒攻击. 其次, MA 不具备抵抗攻击者攻击的能力, 实体被攻击后, 攻击者可以获得MA 的源码和数据, 并可以对MA 进行动态调试. 这种假设是合理的, 因为第三方支付厂商被要求采用安全加固和代码混淆等技术手段对TP-SDK (内有关键安全算法)进行保护, 但不强制对MA 做与TP-SDK 同等能力的安全防护. 最后, 本文主要研究来自移动终端的可能攻击, 因此, 假设MS 和CS 是具有实体安全性, 即攻击者不能获得MS 和CS 存储的数据.

综合上述各种假设, 考虑到协议尚未标准化、开发者开发MA/MS 时存在对协议的简化、Android 平台中存在的密码学误用[23]等现实情况, 为了使分析结果可以覆盖更广的场景和便于分析, 本文将按照下面5 种不同的安全假设条件分别对协议进行建模和分析:

安全假设1: 假设参与实体(MA、TP-SDK、MS 和CS) 完整地实现了协议, MA 和MS 之间使用了安全的通信协议, TP-SDK 具备抵抗攻击者攻击的能力, MA 不具备抵抗攻击者攻击的能力;

安全假设2: 签名私钥被写入MA, 且MS 未完全校验ri;

安全假设3: 在安全假设2 的基础上, tn 和tri 由MA 生成且未经MS 签名;

安全假设4: MA 和MS 之间未使用安全通信协议(如HTTPS 协议), 且MA 未完整展示支付信息;

安全假设5: MS 省略了验签过程, 且MS 未完全校验ri.

3.2 安全目标

本文从机密性、认证性、完整性和不可否认性四个方面, 给出应用内第三方支付协议安全目标的形式化表述.

机密性:任何情况下, 签名私钥SKMS 和SKCS 都应该保持机密, 否则, 消息签名机制将失去作用.形式化地:

认证性:应用内第三方支付协议应满足参与实体的认证性.例如, MA 向MS 发起新订单申请odi, MS接受odi 并将生成的tn 和tri 签名并返回给MA, MA 接收后验证MS 签名, 这个过程可以看作是MA和MS 的相互认证. 这里采用了Lowe 的认证属性分类法[24], 将实体A 和B 之间的认证属性由弱到强分为四种: 弱一致性(weak agreement)—只确保B 在之前已经运行过协议但不一定跟A 一起运行; 存活性(aliveness)—确保B 曾与A 一起运行协议但不一定使用相同的数据; 非单射一致性(no-injective agreement)—确保B 与A 一起运行协议, 并对数据达成一致; 单射一致性(injective agreement)—在非单射一致性的基础上保证B 的每次运行对应A 的唯一运行. 该分类法广泛应用于协议的形式化研究[12].形式化地:

完整性:任何情况下, 订单信息应保持完整, 否则, 攻击者可能会篡改订单申请和订单信息.具体地: 在存在攻击者的情况下, odi 应在生成订单阶段保持完整, tn 应在绑定订单阶段保持完整, tri 应在绑定订单阶段保持完整. 形式化地:

不可否认性: 在任何情况下, 协议结束时能够分别给MA 和MS 提供有效的对方不可否认证据. 应用内第三方支付协议应保证odi, tri, tn 和ri 的不可否认性. 形式化地:

4 形式化分析建模

4.1 建模工具

本文使用ProVerif 工具进行形式化分析. ProVerif 是一种自动的符号协议验证工具, 可以验证协议的机密性、认证性等安全属性[25], 广泛应用于分析包括TLS1.3 协议在内的诸多安全协议[26–28]. 与其他形式化分析工具相比, 如AVISPA[29]和Tamarin[30], ProVerif 解决了状态爆炸的问题, 且支持无限次数的会话. ProVerif 使用应用pi 演算进行验证, 并基于Horn 子句[31]的一阶逻辑解析规则. ProVerif 首先验证协议是否满足安全目标, 如果不满足安全目标, 则尝试自动构造攻击.

4.2 安全目标建模

对于机密性, attacker 语句可以直接质询攻击者是否可以获得机密. 例如, 质询攻击者是否可以获得MS 的签名私钥:

对于认证性, 首先定义与身份认证相关的事件类型, 然后质询事件之间是否存在对应关系. 例如, 事件CreatOrderInfo(odi)表示MA 发出了odi, 事件MS_Generate_OutTradeNo(odi)表示MS 根据odi 生成了订单号. 然后用以下方式质询这两个事件是否存在关于odi 的单射一致性对应关系:

对于完整性, ProVerif 没有提供直接验证完整性的语句, 但可以通过间接方式质询. 例如, 事件MS_Generate_Transaction(odi, tn, tri) 表示MS 根据odi 和tn 生成了tri, MS_ALL_SUCCESS_Asyn(tn, tri) 表示MS 相信订单号为tn, 交易信息为tri 的这笔交易已经成功了. 然后质询这两个事件是否存在非单射一致性的对应关系. 如果存在, 则证明在tn 和tri 未被篡改. 例如:

对于不可否认性, 在应用内支付的四个阶段中, 定义与不可否认性相关的事件类型. 例如, 在生成订单阶段, 事件CreatOrderInfo_Fin(odi) 表示MA 已经向MS 发出了odi, 事件MS_Generate_OutTradeNo_Fin(odi) 表示 MS 收到了 MA 发出的 odi 且已经生成了订单号. 然后, 在 MA 发出订单后中注册事件CreatOrderInfo_Fin(odi), 在MS 接收订单申请并生成订单号过程后注册事件MS_Generate_OutTradeNo_Fin(odi). 在最后质询这两个事件在生成订单阶段结束后是否均已发生:

4.3 协议流程建模

参与协议的四个实体被建模成四个宏, 每个宏由描述协议流程的语句组成. 例如, let MA(odi: bitstring) 表示实体MA 的宏, 参数odi 表示MA 的订单申请, out(HTTPS-Msg1, Msg1) 表示MA 向HTTPS-Msg1 信道发送Msg1, in(HTTPS-Msg1, Msg2-A1: bitstring) 表示MA 从HTTPS-Msg2-A1信道接收Msg2-A1:

为了更准确的对信道进行建模, 提升Proverif 的分析效率, 实体间的信道建被模成多条逻辑子信道.例如, MA 和MS 之间的通信了三次, 则建模三条逻辑子信道, 信道HTTPS-Msg1 传输消息Msg1, 信道HTTPS-Msg2-A1 传输消息Msg2-A1, 以此类推:

5 安全分析

在这部分将首先给出在五种安全假设条件下的应用内第三方支付协议的形式化分析结果, 之后给出了通过形式化分析找到的可能的攻击流程, 最后给出了对采用第三方支付协议的App 进行攻击测试的结果.

5.1 形式化分析结果

表2 为机密性和认证性的分析结果, 表3 为完整性和不可否认性的分析结果,表示满足安全目标, ×表示不满足安全目标, ! 表示部分满足安全目标. 可以看出, 除了在安全假设1 的条件下, 应用内第三方支付协议都存在安全目标无法全部满足的情况.

表2 机密性和认证性分析结果Table 2 Analysis result of confidentiality and authentication

表3 完整性和不可否认性分析结果Table 3 Analysis result of integrity and non-repudiation

ProVerif 构造了三种潜在类型的攻击: (1) 订单篡改攻击. (2) 订单替换攻击. (3) 通知伪造攻击. 在安全假设2 或安全假设3 下, 协议将遭受订单篡改攻击; 在安全假设4 下, 协议将遭受订单替换攻击; 在安全假设5 下, 协议将遭受通知伪造攻击.

5.2 可能的攻击

订单篡改攻击: 在安全假设2 或安全假设3 下, 安全目标C1、I2、I3 和NR2 未能达到. 对于A1-A4,协议没有达到单射一致性的认证性, 只能部分达到非单射一致性的认证性. 在上述安全目标未能达到时,存在一种潜在的订单篡改类型的攻击. 在这种类型的攻击中, 攻击者充当恶意用户, MS 为受害者. 在这种情况下, 攻击者会篡改tri, 并重新签名, 或者在本地生成订单的情况下, 直接篡改tri, 并重新签名. 最终,在商家不知情的情况下, 攻击者可以支付更少的钱. 图3 和图4 分别为两种订单篡改攻击的示意图.

图3 订单篡改攻击1Figure 3 Order tampering attack 1

图4 订单篡改攻击2Figure 4 Order tampering attack 2

订单替换攻击: 在安全假设4 下, 安全目标NR1、P2、A1、A2、A4、I1、I2 和I3 未能达到. 在这种情况下, 存在一种中间人攻击. 在这种类型的攻击中, 攻击者充当中间人, MA 为受害者. 在这种攻击中,攻击者将一笔交易的订单替换为另一笔交易, 并误导受害MA 在不知不觉中为攻击者的订单付款. 当MA和MS 的消息是通过不安全的网络通信通道传输时, 攻击者可以截取消息, 并用另一笔合法交易替代, 并将其发送给MA. 然后, 受害者将为攻击者的订单付费. 图5 为订单替换攻击的示意图.

图5 订单替换攻击Figure 5 Order replacement attack

通知伪造攻击: 在安全假设5 下, 安全目标NR3、A3 和A4 未能达到. 在这种情况下, 存在一种通知伪造攻击.在这种类型的攻击中, 攻击者充当恶意用户, MS 为受害者.攻击者在TP-SDK 要求用户确认订单并输入密码时不付款, 并向MS 发送伪造的付款结果通知. 最终, 攻击者可以不付钱并得到商品. 图6 为通知伪造攻击过程示意图.

图6 通知伪造攻击Figure 6 Notification forgery attack

5.3 攻击验证结果

本文从腾讯应用宝批量下载了近300 个App, 涵盖了下载量榜单的头部中部和尾部. 经筛选, 共有210 个App 集成了应用内第三方支付. 经验证, 13.8% 的App 存在形式化分析结果中发现的安全隐患, 这些App 主要分布在下载量榜单的尾部. 共计4 个App 面临订单篡改的风险, 22 个App 面临订单替换的风险, 3 个App 存在通知伪造的风险. 表4 为App 检测结果汇总.

表4 App 检测结果Table 4 Result of app test

涉及网络通信的部分, 通过burp suite 等工具搭建代理网络进行实验. 近33.8% 的App 在进行应用内第三方支付时使用HTTP 通信, 这意味着在生成订单、绑定订单到和通知付款结果这三个阶段, 攻击者可以轻而易举的获得交易的详细信息. 4% 的MS/MA 省略了验签过程; 1.43% 的MS 消息未签名.4.76% 的App 存在MS 未完全校验ri 的情况.

对于tn 和tri 由MA 生成、将签名私钥等放进MA 这两种情况, 在使用Apktool 和IDA 对App逆向分析后, 发现部分App 存在本地生成tn 和tri 的代码, 结合网络流量分析, 这些App 在订单生成以及绑定订单到支付阶段, 或未与MS 进行交互, 或将本地生成的tn 和tri 发给MS, MS 签名后发回MA.约13.8% 的App 存在本地生成tn 和tri 的情况. 在静态分析的过程中, 发现2.38% 的App 存在将签名私钥写入MA 的情况.

对于MA 未完整展示支付信息, 则对App 逐个进行人工分析, 检测支付时App 是否将支付信息完整的展示给用户. 经检测, 36.2% 的App 存在支付信息展示不全的情况, 这些App 只展示了交易的总金额,不展示订单号, 商品名和商品数量等信息. 表5 为上述缺陷在样本App 中的命中率.

表5 缺陷命中率Table 5 Defect hit rate

需要指出的是, 不同于传统的购物App, 很多工具类、教育类、文娱类和单机游戏类的App 常常使用应用内第三方支付完成付费解锁某项功能, 可付款的内容一般被在App 代码中进行限制, 而不是从服务器获取, 这些App 更易于被攻击.

5.4 建议

本文的工作表明, 应用内第三方支付协议在Android 平台进行实现的过程中, 存在多种无法保证应用内第三方支付的安全性的实现实例. 为了尽可能地规避这种情况, 本文给出了如下建议.

对于第三方支付平台:

(1) 应用内第三方支付协议应标准化. 目前, 大部分第三方支付平台只提供协议的简易流程图和API接口说明, 缺乏对协议的规范化描述, 且说明内容分散在各个文档中, 导致开发者难以准确地理解协议, 缺乏对协议的总体认识, 更多是在“面向API 接口” 开发.

(2) 明确应用内第三方支付协议的安全目标. 相比于FIDO 协议、Oauth 协议和5G-AKA 协议中明确的安全目标, 除微信支付对关于机密性的安全目标稍有提及外, 其他的第三方支付平台几乎没有对协议提出安全目标. 安全目标不是默认的、总所周知的, 而应由平台明确提出并规范化, 并涵盖机密性、完整性、认证性和不可否认性等安全属性.

对于应用:

(1) 需要实现MA 与MS 之间安全的网络通信, 例如使用HTTPS 协议并正确配置SSL 证书.

(2) 需能保证MA 可以展示支付的详细信息, 包括本次支付的总金额, 支付的商品名和商品数量, 订单号等.

(3) 需要确保MA 和MS 的签名& 验签过程不能被省略, 证书配置正确.

(4) 需要保证订单号& 订单详细信息在MA 提交订单申请后由服务器生成, 而不是由MA 本地生成.

(5) 需要保证MS 能够完成同步通知和异步通知, 并完成核对通知结果.

6 结束语

本文通过对应用内第三方支付协议进行形式化分析及对Android 系统App 进行实际攻击验证, 表明各种各样的原因使得应用内第三方支付协议常常运行在缺陷状态下, 导致协议无法达到其安全目标. 这些原因包括官方文档对安全目标的描述缺失、对协议流程的非标准化描述等使得开发人员更容易对协议的理解错误和简化开发, 最终使应用内第三方支付协议易于遭受攻击. 最后, 为保证应用内第三方支付协议的安全性, 本文对第三方支付平台和应用的开发者给出了建议. 在未来的工作中, 将重点从扩充安全假设、细化安全目标、扩大App 攻击测试范围这三个维度继续深入研究.