命令式模糊程序语言的语义

文中关注计算机语言的形式语义学,旨在建立一种命令式模糊程序语言的指称语义与最弱(线性)前置条件语义.首先,借助模糊逻辑中的三角模、三角余模、非、蕴含以及模糊关系的合成等成功地完成了这两种语义的建模.这种方法为形式语义学的研究提供了一个新的视角.其次,证明了该语言的一些重要性质并讨论了最弱前置条件语义与最弱线性前置条件语义之间的关系.最后,证明了指称语义与最弱(线性)前置条件语义之间的对偶,该对偶表明了这两种语义可以相互诱导.     

基于程序正确性的演算方法

为了使开发出的程序更具有可靠性,研究了两种正确性验证的演算方法,Dijkstra的最弱前置谓词变换法和Hoare的公理化方法.针对于Hoare公理化方法证明中的前置条件难以寻找的问题,提出了将这两种演算方法结合使用的方法.对最弱前置谓词变换法的过程进行分析,确定了最弱前置谓词算法的准确性.将最弱前置谓词应用到公理化方法中,即把最弱前置谓词变换法求出的前置谓词作为公理化方法的前置条件.通过一个具体实例,详细说明了其验证过程,并证明了该方法的有效性.     

静态缺陷检测中的误报消除技术研究

误报率是衡量静态缺陷检测工具的重要指标.在对比分析了各种误报消除技术的基础上,提出了一种前向数据流分析结合逆向约束搜索技术的误报消除方法:前向数据流分析的保守数据流解可以用于缺陷状态迭代,并得到初始的缺陷检测结果;根据缺陷发生处的数据流特征,逆向搜索可能导致缺陷发生的约束条件,该约束条件可以作为通用约束求解器的输入判断缺陷的可满足性,从而对初始的缺陷检测结果进行精化.同时,在数据流分析过程中引入符号执行技术,不仅提高了数据流分析的精度,且便于约束表示及转化,提高了约束搜索的效率.对SPECCPU2000中11个工程的对比实验表明,前向数据流分析与逆向约束搜索相结合的误报消除方法在增加了有限开销的同时有效地消除了部分误报,且与同类工具相比具有更好的可扩展性.     

一种基于单条程序执行路径的错误定位方法

当程序在测试中发生错误时,将形成一条错误的程序执行路径,程序员将会花费很多精力去检测程序代码和定位最终的程序错误．提出一种基于单条程序执行路径的错误定位方法,该方法通过对程序进行反向执行,计算出多个最弱前置条件及其相对应的疑似错误语句集,并生成错误定位树,来辅助程序员进行快速错误定位．对西门子测试数据集进行的实验表明了该方法具有良好的效果．     

基于目标制导符号执行的静态缓冲区溢出警报自动确认技术

缓冲区溢出漏洞是一类严重的安全性缺陷。目前存在动态测试和静态分析技术来检测缓冲区溢出缺陷:动态测试技术的有效性取决于测试用例的设计,而且往往会引入执行开销;静态分析技术及自动化工具已经被广泛运用于缓冲区溢出缺陷检测中,然而静态分析由于采取了保守的策略,其结果往往包含数量巨大的误报,需要通过进一步人工确认来甄别误报,但人工确认静态分析的结果耗时且容易出错,严重限制了静态分析技术的实用性。符号执行技术使用符号代替实际输入,能系统地探索程序的状态空间并生成高覆盖度的测试用例。本文提出一种基于目标制导符号执行的静态缓冲区溢出警报确认方法,使用静态分析工具的输出结果作为目标,制导符号执行确认警报。我们的方法分为3步:首先在过程间控制流图中检测静态分析警报路径片段的可达性,并将可达的警报路径片段集合映射为用于确认的完整确认路径集合;其次在符号执行中通过修剪与溢出缺陷疑似语句无关的路径,指导符号执行沿特定确认路径执行;最后在溢出缺陷疑似语句收集路径约束并加入溢出条件,通过约束求解的结果,对静态分析的警报进行分类。基于上述方法我们实现了原型工具BOVTool,实验结果表明在实际开源程序上BOVTool能够代替人工减少检查59.9%的缓冲区溢出误报。     

