基于計算模型的安全協(xié)議Swift語言實施安全性分析

孟博，何旭東，張金麗，堯利利，魯金鈿

?

基于計算模型的安全協(xié)議Swift語言實施安全性分析

孟博，何旭東，張金麗，堯利利，魯金鈿

（中南民族大學(xué)計算機科學(xué)學(xué)院，湖北 武漢 430074）

分析IOS平臺上的安全協(xié)議Swift語言實施安全性，對保障IOS應(yīng)用安全具有重要意義。首先對已有安全協(xié)議Swift語言實施進行分析，確定Swift語言子集SubSwift，并給出其BNF；其次基于操作語義，建立SubSwift語言到Blanchet演算的映射模型，主要包含SubSwift語言的語句、類型到Blanchet演算的語句及類型的映射關(guān)系與規(guī)則；再次根據(jù)SubSwift語言到Blanchet演算的映射模型，提出從安全協(xié)議SubSwift語言實施生成安全協(xié)議Blanchet演算實施方法；最后應(yīng)用Antrl4工具和Java語言開發(fā)安全協(xié)議Blanchet演算實施生成工具SubSwift2CV，分析OpenID Connect協(xié)議、Oauth2.0協(xié)議和TLS協(xié)議的SubSwift語言實施安全性。

安全協(xié)議；實施安全性；Swift語言；形式化分析；模型抽取

1 引言

安全協(xié)議既是網(wǎng)絡(luò)空間安全[1-4]的重要組成部分，又是保障網(wǎng)絡(luò)空間安全的關(guān)鍵。從安全協(xié)議設(shè)計、安全協(xié)議抽象規(guī)范安全性的分析與驗證[5-6]到安全協(xié)議實施（安全協(xié)議代碼）[7-10]，人們主要集中在安全協(xié)議抽象規(guī)范安全性的分析和驗證方面[11]進行研究，其實用性較差。近幾年來，人們對安全協(xié)議的最終表現(xiàn)形式——安全協(xié)議實施越來越感興趣。因為無論任何安全協(xié)議都必須進行安全協(xié)議實施安全性分析才能發(fā)揮作用，所以安全協(xié)議實施安全性分析對保障網(wǎng)絡(luò)空間安全具有重要意義。

當(dāng)前，基于得到的安全協(xié)議實施，分析其安全性的主要方法有程序驗證法和模型抽取法。用程序驗證方法對已有安全協(xié)議實施的安全性進行分析時，主要集中在基于邏輯、基于類型系統(tǒng)、類型系統(tǒng)與邏輯證明相結(jié)合等方面，直接分析安全協(xié)議實施的安全性。這些方法大部分既沒有證明分析過程的正確性，又依賴于在安全協(xié)議實施中添加大量的代碼注釋與斷言。文獻[12-13]首先提出安全協(xié)議采用C語言和Java語言實施安全性分析方法：文獻[14-15]基于符號模型，提出分析安全協(xié)議C語言實施認(rèn)證性和保密性的方法。文獻[16-21]基于F類語言類型檢查器分析安全協(xié)議F類實施的認(rèn)證性和保密性。模型抽取方法首先從安全協(xié)議實施中抽取安全協(xié)議抽象規(guī)范，并且證明抽取方法的正確性，然后用協(xié)議抽象規(guī)范安全性分析工具來分析其安全性。此方法被認(rèn)為是有效且合理的，適合分析協(xié)議實施這類規(guī)模較小的代碼。在程序驗證方法中，也有部分涉及模型抽取的方法，分別是基于符號模型和計算模型。文獻[22-24]抽取安全協(xié)議F類實施的抽象模型，并分析其安全屬性；文獻[25-27]抽取安全協(xié)議C語言實施的抽象模型，分別使用ProVerif[28]和CryptoVerif[29]分析其安全性和保密性；文獻[30-31]抽取安全協(xié)議Java實施的抽象模型，并分析其安全屬性。

目前，在IOS平臺上，許多安全協(xié)議采用Swift語言實施，故其安全性的分析對保障IOS應(yīng)用安全具有重要意義。同時，目前未見關(guān)于對安全協(xié)議Swift語言實施安全性進行分析的相關(guān)文獻，因此本文基于計算模型，應(yīng)用模型抽取方法來分析安全協(xié)議Swift語言實施的安全性。

本文主要貢獻如下。

1) 定義與安全協(xié)議實施相關(guān)的Swift語言子集SubSwift，并給出SubSwift語言的巴科斯范式（BNF, Backus-Naur form）。

2) 建立SubSwift語言到Blanchet演算的映射模型，其主要包含SubSwift語言的語句、類型到Blanchet演算的語句、類型的映射關(guān)系與規(guī)則等。

3) 提出從安全協(xié)議SubSwift語言實施生成安全協(xié)議Blanchet演算實施的方法，并開發(fā)安全協(xié)議SubSwift語言實施到Blanchet演算實施生成工具SubSwift2CV。

4) 應(yīng)用CryptoVerif和開發(fā)的安全協(xié)議Blanchet演算實施生成工具SubSwift2CV，分析OpenID Connect協(xié)議、Oauth2.0協(xié)議、TLS（transport layer protocol）協(xié)議等SubSwift語言實施的安全性。

2 相關(guān)工作

