【作者】 刘勇；

【导师】 吴立军；

【作者基本信息】 电子科技大学 ， 工程硕士（专业学位）， 2021， 硕士

【摘要】 模型检测是一种验证软硬件系统的强有力方法,它首先用形式化语言来描述待检验系统和系统需要满足的规范,然后使用DFS(Depth First Search)等算法遍历系统模型的状态空间,找出不满足规范的地方并返回反例以指导系统修改。但是现有的模型检测器都是基于单反例的,其在验证系统时往往需要人为的多次干预才能完成验证过程。另一方面,随着移动互联网时代下各种应用和平台的用户量爆发增长,人们将自己在某个平台的信息授权给第三方应用的场景越来越常见。OAuth 2.0(Open Authorization)协议作为一种开放授权协议,被国内外许多企业和应用如微信、Google、Facebook等用作其信息授权解决方案。然而,目前关于OAuth2.0协议安全性的研究工作还不够多,且存在建模不准确、分析效率不高等问题。本文使用多反例方法对模型检测工具SPIN(Simple Promela Interpreter)进行研究和改进,并利用模型学习方法和改进后的SPIN对OAuth 2.0协议进行分析验证。具体地,主要工作如下:(1)本文改进了模型检测器SPIN。SPIN是一个基于单反例的模型检测工具,在使用SPIN进行协议验证时,如果发现一个反例它就会自动中止,需要人为地对引发这个反例的错误进行修改,然后重新进行验证以生成下一个反例,这个过程较为繁琐。本文提出了对SPIN验证流程的修改方法,使其仅需一次验证就能搜索出所有反例。针对这些反例中可能存在相似反例的问题,本文借鉴字符串相似度的度量方法对相似反例进行了精简和消除。此工作简化了SPIN的验证过程,提高了它的工作效率,同时对于其它协议和程序的分析也具有积极作用。(2)本文使用模型学习方法对OAuth 2.0协议进行了建模。建模是模型检测方法的第一步,建模的准确性直接影响到验证结果。相比于传统的人为分析建模,模型学习是一种更高效的建模方法,具有自动化程度高、建模准确等优点。本文首次将模型学习方法引入OAuth 2.0协议的建模过程,建立了协议的模型。(3)本文使用多反例的SPIN对OAuth 2.0协议进行了验证。验证结果发现该协议存在一个漏洞,攻击者可以在未经用户授权的情况下获取访问令牌,然后窃取用户的受保护资源。针对这一漏洞本文提出了对OAuth 2.0协议流程的一种改进方法,该方法通过为重定向地址添加授权服务器身份信息来保证安全性,最后通过实验验证了改进方法的有效性。更多还原

【Abstract】 Model checking is a powerful method for verifying software and hardware systems.It first uses formal language to describe the system to be tested and the specifications that the system needs to meet,and then uses algorithms such as DFS(Depth First Search)to traverse the state space of the system model to find out those that do not meet the specifications and return counterexamples to guide system modification.However,the existing model checkers are all based on single counterexample,which often require multiple human interventions to complete the verification process when verifying the system.On the other hand,with the explosive growth of the number of users of various applications and platforms in the mobile Internet era,it is more and more common for people to authorize their information on a certain platform to third-party applications.As an open authorization protocol,the OAuth 2.0(Open Authorization)protocol is used by many domestic and foreign companies and applications such as We Chat,Google,Facebook,etc.as their information authorization solution.However,there is not much research on the security of the OAuth 2.0 protocol,and there are problems such as inaccurate modeling and low analysis efficiency.This thesis uses multiple counterexamples method to improves the well-known model checking tool SPIN(Simple Promela Interpreter),and uses the model learning method and the improved SPIN to analyze and research the OAuth 2.0 protocol.Specifically,the main work is as follows:(1)This thesis improves the model checker SPIN.SPIN is a model checking tool based on single counterexample.When SPIN is used for protocol verification,if a counterexample is found,it will automatically stop.It is necessary to manually modify the error that caused this counterexample and then re-verify the system to generate the next counterexample.This process is cumbersome.This thesis proposes a modification method to the SPIN verification process so that it can search for all counterexamples with only one verification.Aiming at the problem that there may be similar counterexamples in these counterexamples,this thesis draws on the measurement method of string similarity to reduce and eliminate similar counterexamples.This work simplifies the verification process of SPIN,improves its work efficiency,and has a positive effect on the analysis of other protocols and programs.(2)This thesis Uses the model learning method to model the OAuth 2.0 protocol.Modeling is the first step of the model checking method,and the accuracy of modeling directly affects the verification results.Compared with traditional manual analysis and modeling,model learning is a more efficient modeling method,which has the advantages of high degree of automation and accurate modeling.This thesis introduces the model learning method into the modeling process of OAuth 2.0 protocol for the first time and establishes the model of the protocol.(3)This thesis uses SPIN based on multiple counterexamples to verify the OAuth2.0 protocol.The verification result found that there is a vulnerability in this protocol.The attacker can obtain access token without the user’s authorization,and then steal the user’s protected resources.Aiming at this vulnerability,this thesis proposes an improved method to the OAuth 2.0 protocol flows.This method ensures security by adding authorization server identity information to the redirection address.Finally,the effectiveness of the improved method is verified through experiments.更多还原