摘要:形式化方法为安全协议分析提供了理论工具，但经过形式化验证过的协议标准在转换为具体程序实现时，可能无法满足相应的安全属性.为此，提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型，基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明，并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合，能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.
Abstract:Formal method provides a theoretical tool for security protocol analysis, but the theoretical security is not equivalent to the actual security. A verified protocol standard may not meet the required security properties when converted into a concrete program. Hence, a formal verification method for detecting semantic logic errors in security protocol code is proposed. By automatically abstracting the C source code of the protocol into Pi calculus model, protocol security properties are verified based on the Pi calculus. Finally, the correctness of the scheme transformation is proved and the validity of the method is verified by a Kerberos protocol instance code. C2P tools implemented can help protocol developers to detect semantic logic errors in code.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/6238
删除或更新信息，请邮件至freekaoyan#163.com(#换成@)
C2P:基于Pi演算的协议C代码形式化抽象方法和工具
本站小编 Free考研考试/2022-01-02
相关话题/代码 自动化 方案 逻辑 测试
领限时大额优惠券,享本站正版考研考试资料!
优惠券领取后72小时内有效，10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材，产品类型包含电子书、题库、全套资料以及视频，无论您是考研复习、考证刷题，还是考前冲刺等，不同类型的产品可满足您学习上的不同需求。 ...考试优惠券 本站小编 Free壹佰分学习网 2022-09-19基于分支标记的数据流模型的代码生成方法
摘要:模型驱动开发以其低错误率、易仿真、易验证的特点，在嵌入式软件开发中被广泛应用.近年来，基于模型的嵌入式软件开发方法及相应工具也在逐渐发展和完善.数据流模型是各种建模工具中使用最为频繁的语义模型，然而，各种工具对于数据流模型的代码生成能力却参差不齐，特别是对于数据分支组件的支持，当前主流的建模工 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向ROS的差分模糊测试方法
摘要:机器人操作系统（robotoperatingsystem，简称ROS）是一种广泛应用于机器人开发的开源系统，它可以为开发者提供硬件抽象、设备驱动、库函数、可视化、消息传递和软件包管理等诸多功能，应用前景广阔.ROS集成了可以实现不同功能的功能包，例如定位绘图、行动规划、感知、模拟等等，但其中可 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02区块链赋能的高效物联网数据激励共享方案
摘要:近年来，随着大量设备不断地加入物联网中，数据共享作为物联网市场的主要驱动因素成为了研究热点.然而，当前的物联网数据共享存在着出于安全顾虑和缺乏激励机制等原因导致用户不愿意参与共享数据的问题.在此背景下，区块链技术为解决用户的信任问题和提供安全的数据存储被引入到物联网数据共享中.然而，在构建基于 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02一种结构信息增强的代码修改自动转换方法
摘要:在开发过程中，开发人员在进行缺陷修复、版本更新时，常常需要修改多处相似的代码.如何进行自动代码修改已成为软件工程领域的热点研究问题.一种行之有效的方式是：给定一组代码修改示例，通过抽取其中的代码修改模式，辅助相似代码进行自动转换.在现有工作中，基于深度学习的方法取得了一定进展，但在捕获代码间的 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于深度学习的混合模糊测试方法
摘要:随着软件技术的快速发展，面向领域的软件系统在广泛使用的同时带来了研究与应用上的新挑战.由于领域应用对安全性、可靠性有着很高的要求，而符号执行和模糊测试等技术在保障软件系统的安全性、可靠性方面已经发展了数十年，许多研究和被发现的缺陷表明了它们的有效性.但是，由于两者的优劣各有不同，将这两者相结合 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向神经机器翻译系统的多粒度蜕变测试
摘要:机器翻译是利用计算机将一种自然语言转换成另一种自然语言的任务，是人工智能领域研究的热点问题之一.近年来，随着深度学习的发展，基于序列到序列结构的神经机器翻译模型在多种语言对的翻译任务上都取得了超过统计机器翻译模型的效果，并被广泛应用于商用翻译系统中.虽然商用翻译系统的实际应用效果直观表明了神经 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02融合代码与文档的软件功能特征挖掘方法
摘要:在软件复用过程中，简洁、清楚的软件功能自然语言描述是帮助复用者快速了解待复用软件项目/代码库的前提和基础.但当前开源软件往往缺乏高质量的软件功能说明文档，使得这一过程变得更加复杂和困难.为此，提出了一种融合代码与文档的软件功能特征挖掘方法.该方法以动宾短语的形式描述软件功能特征，通过迭代挖掘软 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02一种手绘制导的移动应用界面测试方法
摘要:软件测试在提高移动应用的安全性和可靠性方面扮演着重要角色.然而，目前主流的移动应用界面测试技术存在着许多不足：人工编写脚本和录制回放技术需要消耗大量的人力成本，自动化测试在移动应用界面测试的应用场景上受到了诸多限制.针对这些问题，提出一种基于手绘制导的移动应用界面测试方法.该方法通过设计一种简 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向完美回忆的时态认知逻辑
摘要:传统时态认知逻辑对完美回忆的刻画是狭隘的，并不能完整表达主体记得自己先前的认知状态.新系统S5tCt将认知与时态融合进同一个算子中，个体知识、普遍知识和公共知识都被时间点所标注.S5tCt系统从技术上实现了每个个体（群体）都可以完美回忆自己在之前所有时刻上的认知状态.利用典范模型技术可以证明， ...中科院软件研究所 本站小编 Free考研考试 2022-01-02可修改的区块链方案
摘要:随着区块链的迅速发展，上链数据不仅包括金融交易数据，还包括科技、文化、政治等多类数据.而在现有的区块链系统中，数据一旦上链便无法更改，可能会面临失效数据无法删除、错误数据无法修改等问题.因此，特定条件下可修改的区块链方案具有广阔的应用前景.在POSpace（proofofspace）共识机制下 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02
