SET证书申请协议在SPV下的自动化验证及改进

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.

电子商务支付协议认证性的SVO逻辑验证

与证伪法(如模型检测)相比,采用证真法(如定理证明和逻辑推理)能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。

电子商务中时态信息的处理

电子商务随着计算机技术和网络技术的发展快速发展,但是也存在着诸如合同时间认证等安全性问题使其推广受到阻碍。本文针对目前电子商务中数据处理中存在的不足,结合时态数据库的理论和方法,挖掘在电子商务中存在的时态信息,并提出一种利用时态数据库管理电子商务中数据的框架模型。

协议组合逻辑在实例化空间模型中的语义解释

安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价,选择另一种实用的协议组合逻辑PCL,分析了ISL和PCL之间的关系.在此基础上,将PCL的索状空间语义模型转换为ISL的实例化空间语义模型,在实例化空间下对PCL的主要公式、定理、推导规则做了语义解释.研究表明,实例化空间能够完全表示PCL的语义,且ISL的语义表达能力强于PCL.新的模型解释使PCL更易于扩展,且使得用PCL理论验证的协议能够利用ISL的自动化验证工具SPV进行分析.

基于RISC技术的指令流水虚拟系统

文章在“软件模拟硬件”思想指导下 ,实现基于RISC技术的指令流水虚拟机 ,突出介绍了利用VisualC + +的面向对象开发环境实现虚拟机器的基本构思、设计方法和过程 ,在虚拟机的设计和实现中应用了RISC与指令流水线两大技术 .该虚拟机的实现表明 ,在计算机上建立虚拟系统应用于实验、教学和进一步的研究中是具有可行性的 .

汽车巡航控制系统的软件设计与仿真

基于实际的小车模型,使用PIC16F877A单片机、AH3144霍尔传感器等部件,以C语言为软件编程语言,设计实现了一个汽车电控巡航控制模拟系统.首先对系统总体结构进行介绍,然后详细阐述了系统各功能模块的软件设计方案,并对其软件核心控制策略—增量式PID算法进行改进,最后给出了部分程序示例及仿真调试结果.实验结果表明,改进的增量PID算法使系统响应更快,增加了巡航控制的稳定性,整个系统能较好地满足自动巡航的各项功能需求,具有一定的市场应用价值.

有界模型检测的优化

G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值.

电子政务中时态信息的研究

随着计算机技术和网络技术的发展,电子政务在我国开始全面实施。但是其中存在着诸如对信息时效性不能很好地处理等问题,这使其推广受到阻碍。通过分析目前电子政务中信息处理方法的不足,结合时态数据库的理论和方法,提出了一个解决电子政务中信息有效性的处理模型。

基于单片机控制的自动停车收费管理系统

介绍基于89C51单片机的一款临时停车场自动停车收费管理系统,该系统采用比传统停车计费方式更优越的红外线检测计费方式,可以实现自动计费,实时查询、显示停车场状况,打印数据,自动开启关闭车场大门以及随时更改收费标准等功能。该系统操作简单,价格低廉,安装调试方便,很好地解决了临时停车场的管理收费问题。

移动通信模式下压缩感知视频检测技术及其目标重构

为了解决移动通信视频监控的目标追踪问题,提出一种新的空间域视频压缩感知模型,该模型首先通过测量矩阵获取视频少量样本值,然后通过该样本值同时重构运动目标、背景和视频序列,最后通过视频序列估计得到一个置信图,可以进一步提高目标的重构质量。大量的实验证明,该模型与典型的空域检测技术比较,能够降低视频检测的数据量,并有效地重构视频目标,且对运动干扰具有更好的鲁棒性。

有界模型检测和串空间模型相结合的安全协议验证

提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,进行验证,有效减轻状态空间爆炸问题;利用不安全协议丛结构的特点,对BMC的下界进行优化.这种方式结合了模型检测和定理证明的优点,通过典型的安全协议的分析和实验,验证了本方法较传统的模型检测方法在验证安全协议时,验证效率提高明显.

多重中断技术的软件模拟

多重中断技术在计算机中有着非常重要的地位。本文在软硬件逻辑功能等价性原理的思想指导下,介绍了如何运用软件开发环境模拟中断系统并用可视化界面展示之,实现多重中断工作过程。该中断系统的实现表明,在计算机上用软件模拟硬件,应用于实验、教学和进一步的研究中是具有可行性的。

基于贝叶斯网的飞机维护实训教学专家系统

针对飞机维护实训教学中教学硬件资源少、知识关联性强、检修方案不唯一、学生难以掌握的特点,引入基于贝叶斯网的知识表达和不确定性推理原理,设计并实现了飞机维护实训教学专家系统.与一般基于规则的专家系统相比,本系统利用先验概率分布使推理可以在输入数据不完备的基础上进行;以网络拓扑结构表达定检维修中的定性知识,以网络节点的概率分布表达定检各个环节的关联性和不确定性,从而使不确定性知识的表达直观、明确;可以为学生提供快捷的故障诊断及排故训练.

深度产教融合下的网络空间安全专业“3+1”创新型人才培养模式探讨