文獻[22]提出驗證安全協(xié)議F#實施安全性的架構(gòu)，支持密碼原語的具體實施和符號化實施。該文獻應(yīng)用FS2PV工具把安全協(xié)議F#實施轉(zhuǎn)換為ProVerif的輸入語言——Applied PI演算，進而用ProVerif工具分析安全協(xié)議F#語言實施的保密性和認(rèn)證性。文獻[30]開發(fā)Elygah系統(tǒng)，該系統(tǒng)首先把安全協(xié)議的Java語言實施轉(zhuǎn)化成Lysa演算進程，然后得到安全協(xié)議Java語言實施的形式化模型，進而分析其認(rèn)證性。但是該文獻沒有證明抽取方法的正確性。文獻[25]首先應(yīng)用符號執(zhí)行技術(shù)，符號化執(zhí)行安全協(xié)議C語言實施，獲得安全協(xié)議C語言實施發(fā)送/接收消息的符號化描述；然后得到其形式化抽象模型；最后使用ProVerif分析其保密性和認(rèn)證性。但目前該模型只支持順序執(zhí)行語句，不支持分支語句。文獻[23-24]開發(fā)ML子集到CryptoVerif的編譯器原型FS2CV，該編譯器把安全協(xié)議F#語言實施中的密碼原語、數(shù)據(jù)庫、信道語句等轉(zhuǎn)換成基于Blanchet演算的形式化模型，然后用CryptoVerif分析其F#語言實施的保密性和認(rèn)證性，并且采用手工方式證明抽取方法的正確性。該文獻驗證TLS協(xié)議F#語言實施進行分析，證明其認(rèn)證性和保密性。文獻[26]從安全協(xié)議C語言實施中抽取其形式化模型，然后用CryptoVerif分析其認(rèn)證性與保密性。首先，通過符號化執(zhí)行從安全協(xié)議的C語言實施中抽取安全協(xié)議Ｃ語言實施抽象模型。然后，把抽取的模型轉(zhuǎn)換成CryptoVerif語法描述，使用CryptoVerif分析安全協(xié)議C語言實施的認(rèn)證性與保密性。但是目前只支持順序執(zhí)行協(xié)議，不支持分支語句。文獻[31]首先，通過定義SubJava與Blanchet演算間的語法映射關(guān)系，基于模型抽取技術(shù)開發(fā)模型抽取工具SubJava2CV。該工具對安全協(xié)議的Java語言實施首先進行分析并生成抽象語法樹，然后化簡抽象語法樹，抽取出安全模型，將其轉(zhuǎn)換為Blanchet演算的抽象語法樹，最后生成Blanchet演算代碼。最后，使用SubJava2CV抽取一個認(rèn)證協(xié)議Java語言實施的安全模型，將其轉(zhuǎn)換為Blanchet演算代碼，應(yīng)用自動化分析工具CryptoVerif分析安全屬性，證明協(xié)議實施的認(rèn)證性。文獻[32]首先基于符號模型和計算模型，應(yīng)用ProVerif和CryptoVerif分析TLS1.3安全協(xié)議抽象規(guī)范的安全性，然后給出TLS1.0-1.3安全協(xié)議實施——RefTLS。

3 SubSwift語言與Blanchet演算

3.1 SubSwift語言及其BNF

Swift語言子集SubSwift的定義主要考慮2個因素。1) Swift語言是一種復(fù)雜的編程語言。若在定義SubSwift時，考慮Swift語言的所有語句，則太過復(fù)雜。另外，由于Blanchet演算是一種安全協(xié)議建模語言，其語言簡單且功能不夠強大，故不能建立從Swift到Blanchet的演算映射。2) 對已有的安全協(xié)議實施Swift進行分析，找出開發(fā)安全協(xié)議Swift實施所需要的核心語句。綜合考慮這2個因素來定義SubSwift語言，并定義SubSwift語言的巴科斯范式，如圖1所示。

SubSwift語言主要包含的語句有：表達式語句（expression）、聲明語句（declaration）、分支語句（branch_statement）、控制轉(zhuǎn)移語句（control_ transfer_statement）。表達式語句主要包含常量（value）、變量（variable）、賦值表達式（assignment）、算術(shù)運算表達式、邏輯運算表達式（logical_statement）等。由于Blanchet演算沒有涉及算術(shù)運算，故沒有考慮SubSwift語言的算術(shù)運算部分。SubSwift語言表達式語句主要包含表達式的值、賦值表達式、邏輯運算表達式等。聲明語句是對要進行安全協(xié)議實施中所需的常量、變量、函數(shù)、類、庫等進行定義。SubSwift語言聲明語句主要包含導(dǎo)入聲明（import_declaration）、常量聲明（constant_ declaration）、變量聲明（variable_ declaration）、函數(shù)聲明（functions_declaration）和類聲明（class_ declaration）。導(dǎo)入聲明語句是指定Swift庫文件數(shù)據(jù)分組名，該分組定義多種元素?？刂妻D(zhuǎn)移語句用于控制代碼的執(zhí)行順序，從而實現(xiàn)代碼的跳轉(zhuǎn)。SubSwift語言控制轉(zhuǎn)移語句包括return語句、throw語句。return語句用于從當(dāng)前執(zhí)行的函數(shù)返回到主調(diào)用函數(shù)，同時傳回返回值。throw語句用于創(chuàng)建異常和返回代碼錯誤信息。分支語句用于某種特定條件下執(zhí)行相應(yīng)代碼的情形。SubSwift語言分支語句主要包括if語句和guard語句。if語句如：當(dāng)且僅當(dāng)if后的值為true時，執(zhí)行{statements1}；當(dāng)值為false時，并且if語句中有else語句，就執(zhí)行{statements2}，否則直接執(zhí)行下一條語句。guard語句如：與If語句實現(xiàn)相同的功能，當(dāng)且僅當(dāng)guard后的{statement}值為true時直接跳過else語句執(zhí)行下一條語句。當(dāng)條件表達式為false時，就執(zhí)行else語句，并跳出guard語句代碼段。