基于病毒复制行为的网络免疫系统的研究

生物体免疫系统是一个高度复杂的系统,专门来检测并消除病毒的传染。计算机安全系统同它有很多相似之处,对它们相同点的研究会对加强计算机安全提出许多方法。文中基于生物免疫系统中淋巴细胞激活的理论提出了基于病毒自我复制行为的行为特征检测模型。并对该模型的有效性进行了分析和实验。结果表明该模型可以成为一种新的尝试来针对病毒的复制行为进行检测,同时还能有效地减少在进行"自我"和"非我"的区别时出现的有害误报和无害误报问题。     

基于缺陷关联的静态分析优化

缺陷检测一般包括静态分析与人工审查两个阶段.静态检测工具报告大量缺陷,但是主要的缺陷确认工作仍由人工完成,这是一件费时、费力的工作.巨大的审查开销可能会导致软件开发人员拒绝使用该静态缺陷检测工具.提出一种可靠的基于缺陷关联的静态分析优化方法,能够分组静态检测工具所报告的缺陷,在分组后的任意一组缺陷中,如果其主导缺陷被证明是误报(或者是真实的),就能确认其他缺陷也是误报(也是真实的).实验结果表明,基于缺陷关联的静态分析优化方法在较小的时间和空间开销下减少了22%的缺陷审查工作,能够较好地适应于大型的关键嵌入式系统程序缺陷检测.     

提高静态缺陷检测精度方法

误报率和漏报率是静态缺陷检测的关键技术指标,提高分析精度是降低误报和漏报的主要手段.文中介绍了缺陷模式及其有限状态机描述,提出基于传统数据流分析的缺陷检测方法.采用变量抽象取值来近似地表示程序动态执行信息,通过状态条件中的变量抽象取值范围为空来判断不可达路径,以实现路径敏感分析;使用缺陷相关的函数摘要来表示缺陷检测所需函数调用信息,其中缺陷相关的函数摘要包括前置约束信息、后置约束信息和函数特征信息三部分,实现了上下文敏感的跨函数分析.文中方法已在缺陷检测系统DTS中实现,在大型开源软件分析中的实验结果表明,该方法能减少误报和漏报.     

C程序内存泄漏智能化检测方法

内存泄漏在采用显式内存管理机制的C语言中是一种常见的代码缺陷,内存泄漏的检测方法目前主要是静态分析与动态检测.动态检测开销大,且高度依赖测试用例;静态分析目前被学术界和工业界广泛应用,但是存在大量误报,需要人工对检测结果进行确认.内存泄漏静态分析的误报通常是由于对指针、分支语句和全局变量分析的不准确性导致的.提出了一种内存泄漏的智能化检测方法,通过使用机器学习算法学习程序特征与内存泄漏之间的相关性,构建机器学习分类器,并应用机器学习分类器进一步提高内存泄漏静态分析的准确性.首先构建机器学习分类器,然后通过静态分析方法构建从内存分配点开始的Sparse Value Flow Graph（SVFG）,并从中提取内存泄漏相关特征,再使用规则和机器学习分类器进行内存泄漏的检测.实验结果显示,该方法在分析指针、分支语句和全局变量时是有效的,能够提高内存泄漏检测的准确性,降低内存泄漏检测结果的误报.最后,对未来研究的可行性以及面临的挑战进行了展望.     

一种路径敏感的静态缺陷检测方法

提出一种多项式复杂度的路径敏感静态缺陷检测算法.该方法采用变量的抽象取值范围来表示属性状态条件,通过属性状态条件中的变量抽象取值范围为空来判断不可达路径.在控制流图(control flow graph,简称CFG)中的汇合节点上合并相同属性状态的状态条件,从而避免完整路径上下文分析的组合爆炸问题.该算法已应用于缺陷检测系统DTS(defect testing system).实际测试结果表明,该方法能够减少误报.     

Filtering false alarms of buffer overflow analysis using SMT solvers