针对当前应用本科型高校网络空间安全专业人才培养中存在的问题,在深度产教融合的指导思想下,提出了一种创新型人才培养模式。借助奇安信科技集团的支持,构建了“3+1”人才培养规划方案,实施了面向产业需求、突出实训实践的课程教学方案,同时通过强化“课程思政”、坚持“以赛促学”、引入“名师名家”等措施展开全员、全过程、全方位的育人工作,将学历教育与职业资格教育有机结合,为学生提供就业服务。研究结果是对复合型应用型网络空间安全专业高级技术人才培养的有效探索。

面向频繁项集挖掘的本地差分隐私事务数据收集方法

事务数据常见于各种应用场景中,如购物记录、页面浏览历史等.为了提供更好的服务,服务提供商收集用户数据并进行分析,但收集事务数据会泄露用户的隐私信息.为了解决上述问题,基于压缩的本地差分隐私模型,提出一种事务数据收集方法.首先,定义了一种新的候选项集分值函数;其次,基于该函数,将候选项集的样本空间划分为多个子空间;然后,随机选择其中一个子空间,基于该子空间随机生成事务数据并发送给不可信的数据收集者;最后,考虑到隐私参数的设置问题,基于最大后验置信度攻击模型设计启发式隐私参数设置策略.理论分析表明,该方法能够同时保护事务数据的长度与内容,满足压缩的本地差分隐私要求.实验结果表明,与目前最优的工作相比,所收集的数据具有更高的效用性,隐私参数设置更具有语义性.

产教融合信息类专业人才培养模式探索

运用协同创新理论,结合本科教育规律、信息类专业特征及企业需求,明晰了育人模式中“校业企师”四元协同的地位与作用,构建了“四位一体”的人才培养途径,明确了“知识+技术+创新+应用”的卓越型人才培养目标,最终提出并在教学全过程中贯彻了“四元协同、四位一体”的卓越型人才培养模式,是高校协同育人模式的创新性实践。

基于在线判题系统的程序设计课程群教学研究

精讲多练是程序设计课程群教学的基本原则,理论讲授后需要通过大量上机实验来提高学生程序设计思维能力。然而,程序设计实际教学中存在学生学习兴趣不高、同学之间交流互动较少、作业批改量大以及考试出题阅卷任务重等问题。为解决上述问题,笔者设计并实现了集教学、在线练习、交流、考试、竞赛以及共享等功能于一体的程序设计在线实验平台。该平台经过教学实践,能够有效提升学生学习程序设计的积极性,教学效果良好。

西江干流广东段水陆交错带生态系统服务价值梯度研究

水陆交错带是水域和陆地间进行物质传输、能量转化和生物流动的重要廊道、过滤器和屏障,对其进行生态系统服务价值梯度的研究能在一定程度上厘清生态系统服务价值的高低与水域距离之间的耦合关系。对西江干流广东段的生态系统服务价值进行梯度研究,以1 km为单位将研究区划分为10个梯度级,选用基于单位面积价值当量因子法进行计算和分析。结果表明:(1)研究区各土地利用类型对应的生态系统服务价值占比大小依次为:水域>阔叶林>人工湿地>灌丛>水田>针叶林>自然湿地>草地;(2)1 km梯度级别内水域生态系统服务价值贡献了80%左右的供给服务、85%的调节服务价值和近50%的支持服务;2~5 km的梯度级别内人工湿地的生态系统服务价值最高,其次是阔叶林生态系统;6~10 km梯度级别内阔叶林的生态系统服务价值最高,其次是人工湿地和灌丛生态系统。可以得到以下结论:(1)各类生态系统服务价值的高低主要是由其能够提供的生态系统服务功能及单位面积生态系统服务价值的高低来决定的,并非完全取决于面积的大小;(2)水陆交错带生态系统服务价值的高低与距离水域的远近关联密切,生态系统服务总价值随着距离增加而逐渐减少;(3)用地类型以及景观空间配置在一定程度上会引发生态系统服务功能与价值在空间上的差异。研究为西江流域的保护与可持续发展提供科学参考。

实例化空间逻辑下的SET支付协议验证及改进

使用基于知识推理的实例化空间逻辑及其自动化验证工具SPV对SET支付协议的重要安全性质进行验证,并对协议进行改进.与模型检测法相比,可以验证协议在任意会话中的正确性;与定理证明等方法相比,验证过程是完全自动化的.在不影响原SET支付协议安全性的前提下,使用实例化空间逻辑简化协议的复杂消息,并合理选择协议分支,建立比以往研究更贴近原协议的模型.给出了该模型及其秘密性、认证性在SPV下的形式化描述,并展示验证结果,分析验证效率.针对验证结果中不被满足的认知规范,给出协议的改进方案,解决了持卡人和支付网关之间的认证问题.

“三全育人”视域下网络空间安全专业思政育人体系的构建与应用

网络空间安全专业作为“新工科”专业,对于国家安全至关重要,因此思政教育在人才培养中占据核心地位。在《高等学校课程思政建设指导纲要》指导下,结合专业需求构建思政育人体系至关重要。广东技术师范大学网络空间安全学院以产教融合、科教结合为特色,以“思政强心”为引领,构建多维度思政教学团队,探索育人制度改革,形成涵盖通识、专业和课外思政教育的完整育人体系。该体系支撑五维人才培养模式,有效实施“三全育人”,并对新时代“新工科”专业思政育人创新具有启示作用。