圖1 SubSwift語言的巴科斯范式

3.2 Blanchet演算及其BNF

4 安全協(xié)議SubSwift語言實施到安全協(xié)議Blanchet演算實施的映射模型

基于操作語義，建立安全協(xié)議SubSwift語言實施到安全協(xié)議Blanchet演算實施的映射模型，如圖3所示。將安全協(xié)議SubSwift語言實施中的發(fā)送者類、接收者類分別轉(zhuǎn)化為Blanchet演算中的發(fā)送者進程、接收者進程。套接字聲明轉(zhuǎn)化為Blanchet演算中的通道聲明，消息發(fā)送、接收接口分別對應(yīng)Blanchet演算中通道的輸出、輸入。

4.1 SubSwift語言到Blanchet演算的語句映射

在3.1節(jié)中定義的SubSwift語言主要包含表達式語句、聲明語句、分支語句、控制轉(zhuǎn)移語句等。

圖2 Blanchet演算的巴科斯范式

圖3 SubSwift語言到Blanchet演算的映射模型

圖4 SubSwift語言表達式到Blanchet演算的BNF映射規(guī)則

SubSwift語言聲明語句到Blanchet演算的BNF映射關(guān)系如圖5所示。SubSwift語言的聲明語句主要包含導(dǎo)入聲明、常量聲明、變量聲明、函數(shù)聲明、類聲明等。在Blanchet演算中，不存在與SubSwift中import語句對應(yīng)的語句，因此，若安全協(xié)議SubSwift語言實施轉(zhuǎn)換為Blanchet演算模型的過程中遇到import語句，則直接跳過。

圖5 SubSwift語言聲明語句到Blanchet演算的BNF映射關(guān)系

圖6 SubSwift語言基本語句到Blanchet演算的BNF映射關(guān)系

4.2 SubSwift語言到Blanchet演算的類型映射

SubSwift語言和Blanchet演算是強類型語言，兩者的主要區(qū)別在于，SubSwift語言中的基本類型如整型int、單精度浮點型float、雙精度浮點型double等都是SubSwift語言預(yù)先定義的；而在Blanchet演算中，除與密碼體制、簽名機制相關(guān)的部分?jǐn)?shù)據(jù)類型是由Blanchet演算預(yù)先定義的之外，其他類型是先聲明后使用的。因此，在定義SubSwift語言到Blanchet演算的類型映射關(guān)系時，主要考慮以下2個方面：1) 對SubSwift語言中的基本數(shù)據(jù)類型，在Blanchet演算中聲明一個同名的數(shù)據(jù)類型，直接進行調(diào)用；2) SubSwift語言中與密碼體制、簽名機制相關(guān)的數(shù)據(jù)類型需映射到Blanchet演算中對應(yīng)的密碼體制、簽名機制中的數(shù)據(jù)類型。

5 Blanchet演算實施生成工具SubSwift2CV

根據(jù)第4節(jié)定義的SubSwift語言到Blanchet演算的映射模型，Blanchet演算實施首先基于計算模型，提出安全協(xié)議SubSwift語言實施生成安全協(xié)議Blanchet演算實施的方法，如圖7所示。然后利用Antrl4[34]工具和Java開發(fā)安全協(xié)議Blanchet演算實施生成工具SubSwift2CV。

圖7 安全協(xié)議Blanchet演算實施生成工具開發(fā)模型

Antrl4工具能夠讀取、處理、執(zhí)行或翻譯二進制文件或結(jié)構(gòu)化文本，被廣泛應(yīng)用于構(gòu)建各類語言、工具和框架。Antrl4工具的監(jiān)聽器Listener機制將語法和語言應(yīng)用進行隔離，用戶只需在語法關(guān)系匹配短語開始和結(jié)束時添加相應(yīng)的動作即可獲取指定形式的數(shù)據(jù)。因此應(yīng)用Antrl4工具及其監(jiān)聽器Listener來開發(fā)生成工具SubSwift2CV，詳細(xì)過程如圖8所示。首先根據(jù)SubSwift語言的BNF，應(yīng)用Antrl4工具開發(fā)SubSwift語言詞法分析器和語法分析器。然后輸入安全協(xié)議SubSwift語言實施，并用詞法分析器和語法分析器對其進行詞法分析和語法分析，得到安全協(xié)議SubSwift語言實施語法分析樹。再用SubSwift語言到Blanchet演算語言的映射關(guān)系，遍歷所獲取的安全協(xié)議SubSwift語言實施語法分析樹，生成安全協(xié)議Blanchet演算實施。最后根據(jù)Blanchet演算語法規(guī)則完善生成的安全協(xié)議Blanchet演算實施。

圖8 SubSwift2CV開發(fā)過程

5.1 安全協(xié)議SubSwift語言實施語法分析

應(yīng)用Antrl4工具對安全協(xié)議SubSwift語言實施進行語法分析，并獲取安全協(xié)議SubSwift語言實施語法分析樹。首先根據(jù)SubSwift語言的詞法規(guī)則開發(fā)SubSwift語言詞法分析器并對安全協(xié)議SubSwift語言實施進行詞法分析，進而得到安全協(xié)議SubSwift語言實施的詞法元素序列。然后根據(jù)SubSwift語言的語法規(guī)則開發(fā)SubSwift語言語法分析器，對獲得的安全協(xié)議SubSwift語言實施詞法元素序列進行語法分析，判斷安全協(xié)議SubSwift語言實施是否符合SubSwift語言語法規(guī)則，若符合，則生成安全協(xié)議SubSwift語言實施的語法分析樹。SubSwift語言詞法分析器和語法分析器開發(fā)原理如圖9所示。

