检索结果-南通市图书馆

Research on Microkernel Integrity Semantics Model and Formal Verification

在线全文

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2014年第1期23卷 43-48页

作者： qian zhenjiang LIU Wei HUANG Hao State Key Laboratory for Novel Software Technology Nanjing University Department of Computer Science and Technology Nanjing University

Microkernel integrity is an important aspect of security for the whole microkernel system. Many of the research works on microkernel integrity focus on analysis and safeguards against the existing kernel attacks, and security enhancements for the vulnerabilities of system design and implementation aspects. The formal methods for operating system design and verification ensure the system’s high level of security. The existing formalization work and research for operating system mainly focus on the code-level verification of program correctness. In this paper, we propose a formal abstraction model of microkernel in order to accurately describe the semantics of every kernel behavior, and achieve the description of the whole kernel. Based on the model we illustrate the microkernel integrity criterions and elaborate on the integrity mechanism. Meanwhile, we formally verify the completeness and consistency between the mechanism and the definition of the microkernel integrity. We use the self-implemented operating system VTOS(Verified trusted operating system) as an example to illustrate the design method for the microkernel integrity.

关键词： Microkernel integrity Integrity mechanism Integrity semantics model Formal verification

A measurable refinement method of design and verification for micro-kernel operating systems in communication network

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Digital Communications and Networks 2023年第5期9卷 1070-1079页

作者： zhenjiang qian Rui Xia Gaofei Sun Xiaoshuang Xing Kaijian Xia School of Computer Science and Engineering Changshu Institute of TechnologySuzhou215500China Changshu Hospital of Soochow University Jiangsu215500ChangshuChina

A secure operating system in the communication network can provide the stable working environment,which ensures that the user information is not *** micro-kernel operating system in the communication network retains the core functions in the kernel,and unnecessary tasks are implemented by calling external *** to the small amount of code,the micro-kernel architecture has high reliability and *** the microkernel operating system in the communication network prototype VSOS as an example,we employ the objdump tool to disassemble the system source code and get the assembly layer *** this basis,we apply the Isabelle/HOL,a formal verification tool,to model the system *** referring to the mathematical model of finite automata and taking the process scheduling module as an example,the security verification based on the assembly language layer is *** on the Hoare logic theory,each assembly statement of the module is verified in *** verification results show that the scheduling module of VSOS has good functional security,and also show the feasibility of the refinement framework.

关键词： Assembly-level verification Finite automaton Hoare logic Isabelle/HOL Micro-kernel OS

AFSTGCN:Prediction for multivariate time series using an adaptive fused spatial-temporal graph convolutional network

在线全文

学校读者我要写书评

暂无评论

Digital Communications and Networks 2024年第2期10卷 292-303页

作者： Yuteng Xiao Kaijian Xia Hongsheng Yin Yu-Dong Zhang zhenjiang qian Zhaoyang Liu Yuehan Liang Xiaodan Li School of Information and Control Engineering China University of Mining and TechnologyXuzhou221116China Department of Informatics University of LeicesterLeicesterLE17RHUK The Affiliated Changshu Hospital of Soochow University Changshu215500China School of Computer Science and Engineering Changshu Institute of TechnologySuzhou215500China

The prediction for Multivariate Time Series(MTS)explores the interrelationships among variables at historical moments,extracts their relevant characteristics,and is widely used in finance,weather,complex industries and other ***,it is important to construct a digital twin ***,existing methods do not take full advantage of the potential properties of variables,which results in poor predicted *** this paper,we propose the Adaptive Fused Spatial-Temporal Graph Convolutional Network(AFSTGCN).First,to address the problem of the unknown spatial-temporal structure,we construct the Adaptive Fused Spatial-Temporal Graph(AFSTG)***,we fuse the spatial-temporal graph based on the interrelationship of spatial ***,we construct the adaptive adjacency matrix of the spatial-temporal graph using node embedding ***,to overcome the insufficient extraction of disordered correlation features,we construct the Adaptive Fused Spatial-Temporal Graph Convolutional(AFSTGC)*** module forces the reordering of disordered temporal,spatial and spatial-temporal dependencies into rule-like *** dynamically and synchronously acquires potential temporal,spatial and spatial-temporal correlations,thereby fully extracting rich hierarchical feature information to enhance the predicted *** on different types of MTS datasets demonstrate that the model achieves state-of-the-art single-step and multi-step performance compared with eight other deep learning models.

关键词： Adaptive adjacency matrix Digital twin Graph convolutional network Multivariate time series prediction Spatial-temporal graph

操作系统对象语义模型(OSOSM)及形式化验证

在线全文

学校读者我要写书评

暂无评论

计算机研究与发展 2012年第12期49卷 2702-2712页

作者：钱振江刘苇黄皓南京大学软件新技术国家重点实验室南京210046 南京大学计算机科学与技术系南京210046

操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系... 详细信息

操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系统对象语义模型(OSOSM).OSOSM采用分层结构,包括基本功效层、实现层和优化层.OSOSM将操作系统中的行为主体和资源抽象为操作系统对象,建立操作系统的论域,利用以操作系统对象变元集合为定义域到论域的映射表示操作系统的状态,描述操作系统系统调用等行为的语义,使用逻辑系统的谓词公式表达操作系统的安全属性,给出如何验证操作系统在运行过程中保持安全策略和属性的形式化描述方法.以实现并经过形式化验证的可信操作系统(VTOS)为例,阐述OSOSM的语义正确性.使用Isabelle定理证明工具验证设计和安全需求的一致性,以说明VTOS具有预期的安全属性.

