题名 基于函数式语义的循环和递归程序结构通用证明技术
1
作者
李希萌 王国辉 张倩颖 施智平 关永
机构
首都师范大学 信息工程学院电子系统可靠性技术 北京 市重点实验室(首都师范大学 ) 北京 成像 理论与 技术 高精尖 创新 中心 (首都师范大学 )
出处
《软件学报》
EI
CSCD
北大核心
2023年第8期3686-3707,共22页
基金
国家重点研发计划(2019YFB1309900) 国家自然科学基金(61876111,61877040,62002246) 北京市教育委员会科技计划(KM201910028005,KM202010028010)。
文摘
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.
关键词
程序验证 大步操作语义 定理证明 Coq定理证明器
Keywords
program verification big-step operational semantics theorem proving Coq proof assistant
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
题名 微内核操作系统互斥量模块功能正确性的形式化验证
2
作者
张林雁 李希萌 施智平 关永 曹钦翔 张倩颖
机构
首都师范大学 信息工程学院电子系统可靠性技术 北京 市重点实验室(首都师范大学 ) 北京 成像 理论与 技术 高精尖 创新 中心 (首都师范大学 )上海交通大学 约翰霍普克罗夫特计算机科学中心
出处
《软件学报》
EI
CSCD
北大核心
2024年第9期4179-4192,共14页
基金
国家自然科学基金(62002246,62272322,62272323,62372311,62372312,61902240)。
文摘
操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.
关键词
互斥量 功能正确性 形式化验证 定理证明 Coq定理证明器
Keywords
mutex functional correctness formal verification theorem proof Coq theorem prover
分类号
TP316
[自动化与计算机技术—计算机软件与理论]
题名 面向数据流的ROS2数据分发服务形式建模与分析
被引量：7
3
作者
芦倩 李晓娟 关永 王瑞 施智平
机构
首都师范大学 信息工程学院高可靠嵌入式系统技术 北京 市工程研究中心 (首都师范大学 ) 北京 成像 理论与 技术 高精尖 创新 中心 (首都师范大学 )轻型工业机器人与安全验证北京 市重点实验室(首都师范大学 )
出处
《软件学报》
EI
CSCD
北大核心
2021年第6期1818-1829,共12页
基金
国家重点研发计划(2019YFB1309900) 国家自然科学基金(61876111) +1 种基金 科技创新服务能力建设-基本科研业务费(00620530290073) 首都师范大学交叉科学研究项目(0062155087)。
文摘
机器人操作系统(robot operating system,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法,分析、验证ROS2系统数据分发机制的实时性和可靠性.首先,提出一种面向数据流的ROS2数据分发服务的形式化验证框架,并对通信系统模块建立概率时间自动机模型;其次,运用概率模型检测器,通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性;最后,基于重传机制、服务质量(quality of service,简称QoS)策略分析,通过设置和调整服务质量参数,实现不同的数据需求和传输方式的量化性能分析,为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.
关键词
ROS2 数据分发服务 QOS 概率时间自动机 PRISM 形式化建模与分析
Keywords
ROS2 data distribution service QoS probabilistic timed automata PRISM formal modeling and analysis
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
题名 以太坊中间语言的可执行语义
被引量：5
4
作者
韩宁 李希萌 张倩颖 王国辉 施智平 关永
机构
首都师范大学 信息工程学院电子系统可靠性技术 北京 市重点实验室(首都师范大学 ) 北京 成像 理论与 技术 高精尖 创新 中心 (首都师范大学 )
出处
《软件学报》
EI
CSCD
北大核心
2021年第6期1717-1732,共16页
基金
国家自然科学基金(61572331,61602325,61802375,61876111,61877040,62002246) 北京市教育委员会科技计划(KM20190028005,KM202010028010) 中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)。
文摘
智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.
关键词
智能合约 Yul语言 Isabelle/HOL 形式化语义 以太坊
Keywords
smart contract Yul language Isabelle/HOL formal semantics Ethereum
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
题名 基于Spark的大数据访存行为跨层分析工具
被引量：10
5
作者
许丹亚 王晶 王利 张伟功
机构
首都师范大学 信息工程学院高可靠嵌入式技术 北京 市工程研究中心 (首都师范大学 ) 北京 成像 理论与 技术 高精尖 创新 中心 (首都师范大学 )
出处
《计算机研究与发展》
EI
CSCD
北大核心
2020年第6期1179-1190,共12页
基金
国家自然科学基金项目(61772350) 北京市科技新星计划(Z181100006218093) +2 种基金 北京未来芯片技术高精尖创新中心科研基金项目(KYJJ2018008) 北京市高水平教师队伍建设计划(CIT&TCD201704082) 科技创新服务能力建设基本科研业务费(科研类)(19530050173)。
文摘
大数据时代的到来为信息处理带来了新的挑战,内存计算方式的Spark显著提高了数据处理的性能.Spark的性能优化和分析可以在应用层、系统层和硬件层开展,然而现有工作都只局限在某一层,使得Spark语义与底层动作脱离,如操作系统参数对Spark应用层的性能影响的缺失将使得大量灵活的操作系统配置参数无法发挥作用.针对上述问题,设计了Spark存储系统分析工具SMTT,打通了Spark层、JVM层和OS层,建立了上层应用程序的语义与底层物理内存信息的联系.SMTT针对Spark内存特点,分别设计了针对执行内存和存储内存的追踪方式.基于SMTT工具完成了对Spark迭代计算过程内存使用,以及跨越Spark,JVM和OS层的执行存储内存使用过程的分析,并以RDD为例通过SMTT分析了单节点和多节点情况下Spark中读和写操作比例,结果表明该工作为Spark内存系统的性能分析和优化提供了有力的支持.
关键词
大数据 SPARK 内存管理 跨层分析 内存追踪
Keywords
big data Spark memory management cross-layer analysis memory tracing
分类号
TP391
[自动化与计算机技术—计算机应用技术]
题名 可信执行环境软件侧信道攻击研究综述
被引量：10
6
作者
杨帆 张倩颖 施智平 关永
机构
首都师范大学 信息工程学院高可靠嵌入式系统北京 市工程研究中心 (首都师范大学 ) 计算机体系结构国家重点实验室(中国科学院计算技术 研究所) 电子系统可靠性技术 北京 市重点实验室(首都师范大学 ) 北京 成像 理论与 技术 高精尖 创新 中心 (首都师范大学 )
出处
《软件学报》
EI
CSCD
北大核心
2023年第1期381-403,共23页
基金
国家自然科学基金(61802375,61602325,61876111,61877040) 北京市教委科技计划一般项目(KM201910028005) +1 种基金 中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920) 交叉科学研究院项目(19530012005)。
文摘
为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(TEE)技术,通过对硬件和软件进行隔离为安全敏感程序提供一个与通用计算环境隔离的安全运行环境.侧信道攻击从传统的需要昂贵设备发展到现在仅基于微体系结构状态就能通过软件方式获取机密信息的访问模式,从而进一步推测出机密信息.TEE架构仅提供隔离机制,无法抵抗这类新出现的软件侧信道攻击.深入调研了ARM TrustZone、Intel SGX和AMD SEV这3种TEE架构的软件侧信道攻击及相应防御措施,并探讨其攻击和防御机制的发展趋势.首先,介绍了ARM TrustZone、Intel SGX和AMD SEV的基本原理,并详细阐述了软件侧信道攻击的定义以及缓存侧信道攻击的分类、方法和步骤;之后从处理器指令执行的角度,提出一种TEE攻击面分类方法,利用该方法对TEE软件侧信道攻击进行分类,并阐述了软件侧信道攻击与其他攻击相结合的组合攻击;然后详细讨论TEE软件侧信道攻击的威胁模型;最后全面总结业界对TEE软件侧信道攻击的防御措施,并从攻击和防御两方面探讨TEE软件侧信道攻击未来的研究趋势.
关键词
可信执行环境(TEE) 隔离架构 ARM TrustZone Intel SGX AMD SEV 软件侧信道攻击
Keywords
trusted execution environment(TEE) isolation architecture ARM TrustZone Intel SGX AMD SEV software side-channel attack
分类号
TP309
[自动化与计算机技术—计算机系统结构]
题名 多层神经网络算法的计算特征建模方法
被引量：6
7
作者
方荣强 王晶 姚治成 刘畅 张伟功
机构
首都师范大学 信息工程学院体系结构国家重点实验室(中国科学院计算技术 研究所) 高可靠嵌入式系统技术 北京 市工程研究中心 (首都师范大学 ) 北京 成像 理论与 技术 高精尖 创新 中心 (首都师范大学 )
出处
《计算机研究与发展》
EI
CSCD
北大核心
2019年第6期1170-1181,共12页
基金
国家自然科学基金项目(61772350) 共有信息系统装备预先研究项目(公开)(JZX2017-0988/Y300) +4 种基金 北京市科技新星计划项目(Z181100006218093) 体系结构国家重点实验室开放课题(CARCH201607) 北京未来芯片技术高精尖创新中心科研基金资助项目(KYJJ2018008) 北京市高水平教师队伍建设计划(CIT&TCD201704082) 科技创新服务能力建设-基本科研业务费(科研类)(19530050173,02518530500)~~
文摘
随着深度学习算法在语音和图像等领域中的成功运用,能够有效提取目标特征并做出最优决策的神经网络再次得到了广泛的关注.然而随着数据量的增加和识别精度需求的提升,神经网络模型的复杂度不断提高,因此采用面向特定领域的专用硬件加速器是高效运行神经网络的有效途径.然而如何根据网络规模设计高能效的加速器,以及基于有限硬件资源如何提高网络性能并最大化资源利用率是当今体系结构领域研究的重要问题.为此,提出基于计算特征的神经网络分析和优化方法,基于“层”的粒度解析典型神经网络模型并提取模型通用表达,根据通用表达式和基本操作属性提取模型运算量和存储空间需求等特征.提出了基于最大值更替的运行调度算法,利用所提取的特征分析结果对神经网络在特定硬件资源下的运行调度方案进行优化.实验结果显示:所提方法能够有效分析对比网络特征,并指导所设计调度算法实现性能和系统资源利用率的提升.
关键词
神经网络 特征提取 硬件加速器 计算机体系结构 资源调度
Keywords
neural network features extraction hardware accelerator computer architecture resource scheduling
分类号
TP391
[自动化与计算机技术—计算机应用技术]
