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

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

?

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

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

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

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

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

1 引言

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

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

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

本文主要貢獻如下。

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

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

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

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

2 相關工作

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

3 SubSwift語言與Blanchet演算

3.1 SubSwift語言及其BNF

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

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

圖1 SubSwift語言的巴科斯范式

3.2 Blanchet演算及其BNF

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

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

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

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

圖2 Blanchet演算的巴科斯范式

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

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

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

圖5 SubSwift語言聲明語句到Blanchet演算的BNF映射關系

圖6 SubSwift語言基本語句到Blanchet演算的BNF映射關系

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

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

5 Blanchet演算實施生成工具SubSwift2CV

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

圖7 安全協議Blanchet演算實施生成工具開發模型

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

圖8 SubSwift2CV開發過程

5.1 安全協議SubSwift語言實施語法分析

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

圖9 SubSwift語言語法分析器開發原理

為開發SubSwift語言詞法分析器和語法分析器，創建SubSwift.g4文件并存入 SubSwift語言的詞法規則和語法規則。執行SubSwift.g4文件生成的語法分析相關文件。SubSwiftLexer.java 是SubSwift詞法分析器，將SubSwift代碼轉換為單詞元素序列。SubSwiftParser.java是SubSwift語法分析器，對單詞元素序列進行語法分析。SubSwift BaseListener.java由監聽器Listener默認實現。

5.1.1 SubSwift語言詞法分析器

圖10 SubSwift語言中的整形詞法規則

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

圖11 SubSwift語言中的關鍵字

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

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

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

圖13 SubSwift語言中的分界符

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

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語言語法分析器的輸入是經詞法分析器后所得到的單詞元素序列。根據給定的形式文法分析并確定單詞元素序列的語法組織結構，判斷源程序代碼語法的正確性，若源程序在語法組織結構上正確，則生成語法分析樹。

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

SubSwift語言主要關注的聲明語句有導入聲明、常量聲明、變量聲明、函數聲明及類聲明。Sub Swift.g4文件中聲明語句的文法規則定義如圖14所示。

圖14 SubSwift.g4中聲明語句的文法規則

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

5.2 安全協議Blanchet演算實施生成

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

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

5.2.2 生成Blanchet演算實施

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

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

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

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界面設計與功能說明

SubSwift2CV的主要功能包括：首先接收SubSwift語言實施并進行詞法分析、語法分析，進而輸出該SubSwift語言實施的語法分析樹，最后遍歷SubSwift語言實施的語法分析樹，根據所建立的安全協議SubSwift語言到Blanchet演算的轉換模型，生成并輸出該SubSwift語言實施所對應的Blanchet演算實施。SubSwift2CV界面主要包括3個區域，分別是顯示輸入的SubSwift語言實施、SubSwift語言實施的語法分析樹結構及對應的Blanchet演算實施。其界面設計如圖15所示。

圖15 SubSwift2CV的界面

6 應用案例

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

圖16 分析安全協議SubSwift實施安全性的框架

由圖16可知，分析安全協議SubSwift語言實施安全性的主要思路為：首先，得到安全協議SubSwift語言實施；然后，將其導入SubSwift2CV中，生成安全協議Blanchet演算實施，最后，將該Blanchet演算實施轉化為CryptoVeirf的輸入，進而應用CryptoVeirf分析其安全性。下面以OpenID Connect安全協議SubSwift語言實施安全性分析為例，詳細說明應用SubSwift2CV和CryptoVeirf分析安全協議SubSwift語言實施安全性的過程。

6.1 OpenID Connect安全協議SubSwift語言實施安全性分析

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

圖17 OpenID Connect協議消息結構

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

圖18 OpenID Connect協議SubSwift語言實施安全性分析結果

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

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

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

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

圖19 OpenID供應商Blanchet演算實施結果

圖20 OpenID客戶端Blanchet演算實施

圖21 OpenID Connect協議Blanchet演算實施安全性分析結果

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

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

圖22 Oauth2.0協議SubSwift語言實施安全性分析結果

圖23 Oauth2.0協議Blanchet演算實施安全性分析結果

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

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

圖24 TLS協議SubSwift語言實施安全性分析結果

圖25 TLS協議Blanchet演算實施安全性分析結果

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

7 結束語

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

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

[1] 張煥國, 韓文報, 來學嘉, 等. 網絡空間安全綜述[J]. 中國科學:信息科學, 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] 王世偉. 論信息安全、網絡安全、網絡空間安全[J]. 中國圖書館學報, 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] 張煥國, 吳福生, 王后珍, 等. 密碼協議代碼執行的安全驗證分析綜述[J]. 計算機學報, 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協議認證性的自動化分析[J]. 中南大學民族大學學報（自然科學版）, 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協議認證性自動化分析[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] 孟博, 王德軍.安全協議實施自動化生成與驗證[M]. 北京: 科學出版社, 2016.

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

[11] 雷新鋒, 宋書民, 劉偉兵, 等. 計算可靠的密碼協議形式化分析綜述[J]. 計算機學報, 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] 唐朝京, 魯智勇, 馮超. 基于計算語義的安全協議驗證邏輯[J]. 電子學報, 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-），男，河北行唐人，博士，中南民族大學教授、碩士生導師，主要研究方向為安全協議和形式化方法。

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

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

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

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

2017?07?21；

2018?07?23

孟博，mengscuec@gmail.com

國家自然科學基金資助項目（No.61272497）；湖北省自然科學基金資助項目（No.2014CFB249, No.2018ADC150）；中南民族大學中央高校基本科研業務費專項資金資助項目（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)