Buffer overflow detection using static analysis can provide a powerful tool for software programmers to find difficult bugs in C programs. Sound static analysis based on abstract interpretation, however, often suffers from false alarm problem. Although more precise abstraction can reduce the number of the false alarms in general, the cost to perform such analysis is often too high to be practical for large software. On the other hand, less precise abstraction is likely to be scalable in exchange for the increased false alarms. In order to attain both precision and scalability, we present a method that first applies less precise abstraction to find buffer overflow alarms fast, and selectively applies a more precise analysis only to the limited areas of code around the potential false alarms. In an attempt to develop the precise analysis of alarm filtering for large C programs, we perform a symbolic execution over the potential alarms found in the previous analysis, which is based on the abstract interpretation. Taking advantage of a state-of-art SMT solver, our precise analysis efficiently filters out a substantial number of false alarms. Our experiment with the test cases from three open source programs shows that our filtering method can reduce about 68% of false alarms on average.     

Predicate-transformer semantics of general recursion

Summary We develop the semantics of a language with arbitrary atomic statements, unbounded nondeterminacy, and mutual recursion. The semantics is expressed in weakest preconditions and weakest liberal preconditions. Individual states are not mentioned. The predicates on the state space are treated as elements of a distributive lattice. The semantics of recursion is constructed by means of the theorem of Knaster-Tarski. It is proved that the law of the excluded miracle can be preserved, if that is wanted. The universal conjunctivity of the weakest liberal precondition, and the connection between the weakest precondition and the weakest liberal precondition are proved to remain valid. Finally we treat Hoare-triple methods for proving correctness and conditional correctness of programs.     

False alarm moderation for performance monitoring in industrial water distribution systems

While considerable attention has been given to data driven methods that analyse and control energy systems in buildings, the same cannot be said for building water systems. As a result, approaches which support enhanced efficiency in building water consumption are somewhat underdeveloped, particularly in industrial settings. Water consumption in industrial systems features non-stationarity (i.e., variations in statistical properties over time), making it challenging to distinguish between routine and non-routine water uses. In such scenarios, fault detection and diagnosis methods that leverage multivariate statistical process control with, for example, principal component analysis and detection indices (Hotelling T²-statistics and Q-statistics), can be successfully used to identify system alarms. However, even with these approaches there can be a high prevalence of false alarms leading to low industry uptake of fault detection and diagnosis systems, or where in place, alarms can be ignored. To efficiently detect and diagnose water distribution system faults, false alarms should be controlled through false alarm moderation approaches so that building managers/operators only need to focus on critical system alarms or system alarms with high risk levels. This paper utilises two statistical non-parametric false alarm moderation approaches (window-based, and trial-based) that generate a second control limit for T²-statistics and Q-statistics. The implementation of these false alarm moderation approaches was combined with principal component analysis to detect faults with real water time series data from two case-study sites. Using both approaches false alarms were reduced, and the overall performance and reliability of the fault detection and diagnosis approach was improved. The principal component analysis model with the window-based approach was shown to be particularly effective.     

一种面向Trace与漏洞验证的污点分析方法

静态分析方法被广泛用于Android应用的隐私泄露检测,其以(Source,Sink)对形式检测潜在漏洞,但同时会产生大量虚警。针对该问题,提出一种上下文敏感和域敏感的污点分析方法。对污点传播的操作语义和一致性约束进行形式化定义,保证污点传播的语义正确性,同时分析插桩运行Android应用后产生的Trace片段,验证漏洞是否存在虚警。基于Soot实现原型系统并对DroidBench数据集中的70个应用进行分析,实验结果表明,该方法可成功验证4个虚警并发现8个漏报,表明其能有效判断静态分析结果的正确性。     

Commutativity of quantum weakest preconditions

The notion of quantum weakest precondition was introduced by D'Hondt and P. Panangaden [E. D'Hondt, P. Panangaden, Quantum weakest preconditions, Mathematical Structures in Computer Science 16 (2006) 429-451], and they presented a representation of weakest precondition of a quantum program in the operator-sum form. In this Letter, we give an intrinsic characterization of the weakest precondition of a quantum program given in a system-environment model. Furthermore, some sufficient conditions for commutativity of quantum weakest preconditions are presented.     