关键词：操作系统对象语义模型形式化设计安全性验证 Isabelle定理证明

一种基于Isabelle/HOL的安全通信协议验证方法

在线全文

学校读者我要写书评

暂无评论

计算机工程 2021年第1期47卷 146-153页

作者：夏锐钱振江刘苇苏州大学计算机科学与技术学院江苏苏州215000 常熟理工学院计算机科学与工程学院江苏常熟215500 国网电力科学研究院南京211000

传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上... 详细信息

传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。

关键词：通信协议混合密钥形式化建模形式化验证 Isabelle/HOL定理证明辅助工具

基于服务质量机会测量的传感器网络协作控制机制

在线全文

学校读者我要写书评

暂无评论

计算机应用研究 2018年第5期35卷 1511-1513,1518页

作者：靳勇钱振江常熟理工学院计算机科学与工程学院江苏常熟215500

为了消除制约无线传感器网络性能的因素和提高网络控制效率,基于实时网络服务质量机会测量提出了传感器网络协作控制机制。首先,基于发送端节点和接收端节点状态以及中继节点的协作,测定无线传感器网络实时状态;其次,分析能耗品质和负... 详细信息

为了消除制约无线传感器网络性能的因素和提高网络控制效率,基于实时网络服务质量机会测量提出了传感器网络协作控制机制。首先,基于发送端节点和接收端节点状态以及中继节点的协作,测定无线传感器网络实时状态;其次,分析能耗品质和负载品质对网络性能的影响规律,讨论不同分频调制方式对网络性能的影响规律;最后,制定了网络状态感知的机会分频调制的传感器网络协作控制机制。数学分析和实验结果表明,所提出的传感器网络协作控制机制对无线传感器网络的实时性、可靠性和吞吐率等方面具有较强的保障能力。

关键词：网络状态服务质量机会测量协作控制

基于GOP分帧协作的多媒体多流并行传输机制

在线全文

学校读者我要写书评

暂无评论

电子技术应用 2017年第6期43卷 110-112,117页

作者：靳勇钱振江常熟理工学院计算机科学与工程学院江苏常熟215500

针对移动多媒体通信的可靠性和并行多流的实时性保障问题,通过组建GOP分帧协作网络,提出了多媒体多流并行动态传输机制。首先,基于多媒体流结构和视频帧优先级与吞吐率、可解码帧率和信道质量的关系,提出了GOP分帧协作传输网络的构建和... 详细信息

针对移动多媒体通信的可靠性和并行多流的实时性保障问题,通过组建GOP分帧协作网络,提出了多媒体多流并行动态传输机制。首先,基于多媒体流结构和视频帧优先级与吞吐率、可解码帧率和信道质量的关系,提出了GOP分帧协作传输网络的构建和动态调整方案。其次,基于动态多媒体的状态分析了多媒体流数、信道质量、可解码帧率和误码率的变化规律,结合用户侧需求和通信距离,提出了基于GOP分帧协作的动态多媒体多流并行传输机制。最后,仿真实验证明了所提方案在实时性、并行效率和可靠性等方面具有良好表现,非常适合于并行大规模多媒体实时通信。

关键词： GOP分帧协作传输多媒体流动态调度多流并行

在线全文

学校读者我要写书评

暂无评论

基于冗余代码的控制流混淆算法

计算机应用研究 2020年第11期37卷 3411-3416页

作者：乐德广赵杰钱振江常熟理工学院计算机科学与工程学院江苏常熟215500 苏州同程网络科技股份有限公司江苏苏州215123

目前的平展控制流主要是结合不透明谓词使用的,例如混沌映射和同余方程算法,这些算法会引起大量额外开销。此外,这种结合不透明谓词的平展控制流混淆方法难抵御动态逆向攻击。针对这些问题,提出了在插入与原基本块结构类似、但数据随机... 详细信息

目前的平展控制流主要是结合不透明谓词使用的,例如混沌映射和同余方程算法,这些算法会引起大量额外开销。此外,这种结合不透明谓词的平展控制流混淆方法难抵御动态逆向攻击。针对这些问题,提出了在插入与原基本块结构类似、但数据随机生成且与原基本块不同的冗余块,使攻击者难以区分实际执行基本块的基础上,对实际执行基本块和冗余块进行控制流平展化处理,进一步混淆控制流结构。此外,构建分支函数动态赋值算法,对分支变量进行强化,提高混淆弹性。该控制流混淆算法在mbed TLS程序测试集上进行控制流、逆向工程和性能测试与分析,测试与分析结果表明该混淆算法不仅能大大提高混淆强度,还能有效保护程序控制流信息,抵抗动静态逆向分析。

关键词：冗余代码混淆控制流逆向工程

VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

在线全文

学校读者我要写书评

暂无评论

南京大学学报（自然科学版） 2017年第3期53卷 577-578页

作者：钱振江黄皓宋方敏常熟理工学院计算机科学与工程学院苏州215500 南京大学软件新技术国家重点实验室南京210023

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确... 详细信息

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.

关键词：操作系统内核硬件抽象模型形式化验证 Isabelle/HOL 定理证明