-
题名无线传感器网络中公钥机制研究综述
被引量：10
- 1
-
-
作者
何炎祥
孙发军
李清安
何静
汪吕蒙
-
机构
武汉大学计算机学院
肯尼索州立大学计算机科学系
-
出处
《计算机学报》
EI
CSCD
北大核心
2020年第3期381-408,共28页
-
基金
国家自然科学基金(91118003,61373039,61502346)资助.
-
文摘
物联网是当前学术界和产业界的研究热点,作为物联网主要构成部分之一的无线传感器网络(Wireless Sensor Networks,WSNs),其安全与人们的生活安全及隐私息息相关.过去近二十年来WSNs安全得到了广泛深入的研究,其中公钥机制从最初的不可行认知到现今的广泛研究应用,在WSNs中的可行性正逐渐被认可.然而公钥机制是否可以在WSNs中全面展开、其被引入到WSNs后会带来哪些问题、还有哪些尚未解决,这些都有待进一步探究.本文梳理了WSNs中公钥机制研究的高质量文献并将其归结为原语类、密钥管理类、认证与访问控制类、其他应用类,对比分析了各类文献中的经典研究工作,总结了WSNs中引入公钥机制的必要性、可行性及相关问题与挑战,针对这些挑战分析了其现有解决情况,最后对研究方向及可能的解决方案进行了展望.
-
关键词
传感器网络
安全
综述
密码学原语
密钥协商
密钥管理
物联网
-
Keywords
sensor networks
security
review
cryptographic primitive
key agreement
key management
Internet of Things
-
分类号
TP393
[自动化与计算机技术—计算机应用技术]
-
-
题名机械化定理证明研究综述
被引量：7
- 2
-
-
作者
江南
李清安
汪吕蒙
张晓瞳
何炎祥
-
机构
湖北工业大学计算机学院
武汉大学计算机学院
-
出处
《软件学报》
EI
CSCD
北大核心
2020年第1期82-112,共31页
-
基金
国家自然科学基金(90818018,91018009,61170022,91118003,61373039)
华为技术有限公司合作项目(YB2015090035)
湖北工业大学校博士科研启动基金(BSQD2017043)。
-
文摘
随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.
-
关键词
定理证明
证明助手
消解
自然演绎
类型化的λ演算
编程逻辑
求精
-
Keywords
theorem proving
proof assistant
resolution
natural deduction
typed λ-calculus
logics of programming
refinement
-
分类号
TP18
[自动化与计算机技术—控制理论与控制工程]
-
-
题名通用图形处理器缓存子系统性能优化方法综述
被引量：4
- 3
-
-
作者
张军
谢竟成
沈凡凡
谭海
汪吕蒙
何炎祥
-
机构
东华理工大学江西省放射性地学大数据技术工程实验室
东华理工大学信息工程学院
东华理工大学创新创业学院
武汉大学计算机学院
南京审计大学
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2020年第6期1191-1207,共17页
-
基金
国家自然科学基金项目(61662002,61972293,61902189)
江西省放射性地学大数据技术工程实验室项目(JELRGBDT201905)
江苏省基础研究计划(自然科学基金)项目(BK20180821)。
-
文摘
随着工艺和制程技术的不断发展以及体系架构的日趋完善,通用图形处理器(general purpose graphics processing units,GPGPU)的并行计算能力得到了很大的提升,其在高性能、高吞吐量等通用计算应用场景的使用越来越广泛.GPGPU通过支持大量线程的并发执行,可以较好地隐藏长延时访存操作,从而获得高并行计算能力.然而,GPGPU在处理计算和访存不规则的应用时,其存储子系统的效率受到很大影响,尤其是片上缓存的争用情况尤为突出,难以及时提供计算操作所需的数据,使得GPGPU的高并行计算能力不能得到充分发挥.解决片上缓存的争用问题、优化缓存子系统的性能,是优化GPGPU性能的主要解决方案之一,也是目前研究GPGPU性能优化的主要热点之一.目前,针对GPGPU缓存子系统的性能优化研究主要集中在线程级并行度(thread level parallelism,TLP)调节、访存顺序调节、数据通量增强、最后一级缓存(last level cache,LLC)优化和基于非易失性存储(non-volatile memory,NVM)的GPGPU缓存新架构设计等5个方面.也从这5个方面重点分析讨论了目前主要的GPGPU缓存子系统性能优化方法,并在最后指出了未来GPGPU缓存子系统优化需要进一步探讨的问题,对GPGPU缓存子系统性能优化的研究有重要意义.
-
关键词
通用图形处理器
缓存子系统
性能优化
延迟隐藏
缓存争用
-
Keywords
general purpose graphics processing units(GPGPU)
cache subsystem
performance optimization
latency hiding
cache contention
-
分类号
TP303.1
[自动化与计算机技术—计算机系统结构]
-
-
题名机械化验证一个高效的迭代数据流求解算法
- 4
-
-
作者
江南
汪吕蒙
张晓瞳
何炎祥
-
机构
湖北工业大学计算机学院
武汉大学计算机学院
-
出处
《软件学报》
EI
CSCD
北大核心
2022年第6期2115-2126,共12页
-
基金
国家自然科学基金(61972293)
国家留学基金委地方合作项目(201808420414)。
-
文摘
迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.
-
关键词
机械化验证
高效迭代算法
支配节点
-
Keywords
mechanized verification
efficient iterative algorithm
dominators
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
