基于深度学习的安全缺陷报告预测方法实证研究

软件安全问题的发生在大多数情况下会造成非常严重的后果，及早发现安全问题，是预防安全事故的关键手段之一.安全缺陷报告预测可以辅助开发人员及早发现被测软件中潜藏的安全缺陷，从而尽早得以修复.然而，由于安全缺陷在实际项目中的数量较少，而且特征复杂（即安全缺陷类型繁多，不同类型安全缺陷特征差异性较大），这使得手工提取特征相对困难，并随后造成传统机器学习分类算法在安全缺陷报告预测性能方面存在一定的瓶颈.针对该问题，提出基于深度学习的安全缺陷报告预测方法，采用深度文本挖掘模型TextCNN和TextRNN构建安全缺陷报告预测模型；针对安全缺陷报告文本特征，使用skip-grams方式构建词嵌入矩阵，并借助注意力机制对TextRNN模型进行优化.所构建的模型在5个不同规模的安全缺陷报告数据集上展开了大规模实证研究，实证结果表明：深度学习模型在80%的实验案例中都要优于传统机器学习分类算法，性能指标F1-score平均可提升0.258，在最好的情况下甚至可以提升0.535.除此之外，针对安全缺陷报告数据集存在的类不均衡问题，对不同采样方法进行了实证研究，并对结果进行了分析.     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

Event fairness and non-interleaving concurrency

Event fairness suitable for non-interleaving concurrency is proposed. Fairness is viewed with respect to concurrency, rather than non-determinism, in the sense that no concurrent component of the system should be delayed indefinitely. Shields' asynchronous transition systems and Mazurkiewicz's traces have been used; the model gives rise to a partial order. A class of generalised notions of (weak, strong and unconditional) event fairness relative to progress requirements is derived. The weakest fairness notion in this class is shown to coincide with maximality with respect to the partial order over traces.     

一种针对格式文件的符号执行优化方法

为了解决符号执行中路径爆炸、新路径发现率低等问题，提出了针对文件格式数据块约束的符号执行分析方法（FFCBSE，File Format Constraint Based Symbolic Execution）优化框架.文件格式信息的缺失会影响符号执行的效率以及测试用例生成，该方法通过分析程序代码自动分析程序读取的格式文件数据块之间的依赖关系并建立相关约束，随后使用这些约束引导符号执行更关注于核心功能代码区域.在KLEE中实现了上述优化框架，并对Tcpdump、Readelf、Elfdump、File、Zlib等7个常用文件处理程序做了检测.和KLEE以及DASE相比，FFCBSE发现了13个之前未知的缺陷，在指令覆盖率和分支覆盖率有10%~225%不同程度的提升.     

An optimal distributed solution to the dining philosophers problem

An optimal distributed solution to the dining philosophers problem is presented. The solution is optimal in the sense that it incurs the least communication and computational overhead, and allows the maximum achievable concurrency. The worst case upper bound for concurrency is shown to ben div 3,n being the number of philosophers. There is no previous algorithm known to achieve this bound.     

Intelligent SQL

Intelligent SQL is an intelligent database engine interface language which incorporates object-oriented, inferencing, and multi-media constructs. It is intended to be a powerful extension of existing SQL dialects. It also provides querying capabilities for object-oriented databases. Intelligent SQL was prototyped at Ashton-Tate. This paper discusses the main features of Intelligent SQL.     

On logical and concurrent equivalences

We consider modal analogues of Hintikka et al.'s ‘independence-friendly first-order logic’, and discuss their relationship to equivalences previously studied in concurrency theory.     

解决分布式数据库2PL执行-提交冲突的一种改进的乐观方法

分布式数据库系统通常采用2PL(两阶段锁定协议)来维护其一致性.本文运用Shadow-Opt方法,通过区分写操作将新旧算法结合从而保证一致性并提高性能.     

Transformations for early reply and forward message passing mechanisms

Message passing notations (language, package, etc.) typically include some form of asynchronous or synchronous invocation. In a synchronous invocation, the invoker waits for the invocation's servicer to pass back results. Some message passing notations also include early reply or deferred reply (including forwarding), which alters how and when the servicer passes back its results; this additional flexibility is useful in realistic applications. It is well known how to transform a synchronous invocation into only asynchronous invocations. This paper extends such transformations to early reply and forward. This paper also describes the use of these transformations within the implementations of programming notations. Using the transformation simplifies the implementation without significantly affecting run‐time costs. Copyright © 2015 John Wiley & Sons, Ltd.     

基于Soot的Java程序竞争静态检测工具设计

设计了基于Soot字节码分析框架并实现了软件原型,利用Soot提供的Spark指向分析框架对整个程序做出指向分析,在此基础上拓展了Soot分析框架,对每个可能竞争对进行线程局部对象分析、可能并行分析、别名锁分析,数据竞争结果逐步精确.