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

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

改进的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中实现.本文方法也可用于证明类型化高级语言的类型检查器的可靠性.     

高阶代码消除性能比较框架的设计与实现

函数式语言编译中,闭包变换和函数消除是广泛采用的高阶代码消除方法。为了提高函数式语言的运行效率,针对函数式语言编译阶段的高阶代码消除过程对目标代码效率的影响,设计并实现了一种函数式语言编译框架。该框架采用了菱形的架构,平行地使用了闭包变换与函数消除两种高阶代码消除方法。设计了一种具有代表性的函数式语言——FUN语言,并以FUN语言为基础,给出了比较框架的一个完整实现。通过该系统,对闭包变换与函数消除的效率影响进行对比实验,选取具有典型特征的测试例,分别从生成代码的规模和运行效率方面对闭包变换与函数消除两种方法的结果进行比较。实验结果表明,与闭包变换相比,使用函数消除方式所得的目标代码量更少,最多可减少33.76%的目标代码量;并且运行效率更高,最多可提高69.51%。