一种命令式风格的面向对象语言语义框架

面向对象语言在软件工程实践中有着广泛的应用。为面向对象语言定义严格的语义有助于理解面向对象语言的本质特征,对验证软件、提高软件系统可靠性等也具有重要意义。给出了一种新的面向对象语言的语义框架,该框架基于命令式的风格,具有操作语义和类型规则;证明了该语义框架的类型安全定理。     

改进的LS-SVM方法在EMD端点效应问题中的应用

经验模态分解能有效处理非平稳、非线性信号,但在多次采用三次样条插值获取信号上、下包络的过程中容易产生影响分解精度的端点问题。为了抑制经验模态分解中存在的端点效应问题,提出了一种基于最小二乘支持向量机和镜像延拓的端点效应抑制方法。该方法采用最小二乘支持向量机对原始信号序列两端分别向左、右各延拓有限个数据点;用镜像延拓对延拓后的信号序列进行对称延拓处理,将其延拓成一个环形信号序列;对这一环形信号序列进行经验模态分解。通过对仿真信号以及真实脑电信号进行实验分析以及与其他延拓方法的对比,结果表明该方法能够有效抑制端点效应问题,并在抑制端点效应问题方面优于传统的支持向量机和最小二乘支持向量机。     

Rust语言安全研究综述

Rust是为了解决系统编程领域的安全性问题, 而设计的一门面向系统编程的兼具类型安全、内存安全和并发安全的新型程序设计语言, 强调安全性和高性能, 已经在操作系统内核、Web浏览器、网络协议栈、数据库和区块链等底层软件系统的构建中得到了越来越广泛的应用。现有研究表明, 尽管Rust的设计目标是保证安全性, 但其自身仍然存在许多安全问题。作为一门系统编程语言, Rust的安全性直接影响到基于Rust开发的软件系统的安全性。随着Rust的广泛应用, 对Rust语言安全的研究显得尤为重要。Rust语言安全研究正在成为研究热点, 并且在近几年已经取得了较大研究进展。本综述基于该研究领域已经公开发表的46篇研究论文,对该领域的相关研究进行了系统整理、分析和总结: 首先, 研究分析了Rust的核心安全特性, 包括函数式编程范式、强多态类型系统、基于所有权模型的自动内存管理、对非安全代码的显式标记和隔离; 其次, 提出了Rust语言安全研究领域的分类学, 将已有研究分为安全实证研究、漏洞检测研究、安全增强研究和形式化验证研究四个热点方向, 并分别对这四个方向上的相关研究进行了综述、深入分析和总结, 同时分析了四个研究方向的内在联系; 最后, 指出了该研究领域的待解决的科学问题, 并对未来可能的研究方向进行了展望, 提出了四个潜在的研究方向, 以期为相关领域的研究者提供有价值的参考。     

汇编代码验证中的形式规范自动生成

与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明的编译器自动生成汇编级形式规范,从而减轻程序员的负担.使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力.文章主要描述该方法在出具证明编译器中的实现.     

处理指针相等关系不确定的指针逻辑

为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展,可用来对指针程序进行精确的指针分析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质　证明.     

Android内核钩子的混合检测技术

针对Android平台上内核级钩子检测的研究,提出了一种结合基于特征模式的静态检测技术和基于行为分析的动态检测技术的Android内核钩子检测技术,这两种技术的结合能够检测基于修改系统调用表项的攻击和基于内联钩子的攻击。为所提技术构建了软件原型系统并进行了实验评测,实验结果表明,提出的技术能够针对Android内核钩作出精确检测,并且运行时间开销在7%以内,具有良好运行效率,能够适用于Android内核钩子的混合。     

基于语义的恶意软件判定器框架

目前代码迷惑技术已经成为构造恶意软件变体的主要方式,大量出现的病毒变体使得传统基于程序文本特征的病毒排查工具的防护作用大大降低.本文提出一种新的基于语义的恶意软件变体判定框架,为了确定一个程序是否是某种恶意软件的变体:首先基于符号执行收集程序语义状态,然后通过证明语义之间是否满足变体关系来确定该程序是否是恶意软件的变体.本框架能够识别经代码迷惑变换后得到的程序是属于变换前程序的变体,从而可以减少对病毒数据库的更新.最后,通过一个实现了该框架的原型系统来说明基于语义的恶意软件判定器框架的可行性.     

一个经过证明的类型化汇编语言的类型检查器

编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全, 内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文给出一种类型化汇编语言,然后给出相应的类型检查器,并证明了此类型检查器的可靠性,从而保证经过类型检查的汇编程序的安全性.文本的所有工作,包括类型化汇编语言、类型检查器以及相关定理证明,均已在证明辅助工具Coq中实现.本文方法也可用于证明类型化高级语言的类型检查器的可靠性.     

一种用于指针程序验证的指针逻辑

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.     

一种汇编语言指针逻辑的设计与实现

软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证.