圖9 SubSwift語言語法分析器開發(fā)原理

為開發(fā)SubSwift語言詞法分析器和語法分析器，創(chuàng)建SubSwift.g4文件并存入 SubSwift語言的詞法規(guī)則和語法規(guī)則。執(zhí)行SubSwift.g4文件生成的語法分析相關(guān)文件。SubSwiftLexer.java 是SubSwift詞法分析器，將SubSwift代碼轉(zhuǎn)換為單詞元素序列。SubSwiftParser.java是SubSwift語法分析器，對單詞元素序列進行語法分析。SubSwift BaseListener.java由監(jiān)聽器Listener默認(rèn)實現(xiàn)。

5.1.1 SubSwift語言詞法分析器

圖10 SubSwift語言中的整形詞法規(guī)則

關(guān)鍵字是程序語言中具有固定意義的標(biāo)識符，這些標(biāo)識符只能作為保留字，不能被重新定義為一般標(biāo)識符。在SubSwift語言中，定義的關(guān)鍵字如圖11所示。

圖11 SubSwift語言中的關(guān)鍵字

安全協(xié)議SubSwift實施中標(biāo)識符是程序語言中用來表示安全協(xié)議實體的字符串，如變量名、函數(shù)名、類名等。標(biāo)識符通常由字母、數(shù)字和下劃線組成，且不能以數(shù)字開頭，SubSwift語言中標(biāo)識符的詞法規(guī)則如下。

運算符一般分為算術(shù)運算符、邏輯運算符、賦值運算符、關(guān)系運算符及連接運算符。在Blanchet演算中，只有賦值運算和邏輯運算，因此主要考慮SubSwift語言運算符中的賦值運算符和邏輯運算符。SubSwift語言中運算符的定義如圖12所示。

分界符是程序語言中一個重要組成部分，通常包括括號、分號、冒號、下劃線等。SubSwift語言的分界符定義如圖13所示。

圖13 SubSwift語言中的分界符

在SubSwift語言代碼中，有些代碼如空格、換行符、注釋等在詞法分析中可忽略，其具體詞法規(guī)則定義如下。

WS : [ ]+-> channel(HIDDEN) ;

block_comment : '/*' (block_comment|.)*? '*/'-> channel(HIDDEN) ;

line_comment :'//'.*? (' '|EOF)->channel(HIDDEN)

其中，WS的作用是忽略換行符、空格、制表符，Block_comment中定義的是多行注釋，line_comment中定義的是單行注釋，channel(HIDDEN)的作用是跳過這些字符。

5.1.2 SubSwift語言語法分析器

SubSwift語言語法分析器的輸入是經(jīng)詞法分析器后所得到的單詞元素序列。根據(jù)給定的形式文法分析并確定單詞元素序列的語法組織結(jié)構(gòu)，判斷源程序代碼語法的正確性，若源程序在語法組織結(jié)構(gòu)上正確，則生成語法分析樹。

根據(jù)Antrl4工具的文法定義規(guī)則，在SubSwift.g4文件中添加定義的SubSwift語言的語法規(guī)則，編譯執(zhí)行之后生成的SwiftParser.java文件，即為SubSwift語言語法分析器。SubSwift的BNF，主要包括表達式語句、聲明語句、分支語句和控制轉(zhuǎn)換語句，根據(jù)SubSwift中語句的語法規(guī)范，SubSwift.g4文件的文法規(guī)則定義如下。

SubSwift語言主要關(guān)注的聲明語句有導(dǎo)入聲明、常量聲明、變量聲明、函數(shù)聲明及類聲明。Sub Swift.g4文件中聲明語句的文法規(guī)則定義如圖14所示。

圖14 SubSwift.g4中聲明語句的文法規(guī)則

在SubSwift語言中，除表達式語句、聲明語句之外，其他語句還包括分支語句和控制轉(zhuǎn)換語句，其中，分支語句主要包括if語句和guard語句，控制轉(zhuǎn)換語句主要包括return語句和throw語句，在SubSwift.g4文件中，文法規(guī)則定義如下。

5.2 安全協(xié)議Blanchet演算實施生成

5.2.1 遍歷安全協(xié)議SubSwift語言實施語法分析樹

用ParseTreeWalker類遍歷安全協(xié)議SubSwift語言實施語法分析樹。Antrl4工具的語法分析器編譯SubSwift.g4文件時，會根據(jù)定義的SubSwift語言語法規(guī)則自動化生成語法樹監(jiān)聽器ParseTree Listener接口的子接口SwiftListener及其默認(rèn)實現(xiàn)SwiftBaseListener，其中包含SubSwift語言語法中每個規(guī)則對應(yīng)的Enter方法和Exit方法。采用深度優(yōu)先遍歷SubSwift語言語法分析樹。當(dāng)樹遍歷器遇到SubSwift語言某個語法規(guī)則節(jié)點時，就會調(diào)用該規(guī)則所對應(yīng)的Enter方法，并將該語法樹節(jié)點的上下文傳遞給該規(guī)則對應(yīng)的上下文對象；當(dāng)樹遍歷器遍歷完這個節(jié)點下所有的子節(jié)點之后，就會調(diào)用該規(guī)則對應(yīng)的Exit方法。

5.2.2 生成Blanchet演算實施

用Antrl4工具對SubSwift語句進行分析得到的語法分析樹無法按照傳統(tǒng)的方法通過對語法分析樹的節(jié)點進行移動、刪除或添加等操作來獲得與之對應(yīng)的Blanchet演算語法樹，進而獲得Blanchet演算語句。故采用Antrl4工具中特有的方式——注解語法樹來獲取Blanchet演算語句。