Intrusion detection alarms reduction using root cause analysis and clustering

As soon as the Intrusion Detection System (IDS) detects any suspicious activity, it will generate several alarms referring to as security breaches. Unfortunately, the triggered alarms usually are accompanied with huge number of false positives. In this paper, we use root cause analysis to discover the root causes making the IDS triggers these false alarms; most of these root causes are not attacks. Removing the root causes enhances alarms quality in the future. The root cause instigates the IDS to trigger alarms that almost always have similar features. These similar alarms can be clustered together; consequently, we have designed a new clustering technique to group IDS alarms and to produce clusters. Then, each cluster is modeled by a generalized alarm. The generalized alarms related to root causes are converted (by the security analyst) to filters in order to reduce future alarms’ load. The suggested system is a semi-automated system helping the security analyst in specifying the root causes behind these false alarms and in writing accurate filtering rules. The proposed clustering method was verified with three different datasets, and the averaged reduction ratio was about 74% of the total alarms. Application of the new technique to alarms log greatly helps the security analyst in identifying the root causes; and then reduces the alarm load in the future.     

The influence of alarm timing on driver response to collision warning systems following system failure

This driving simulator study focuses on false and missing alarms produced by a forward collision warning system and estimates the effect of alarm timing on driver response to alarm malfunction from the perspective of driver trust in alarms. The results show that drivers who experience late alarms are reluctant to respond to a false alarm and are not influenced by a missed alarm; however, drivers who experience early alarms tend to respond to a false alarm and suffer a delayed response to critical situations when a missing alarm happens. Furthermore, drivers whose judgement of trust is relatively high, tend to exhibit delayed braking, compared with drivers that have lower levels of trust. Driver behaviour towards false and missed alarms may vary according to alarm timing and its influence on trust in alarms; moreover, impaired system effectiveness caused by alarm malfunction may be mitigated by manipulating alarm timing.     

The influence of alarm timing on driver response to collision warning systems following system failure

This driving simulator study focuses on false and missing alarms produced by a forward collision warning system and estimates the effect of alarm timing on driver response to alarm malfunction from the perspective of driver trust in alarms. The results show that drivers who experience late alarms are reluctant to respond to a false alarm and are not influenced by a missed alarm; however, drivers who experience early alarms tend to respond to a false alarm and suffer a delayed response to critical situations when a missing alarm happens. Furthermore, drivers whose judgement of trust is relatively high, tend to exhibit delayed braking, compared with drivers that have lower levels of trust. Driver behaviour towards false and missed alarms may vary according to alarm timing and its influence on trust in alarms; moreover, impaired system effectiveness caused by alarm malfunction may be mitigated by manipulating alarm timing.     

Webprobe:自验证的Web服务安全探测工具

为了有效解决现存网络安全扫描工具中普遍存在的高误判率问题，提出了基于试探攻击和漏洞验证来评估Web服务安全的方法，描述了一个用该方法实现的Web服务安全探测工具——Webprobe，对比和讨论了现存Web服务器扫描软件的判断不准确的问题。实验证明，这种自验证方法可以大大降低误判率，提高网络安全管理人员的工作效率。     

Requirements for sequential flow and static image analysis—a preliminary study

The hybridization of flow and image analysis in the prescreening of gynecological smears combines the advantages of both methods. Taking the Heidelberg flow analysis system (HEIFAS) as an example the prerequisites of a successful combination of both systems are presented: (a) preservation of cell morphology; (b) avoidance of preferential cell loss; (c) ability to restain sorted cells; and (d) recognition of false alarms at high resolution. Two TV-based imaging instruments have been applied to cells sorted by two-parameter flow cytometry. Both instruments operating in the absorption mode (FAZYTAN) as well as in the fluorescence mode (LEYTAS) allow the detection of false alarms in flow. This preliminary study shows, that a discrimination of false alarms and true suspicious cells was found to be possible.