基于计算模型的安全协议Swift语言实施安全性分析

doi:10.11959/j.issn.1000-436x.2018165

通信学报 ›› 2018, Vol. 39 ›› Issue (9): 178-190.doi: 10.11959/j.issn.1000-436x.2018165

• 论文Ⅲ：学术论文 • 上一篇

基于计算模型的安全协议Swift语言实施安全性分析

孟博(),何旭东,张金丽,尧利利,鲁金钿

中南民族大学计算机科学学院，湖北武汉 430074

修回日期:2018-07-23 出版日期:2018-09-01 发布日期:2018-10-19
作者简介:孟博（1974-），男，河北行唐人，博士，中南民族大学教授、硕士生导师，主要研究方向为安全协议和形式化方法。|何旭东（1991-），男，湖北武汉人，中南民族大学硕士生，主要研究方向为安全协议实施安全。|张金丽（1991-），女，湖北随州人，中南民族大学硕士生，主要研究方向为安全协议实施安全。|尧利利（1993-），女，江西抚州人，中南民族大学硕士生，，主要研究方向为安全协议实施安全|鲁金钿（1991-），男，土家族，湖南湘西人，中南民族大学硕士生，主要研究方向为形式化方法和安全协议逆向分析。
基金资助:
国家自然科学基金资助项目(61272497);湖北省自然科学基金资助项目(2014CFB249);湖北省自然科学基金资助项目(2018ADC150);中南民族大学中央高校基本科研业务费专项资金资助项目(CZZ18003);中南民族大学中央高校基本科研业务费专项资金资助项目(QSZ17007)

Security analysis of security protocol Swift implementations based on computational model

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

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

Revised:2018-07-23 Online:2018-09-01 Published:2018-10-19
Supported by:
The National Natural Science Foundation of China(61272497);The Natural Science Foundation of Hubei Province(2014CFB249);The Natural Science Foundation of Hubei Province(2018ADC150);The Central University Basic Business Expenses Special Funding for Scientific Research Project(CZZ18003);The Central University Basic Business Expenses Special Funding for Scientific Research Project(QSZ17007)

摘要/Abstract

摘要：

分析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语言, 形式化分析, 模型抽取

Abstract:

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.

Key words: security protocol, implementations security, Swift language, formal analysis, model extraction

中图分类号:

TP309

孟博,何旭东,张金丽,尧利利,鲁金钿. 基于计算模型的安全协议Swift语言实施安全性分析[J]. 通信学报, 2018, 39(9): 178-190.

Bo MENG,Xudong HE,Jinli ZHANG,Lili YAO,Jintian LU. Security analysis of security protocol Swift implementations based on computational model[J]. Journal on Communications, 2018, 39(9): 178-190.

图/表 25

图1

图2

图3

图4

图5

图6

图7

图8

图9

图10

图11

图12

图13

图14

图15

图16

图17

图18

图19

图20

图21

图22

图23

图24

图25

参考文献 38

[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 PressPress, 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 . Dependent types and multi-monadic effects in F*[C]// 43rd annual ACM SIGPLANSIGACT 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]	SONY Corporation. The Swift Programming Language[EB/OL].[2017-4-1]
[34]	TERENCE P . The definitive Antrl4 reference[M]. USA: The Pragmatic BookshelfPress, 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].

基于计算模型的安全协议Swift语言实施安全性分析

Security analysis of security protocol Swift implementations based on computational model

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 25

参考文献 38

相关文章 15

Metrics

推荐阅读 0

[1]	龚翔, 冯涛, 杜谨泽. 基于CPN的安全协议形式化建模及安全分析方法[J]. 通信学报, 2021, 42(9): 240-253.
[2]	朱辉,武衡,赵海强,赵玉清,李晖. 适用于双层卫星网络的星间组网认证方案[J]. 通信学报, 2019, 40(3): 1-9.
[3]	谷文,韩继红,袁霖. SSMCI：以攻击者为中心的安全协议验证机制[J]. 通信学报, 2017, 38(10): 175-188.
[4]	杨京,范丹,张玉清. 改进的安全协议自适应分析算法[J]. 通信学报, 2015, 36(Z1): 266-276.
[5]	李永凯,刘树波,杨召唤,刘梦君. 机会网络中用户属性隐私安全的高效协作者资料匹配协议[J]. 通信学报, 2015, 36(12): 163-171.
[6]	朱玉娜，韩继红，袁霖，陈韩托，范钰丹. 基于主体行为的多方安全协议会话识别方法[J]. 通信学报, 2015, 36(11): 190-200.
[7]	顾纯祥，王焕孝，郑永辉，辛丹，刘楠. 基于SAT的安全协议惰性形式化分析方法[J]. 通信学报, 2014, 35(11): 13-116.
[8]	焦政达，马建峰，孙聪，姚青松. 新的车辆远程诊断授权协议[J]. 通信学报, 2014, 35(11): 17-154.
[9]	顾纯祥,王焕孝,郑永辉,辛丹,刘楠. 基于SAT的安全协议惰性形式化分析方法[J]. 通信学报, 2014, 35(11): 117-125.
[10]	焦政达,马建峰,孙聪,姚青松. 新的车辆远程诊断授权协议[J]. 通信学报, 2014, 35(11): 146-153.
[11]	刘礼才1,2，殷丽华2，郭云川2，孙燕1,2. 基于CSP方法的移动自组织网络认证协议TAM的分析与改进[J]. 通信学报, 2013, 34(Z1): 8-66.
[12]	刘礼才,殷丽华,郭云川,孙燕. 基于CSP方法的移动自组织网络认证协议TAM的分析与改进[J]. 通信学报, 2013, 34(Z1): 58-66.
[13]	许金超,曾国荪,王伟. 基于软件水印的云平台下软件服务保护安全协议[J]. 通信学报, 2012, 33(Z2): 176-181.
[14]	韩志耕,陈耿,罗军舟. 多方不可否认协议的增广CSP建模与分析[J]. 通信学报, 2012, 33(Z2): 189-195.
[15]	鲁来凤,段新东,马建峰. Otway-Rees协议改进及形式化证明[J]. 通信学报, 2012, 33(Z1): 250-254.