注解SubSwift語法分析樹是為了將SubSwift語句對應(yīng)的Blanchet演算語句存儲在該SubSwift語句語法分析樹的根節(jié)點中，只要訪問根節(jié)點對應(yīng)的映射值即可獲得某條SubSwift語句所對應(yīng)的Blanchet演算語句。

注解SubSwift語法分析樹的具體方法是：通過使用ParseTreeProperty類型的字段cv及幫助方法getCV()、setCV()，得到SubSwift語言輸入短語所對應(yīng)的Blanchet演算語句。在SubSwift語法分析樹中，首先，將每棵子樹轉(zhuǎn)換為Blanchet演算語句，然后，把相關(guān)字符串關(guān)聯(lián)在該子樹的根節(jié)點上，在更高節(jié)點上捕獲這些關(guān)聯(lián)的字符串來獲取更大的字符串，并關(guān)聯(lián)在該節(jié)點上，最后，整個語句的根節(jié)點所關(guān)聯(lián)的字符串即為整個語句轉(zhuǎn)換為Blanchet演算后的結(jié)果。在SubSwift2CV.java文件中，定義轉(zhuǎn)換器類CVEmitter、字段cv和幫助方法getCV()、setCV()，getCV()用于獲取與當(dāng)前根節(jié)點所關(guān)聯(lián)的字符串值，setCV()用于注解當(dāng)前根節(jié)點，其代碼如下。

public static class CVEmitter extends SwiftBase- Listener {

ParseTreeProperty cv =

new ParseTreeProperty();

String getCV(ParseTree ctx) { return cv.get (ctx); }

void setCV(ParseTree ctx, String s) { cv.put (ctx, s); }

5.3 SubSwift2CV界面設(shè)計與功能說明

SubSwift2CV的主要功能包括：首先接收SubSwift語言實施并進行詞法分析、語法分析，進而輸出該SubSwift語言實施的語法分析樹，最后遍歷SubSwift語言實施的語法分析樹，根據(jù)所建立的安全協(xié)議SubSwift語言到Blanchet演算的轉(zhuǎn)換模型，生成并輸出該SubSwift語言實施所對應(yīng)的Blanchet演算實施。SubSwift2CV界面主要包括3個區(qū)域，分別是顯示輸入的SubSwift語言實施、SubSwift語言實施的語法分析樹結(jié)構(gòu)及對應(yīng)的Blanchet演算實施。其界面設(shè)計如圖15所示。

圖15 SubSwift2CV的界面

6 應(yīng)用案例

應(yīng)用SubSwift2CV和CryptoVerif分析OpenID Connect協(xié)議[35]、Oauth2.0協(xié)議[36]、TLS協(xié)議[37]的SubSwift語言實施安全性，其原理如圖16所示。

圖16 分析安全協(xié)議SubSwift實施安全性的框架

由圖16可知，分析安全協(xié)議SubSwift語言實施安全性的主要思路為：首先，得到安全協(xié)議SubSwift語言實施；然后，將其導(dǎo)入SubSwift2CV中，生成安全協(xié)議Blanchet演算實施，最后，將該Blanchet演算實施轉(zhuǎn)化為CryptoVeirf的輸入，進而應(yīng)用CryptoVeirf分析其安全性。下面以O(shè)penID Connect安全協(xié)議SubSwift語言實施安全性分析為例，詳細(xì)說明應(yīng)用SubSwift2CV和CryptoVeirf分析安全協(xié)議SubSwift語言實施安全性的過程。

6.1 OpenID Connect安全協(xié)議SubSwift語言實施安全性分析

OpenID Connect安全協(xié)議包含客戶端（client）、終端用戶（end-user）和OpenID供應(yīng)商（OpenID provider）3個主體。 OpenID Connect協(xié)議可通過隱式流（implicit flow）、授權(quán)碼流（authorization code flow）和混合流（hybrid flow）3種方式進行身份認(rèn)證，不同的方式?jīng)Q定ID Token和Access Token返回到客戶端的方式不同，其消息流程也會有所區(qū)別。本文選擇授權(quán)碼流的方式進行身份認(rèn)證，ID Token和Access Token從令牌終端中返回，客戶端可以利用授權(quán)服務(wù)器發(fā)送的授權(quán)碼向令牌終端請求ID Token和Access Token，這種方式可有效防止令牌泄露。OpenID Connect協(xié)議的消息結(jié)構(gòu)如圖17所示。

圖17 OpenID Connect協(xié)議消息結(jié)構(gòu)

授權(quán)碼流進行身份驗證的客戶端首先將用戶名、密碼和重定向URL發(fā)送給OpenID供應(yīng)商，然后接收OpenID供應(yīng)商的公鑰，最后收到來自O(shè)penID供應(yīng)商的令牌響應(yīng)。因為令牌響應(yīng)中的ID Token經(jīng)過數(shù)字簽名，客戶端收到令牌響應(yīng)之后，需要驗證該數(shù)字簽名，若驗證結(jié)果為真，則表明客戶端能認(rèn)證OpenID供應(yīng)商若驗證為所示時。其中OpenID供應(yīng)商首先要生成公鑰和私鑰，并在客戶端發(fā)送令牌響應(yīng)時使用生成的私鑰對ID Token進行數(shù)字簽名。當(dāng)OpenID供應(yīng)商收到客戶端發(fā)送的身份信息時，將產(chǎn)生的公鑰發(fā)送給客戶端。當(dāng)OpenID供應(yīng)商收到發(fā)自客戶端的令牌請求時，對客戶端的身份信息進行驗證，驗證成功后生成ID Token和Access Token及相關(guān)參數(shù)，并向客戶端發(fā)送令牌響應(yīng)，執(zhí)行OpenID Connect安全協(xié)議OpenID供應(yīng)商、客戶端SubSwift語言實施。結(jié)果如圖18所示。結(jié)果表明客戶端能夠認(rèn)證OpenID供應(yīng)商。

圖18 OpenID Connect協(xié)議SubSwift語言實施安全性分析結(jié)果

6.2 OpenID Connect安全協(xié)議Blanchet演算生成及其安全性分析

首先，將獲取的安全協(xié)議SubSwift語言實施輸入SubSwift2CV。然后，經(jīng)過詞法分析及語法分析，進而生成安全協(xié)議SubSwift實施語法分析樹，遍歷語法分析樹，從而生成安全協(xié)議Blanchet演算實施。最后，將生成的安全協(xié)議Blanchet演算實施轉(zhuǎn)換為CryptoVerif工具的輸入進而分析其安全性，同時獲得其安全性分析結(jié)果。

實驗采用的OpenID Connect源碼[38]是由Aero Gear項目提供的，該項目致力于將企業(yè)與移動端結(jié)合起來使跨平臺企業(yè)移動開發(fā)變得容易，目前，該項目獲得Twitter、Facebook 、Google等公司支持，分析該項目的OpenID Connect實施對網(wǎng)絡(luò)空間安全具有重要意義。

OpenID Connect安全協(xié)議將OpenID供應(yīng)商、客戶端SubSwift語言實施分別導(dǎo)入SubSwift2CV工具中，輸出結(jié)果如圖19和圖20所示。整理SubSwift2CV工具生成的OpenID Connect安全協(xié)議Blanchet演算實施，并將其轉(zhuǎn)化為CryptoVerif語句后輸入Crypto Verif工具中，進而得到的安全性分析結(jié)果如圖21所示。結(jié)果表明客戶端能夠認(rèn)證OpenID供應(yīng)商。

圖19 OpenID供應(yīng)商Blanchet演算實施結(jié)果

圖20 OpenID客戶端Blanchet演算實施

圖21 OpenID Connect協(xié)議Blanchet演算實施安全性分析結(jié)果

6.3 Oauth2.0和TLS安全協(xié)議SubSwift語言實施安全性分析

用同樣的方法，對Oauth2.0安全協(xié)議SubSwift語言實施和生成的Blanchet演算實施的安全性分別進行分析，結(jié)果如圖22和圖23所示。

圖22 Oauth2.0協(xié)議SubSwift語言實施安全性分析結(jié)果

圖23 Oauth2.0協(xié)議Blanchet演算實施安全性分析結(jié)果

由圖22和圖23可知，Oauth2.0協(xié)議SubSwift語言實施和Blanchet演算實施的安全性分析結(jié)果是一致的，這表明客戶端無法認(rèn)證授權(quán)服務(wù)器，即當(dāng)客戶端收到授權(quán)碼時不能夠確定該授權(quán)碼是否來自授權(quán)服務(wù)器。因為授權(quán)服務(wù)器向客戶端發(fā)送授權(quán)碼的過程中，沒有采用數(shù)字簽名機制，所以攻擊者能獲得其授權(quán)碼，并對其進行篡改。

同樣地，對TLS安全協(xié)議SubSwift語言實施和生成的Blanchet演算實施的安全性分別進行分析，結(jié)果如圖24和圖25所示。

圖24 TLS協(xié)議SubSwift語言實施安全性分析結(jié)果

圖25 TLS協(xié)議Blanchet演算實施安全性分析結(jié)果

由圖24和圖25可知，TLS安全協(xié)議SubSwift語言實施和Blanchet演算實施的安全性分析結(jié)果是一致的，這表明在客戶端與服務(wù)器通信的過程中，能夠保證預(yù)主密鑰的保密性，且客戶端能夠認(rèn)證服務(wù)器。

7 結(jié)束語

基于計算模型對IOS平臺上的安全協(xié)議Swift語言實施的安全性進行分析，對保障IOS應(yīng)用安全具有重要意義。首先對已有的安全協(xié)議Swift語言實施進行分析，進而確定與安全協(xié)議Swift實施緊密相關(guān)的Swift語言子集SubSwift。然后根據(jù)操作語義，建立從SubSwift語言到Blanchet演算的映射模型，提出從安全協(xié)議SubSwift語言實施中抽取安全協(xié)議Blanchet演算實施的方法，并開發(fā)安全協(xié)議Blanchet演算實施生成工具SubSwift2CV，同時對OpenID Connect協(xié)議、Oauth2.0協(xié)議及TLS協(xié)議的安全性進行分析。結(jié)果表明OpenID Connect協(xié)議、Oauth2.0協(xié)議和TLS協(xié)議的SubSwift語言實施與安全協(xié)議Blanchet演算實施的安全性分析結(jié)果分別是“客戶端能夠認(rèn)證OpenID供應(yīng)商”和“客戶端無法認(rèn)證授權(quán)服務(wù)器”。在SubSwift客戶端與服務(wù)器通信過程中能夠保證預(yù)置密鑰保密性，且客戶端能認(rèn)證服務(wù)器端。

開發(fā)的安全協(xié)議Blanchet演算實施生成工具SubSwift2CV不是復(fù)雜的編譯器，故在當(dāng)前的版本中存在優(yōu)化等問題。未來計劃展開以下4個方面的工作：1) 對SubSwift語言進行擴充，使其包含更多語句和特征；2) 基于互模擬技術(shù)，應(yīng)用Coq來證明SubSwift2CV工具的正確性；3) 使用SubSwift2CV和CryptoVerif分析更多的安全協(xié)議SubSwift實施的安全性；4) 把本文提出的模型抽取方法和映射模型進行推廣，分析IOS平臺上大量存在的安全協(xié)議Object C語言實施的安全性。

[1] 張煥國, 韓文報, 來學(xué)嘉, 等. 網(wǎng)絡(luò)空間安全綜述[J]. 中國科學(xué):信息科學(xué), 2016, 46(2): 125-164.

ZHANG H G, HAN W B, LAI X J, et al. Survey on cyberspace security[J]. SCIENTIA SINICA Informationis, 2016, 46(2): 125-164.

[2] 王世偉. 論信息安全、網(wǎng)絡(luò)安全、網(wǎng)絡(luò)空間安全[J]. 中國圖書館學(xué)報, 2015(2):72-84.

WANG S W. On information security, network security and cyberspace security[J]. Journal of Library Science in China, 2015(2):72-84.

[3] MIN K S, CHAI S W, HAN M. An international comparative study on cyber security strategy[J]. International Journal of Security and its Applications, 2015, 9(2):13-20.

[4] 張煥國, 吳福生, 王后珍, 等. 密碼協(xié)議代碼執(zhí)行的安全驗證分析綜述[J]. 計算機學(xué)報, 2018,41(2): 288-308.

ZHANG H G, WU F S, WANG H Z, et al. A survey: security verification analysis of cryptographic protocols implementations on real code[J]. Chinese Journal of Computers, 2018, 41(2): 288-308.

[5] 孟博, 張金麗, 魯金鈿. 基于計算模型的OpenID Connect協(xié)議認(rèn)證性的自動化分析[J]. 中南大學(xué)民族大學(xué)學(xué)報（自然科學(xué)版）, 2016,35(3): 123-129.

MENG B, ZHANG J L, LU J T. Automatic analysis of authentication of OpenID Connect protocol based on the computational model[J]. Journal of South-Central University for Nationalities (Natural Science Edition), 2016, 35(3): 123-129.

[6] 牛樂園, 楊伊彤, 王德軍, 等. 計算模型下的SSHV2協(xié)議認(rèn)證性自動化分析[J]. 計算機工程, 2015, 41(10): 148-154.

NIU L Y, YANG Y T, WANG D J, et al. Automatic analysis on authentication of SSHV2 protocol in computational model[J]. Computer Engineering, 2015, 41(10): 148-154.

[7] AVALLE M, PIRONTI A, SISTO R. Formal verification of security protocol implementations: a survey[J]. Formal Aspects of Computing, 2014, 26(1): 99-123.

[8] MENG B, HUANG C T,YANG Y T, et al. Automatic generation of security protocol implementations written in Java from abstract specifications proved in the computational model[J]. International Journal of Network Security, 2017,19(1): 138-153.

[9] MENG B, YANG Y T, ZHANG J L, et al. PV2Java: automatic generator of security protocol implementations written in Java language from the applied PI calculus proved in the symbolic model[J]. International Journal of Security and its Applications, 2016, 10(11): 211-229.

[10] 孟博, 王德軍.安全協(xié)議實施自動化生成與驗證[M]. 北京: 科學(xué)出版社, 2016.

MENG B, WANG D J. Automatic generation and verification of security protocols’ implements[M]. Beijing: Science Press, 2016.

[11] 雷新鋒, 宋書民, 劉偉兵, 等. 計算可靠的密碼協(xié)議形式化分析綜述[J]. 計算機學(xué)報, 2014, 37(5): 993-1016.

LEI X F, SONG S M, LIU W B, et al. A Survey on computationally sound formal analysis of cryptographic protocols[J]. Chinese Journal of Computers, 2014, 37(5): 993-1016.

[12] GOUBAULT L J, PARRENNES F. Cryptographic protocol analysis on real C code[C]//International Workshop on Verification, Model Checking, and Abstract Interpretation. 2005: 363-379.

[13] JURJENS J. Automated security verification for crypto protocol implementations: verifying the JESSIE project[J]. Electronic Notes in Theoretical Computer Science, 2009, 250(1): 123-136.

[14] CHAKI S, DATTA A. ASPIER: an automated framework for verifying security protocol implementations[C]//22nd IEEE Computer Security Foundations Symposium. 2009:172-185.

[15] DUPRESSOIR F, GORDON A D, JüRJENS J, et al. Guiding a general-purpose C verifier to prove cryptographic protocols[C]// 24th IEEE Computer Security Foundations Symposium. 2011:3-17.

[16] BHARGAVAN K, GORDON A D. Modular verification of security protocol code by typing[C]//ACM Sigplan-Sigact Symposium on Principles of Programming Languages. 2010:445-456.

[17] BACKES M, MAFFEI M, UNRUH D. Computationally sound verification of source code[C]// 17th ACM Conference on Computer and Communications Security. 2010:387-398.

[18] BENGTSON J, BHARGAVAN K, FOURNET C, et al. Refinement types for secure implementations[J]. ACM Transactions on Programming Languages and Systems, 2011, 33(2): 8-45.

[19] SWAMY N, CHEN J, FOURENT C, et al. Secure distributed programming with value-dependent types[C]]// 16th ACM Sigplan International Conference on Functional Programming. 2011:266-278.

[20] SWAMY N, HRI?CU C, KELLER C, et al. Semantic purity and effects reunited in F*[C]// 20th ACM SIGPLAN International Conference on Functional Programming. New York: ACM, 2015:12.

[21] SWAMY N, HRI?CU C, KELLER C, et al. Dependent types and multi-monadic effects in F*[C]// 43rd annual ACM SIGPLAN- SIGACT Symp on Principles of Programming Languages. 2016: 256-270.

[22] BHARGAVAN K, FOURNET C, GORDON A D, et al. Verified interoperable implementations of security protocols[J]. ACM Transactions on Programming Languages and Systems. 2008, 31(1): 5.

[23] BHARGAVAN K, CORIN R, FOURNET C, et al. Automated computational verification for cryptographic protocol implementations[J]. Unpublished draft, Oct, 2009.

[24] BHARGAVAN K, FOURNET C, CORIN R, et al. Cryptographically verified implementations for TLS[C]// 15th ACM Conference on Computer and Communications Security. 2008:459-468.

[25] MIHHAIL A, GORDON A D, JüRJENS J. Extracting and verifying cryptographic models from C protocol code by symbolic execution[C]//18th ACM Conference on Computer and Communications Security. 2011: 331-340.

[26] AIZATULIN M, GORDON A D, JURJENS J. Computational verification of C protocol implementations by symbolic execution[C]//19th ACM Conference on Computer and Communications Security. 2012: 712-723.

[27] BHARGAVAN K, BLANCHET K,KOBEISSI N. Verified models and reference implementations for the TLS 1.3 standard candidate[C]// 38th IEEE Symp on Security and Privacy. 2017:20.

[28] BLANCHET B. A computationally sound mechanized prover for security protocols[J]. IEEE Transactions on Dependable and Secure Computing, 2008, 5(4):193-207.

[29] BLANCHET B. An efficient cryptographic protocol verifier based on prolog rules[C]//14th IEEE Computer Security Foundations Workshop, Cape Breton.2001:82-96.

[30] O'SHEA N. Using ELYJAH to analyses Java implementations of cryptographic protocols[C]// FCS-ARSPA-WITS'08. 2008: 211-223.

[31] LI Z M, MENG B, WANG D J, et al. Mechanized verification of cryptographic security of cryptographic security protocol implementation in JAVA through model extraction in the computational model[J]. Journal of Software Engineering, 2015, 9(1): 1-32.

[32] 唐朝京, 魯智勇, 馮超. 基于計算語義的安全協(xié)議驗證邏輯[J]. 電子學(xué)報, 2014, 42(6):1179-1185.

TANG Z J, LU Z Y, FENG C. A verification logic for security protocols based on computational semantics[J]. Chinese Journal of Electronics, 2014, 42(6):1179-1185.

[33] Apple Inc. The Swift Programming Language[EB/OL]. [2017-4-1]

[34] TERENCE P. The definitive Antrl4 reference[M]. USA: The Pragmatic Bookshelf, 2012

[35] SAKIMURA N, BRADLEY J, JONES M, et al. OpenID connect core 1.0[EB/OL].[2017-1-10]

[36] XU X D, NIU L Y, MENG B. Automatic verification of security properties of OAuth 2.0 protocol with CryptoVerif in computational model[J]. Information Technology Journal, 2013, 12(12): 2273-2285.

[37] MENG B, NIU L Y, YANG Y T, et al. Mechanized verification of security properties of transport layer security 1.2 protocol with CryptoVerif in computational model[J]. Information Technology Journal, 2014, 13(4): 601-613.

[38] Client library for OAuth2/OpenID Connect [EB/OL]. [2016-10-1].

Security analysis of security protocol Swift implementations based on computational model

MENG Bo, HE Xudong, ZHANG Jinli, YAO Lili, LU Jintian

College of Computer Science, South Central University For Nationalities,Wuhan 430074, China

Analysis of security protocol Swift implementations in IOS platform is important to protect the security of IOS applications. Firstly, according to the security protocol Swift implementations, the SubSwift language, which was a subset of Swift language, was widely used in IOS system, and its BNF were specified. Secondly, the mapping model from SubSwift language to Blanchet calculus based on the operational semantic was presented which consisted of mapping rules, relationship from the statements and types in SubSwift language to Blanchet calculus. And then, a method of generating security protocol Blanchet calculus implementations from SubSwift language implementations was developed. Finally, security protocol Blanchet calculus implementation generation tool SubSwift2CV was developed with Antrl4 and Java language. At the same time, OpenID Connect, Oauth2.0 and TLS security protocol SubSwift language implementations were analyzed with SubSwift2CV and CryptoVerif.

security protocol, implementations security, Swift language, formal analysis, model extraction

TP309

A

10.11959/j.issn.1000?436x.2018165

孟博（1974-），男，河北行唐人，博士，中南民族大學(xué)教授、碩士生導(dǎo)師，主要研究方向為安全協(xié)議和形式化方法。

何旭東（1991-），男，湖北武漢人，中南民族大學(xué)碩士生，主要研究方向為安全協(xié)議實施安全。

張金麗（1991-），女，湖北隨州人，中南民族大學(xué)碩士生，主要研究方向為安全協(xié)議實施安全。

堯利利（1993-），女，江西撫州人，中南民族大學(xué)碩士生，，主要研究方向為安全協(xié)議實施安全

魯金鈿（1991-），男，土家族，湖南湘西人，中南民族大學(xué)碩士生，主要研究方向為形式化方法和安全協(xié)議逆向分析。

2017?07?21；

2018?07?23

孟博，mengscuec@gmail.com

國家自然科學(xué)基金資助項目（No.61272497）；湖北省自然科學(xué)基金資助項目（No.2014CFB249, No.2018ADC150）；中南民族大學(xué)中央高?；究蒲袠I(yè)務(wù)費專項資金資助項目（No.CZZ18003, No.QSZ17007）

The National Natural Science Foundation of China (No.61272497), The Natural Science Foundation of Hubei Province (No.2014CFB249, No.2018ADC150), The Central University Basic Business Expenses Special Funding for Scientific Research Project (No.CZZ18003, No.QSZ17007)