入侵检测系统中报警验证模块的设计与实现

传统入侵检测系统虽然可以根据特征匹配的方法检测出攻击企图,却无法验证攻击企图是否成功,生成的报警不仅数量巨大而且误警率很高。该文提出一种结合漏洞扫描工具对入侵检测系统生成的报警进行验证的方法,根据被攻击主机是否包含能使攻击成功的漏洞来判定攻击能否成功,对攻击的目标主机不存在对应漏洞的报警降低优先级,从而提高报警质量。说明了报警验证模型各部分的设计和实现方法,系统运行结果显示该方法能有效地压缩报警量,降低误警率,帮助管理员从大量数据中找到最应该关注的真实报警。     

基于代价敏感神经网络的警告分类研究

静态分析工具可以帮助开发人员在项目编码初期定位可能存在缺陷的代码。然而有研究表明,此类工具往往会报告大量的警告,且其中大部分为误报警告。为了增强静态分析工具的可用性,研究者们通常采用统计和机器学习方法将警告分类为有效警告和误报警告。然而,现有警告分类方法并未考虑大量误报警告造成警告数据类不平衡问题,以及误分类代价不等的问题。鉴于此,分别将BP神经网络和基于过采样、阈值操作、欠采样方法的代价敏感神经网络应用到有效警告的分类中。实验结果对比发现,相比BP神经网络,基于代价敏感神经网络方法在有效警告查全率方面平均提高了44.07%,且当有效警告被误分类的代价高于一定值时,代价敏感分类方法能得到更低的分类代价。     

基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具.这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测.但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全.为了解决这些问题,文中提出...     

Alattin: mining alternative patterns for defect detection

To improve software quality, static or dynamic defect-detection tools accept programming rules as input and detect their violations in software as defects. As these programming rules are often not well documented in practice, previous work developed various approaches that mine programming rules as frequent patterns from program source code. Then these approaches use static or dynamic defect-detection techniques to detect pattern violations in source code under analysis. However, these existing approaches often produce many false positives due to various factors. To reduce false positives produced by these mining approaches, we develop a novel approach, called Alattin, that includes new mining algorithms and a technique for detecting neglected conditions based on our mining algorithm. Our new mining algorithms mine patterns in four pattern formats: conjunctive, disjunctive, exclusive-disjunctive, and combinations of these patterns. We show the benefits and limitations of these four pattern formats with respect to false positives and false negatives among detected violations by applying those patterns to the problem of detecting neglected conditions.     

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

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

基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销.     

基于静态检测工具的源代码安全缺陷检测研究*

针对已有的使用单个静态检测工具进行源代码安全缺陷检测存在的漏报率和误报率很高的问题,提出了一种基于多种静态检测工具的检测方法。该方法通过对多种工具的检测结果进行统计分析,有效地降低了漏报率和误报率。设计和实现了一个可扩展的源代码静态分析工具平台,并通过实验表明,相对于单个工具的检测结果而言,该平台明显降低了漏报率和误报率。     

基于数据融合的源代码静态分析

采用数据融合技术对源代码进行静态分析,实现可扩展的原型系统。对现有静态分析工具的分析结果进行解析和数据融合,并对相应的参数进行估计。为便于读取和分析输出结果,采用XML格式输出结果。对常用网络软件进行测试,结果表明相对于单个源代码分析工具,该技术有效地降低了误报率和漏报率。     

Executable formal specifications of complex distributed systems with CoreASM

Formal specifications play a crucial role in the design of reliable complex software systems. Executable formal specifications allow the designer to attain early validation and verification of design using static analysis techniques and accurate simulation of the runtime behavior of the system-to-be. With increasing complexity of software-intensive computer-based systems and the challenges of validation and verification of abstract software models prior to coding, the need for interactive software tools supporting executable formal specifications is even more evident. In this paper, we discuss how CoreASM, an environment for writing and running executable specifications according to the ASM method, provides flexibility and manages the complexity by using an innovative extensible language architecture.     

基于数据融合的源代码静态分析漏洞检测技术

针对目前现有静态分析方法存在的漏报率和误报率较高的问题,提出一种基于数据融合的源代码静态分析漏洞检测技术.该技术通过对不同检测方法的分析结果进行解析和数据融合,有效地降低误报率和漏报率.设计与实现了一个可扩展的源代码静态分析工具原型,可通过用户的反馈信息自动寻优.实验结果表明:相对于单个漏洞检测方法而言,该方法的误报率和漏报率明显降低.     

A model-extraction approach to verifying concurrent C programs with CADP

The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account; (2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system; (3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs.     

一种基于多因素的告警关联方法

入侵检测系统作为保护网络安全的重要工具已被广泛使用,其通常产生大量冗余度高、误报率高的告警。告警关联分析通过对底层告警进行综合分析与处理,揭示出其中包含的多步攻击行为。许多告警关联方法通过在历史告警中挖掘频繁模式来构建攻击场景,方法容易受冗余告警、误报影响,挖掘出的多步攻击链在某些情况下不能反映出真实的多步攻击行为。为此,提出一种基于多因素的多步攻击关联方法。通过聚合原始告警以得到超级告警,降低冗余告警带来的影响;将超级告警构造成超级告警时间关系图,同时结合超级告警间的多因素关联度评价函数从时间关系图中挖掘出多步攻击场景。实验结果表明,该方法能克服冗余告警及大部分误报带来的负面影响、有效地挖掘出多步攻击链。     

常用循环摘要的自动生成方法及其应用

采用形式化方法证明软件的正确性是保障软件可靠性的有效方法,而对循环语句的分析与验证是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.本文提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要.同时,本文提出了一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,我们可以自动生成循环语句的规约,包括循环不变式、循环的前置条件以及循环的后置条件.我们已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中,实验表明,我们的方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担.     

面向SQLite3数据库API调用序列的并行运行时验证方法

作为轻量级的高可靠嵌入式数据库, SQLite3已被广泛应用于航空航天和操作系统等多个安全攸关领域, 其提供了丰富灵活API函数以支持用户快速实现项目构建.然而, 不正确的API函数调用序列会导致严重后果, 包括运行错误、内存泄露和程序崩溃等.为了高效准确地监控SQLite3数据库API函数的正确调用情况, 本文提出了基于多核系统的并行运行时验证方法.该方法首先分析API函数文档, 自动挖掘相关API调用序列规约描述, 辅助人工将其形式化表达为具有完全正则表达能力的命题投影时序逻辑公式; 然后在程序运行时, 采用多任务调度策略, 将程序执行产生的状态序列分割并对不同片段并行验证.实验结果表明, 该方法能够发现调用SQLite3数据库API函数的30个被验证C程序中, 违背API函数调用序列规约的达16个.另外, 与传统串行运行时验证方法的对比实验表明, 本文提出的并行运行时验证方法能够有效提高多核系统的验证效率.     

Automatic Buffer Overflow Warning Validation

Static buffer overflow detection techniques tend to report too many false positives fundamentally due to the lack of software execution information. It is very time consuming to manually inspect all the static warnings. In this paper, we propose BovInspector, a framework for automatically validating static buffer overflow warnings and providing suggestions for automatic repair of true buffer overflow warnings for C programs. Given the program source code and the static buffer overflow warnings, BovInspector first performs warning reachability analysis. Then, BovInspector executes the source code symbolically under the guidance of reachable warnings. Each reachable warning is validated and classified by checking whether all the path conditions and the buffer overflow constraints can be satisfied simultaneously. For each validated true warning, BovInspector provides suggestions to automatically repair it with 11 repair strategies. BovInspector is complementary to prior static buffer overflow discovery schemes. Experimental results on real open source programs show that BovInspector can automatically validate on average 60% of total warnings reported by static tools.

     

开源CC++静态软件缺陷检测工具实证研究

软件静态缺陷检测是软件安全领域中的一个研究热点.随着使用C/C++语言编写的软件规模和复杂度的逐渐提高, 软件迭代速度的逐渐加快, 由于静态软件缺陷检测不需要运行目标代码即可发现其中潜藏的缺陷, 因而在工业界和学术界受到了更广泛的关注.近年来涌现大量使用软件静态分析技术的检测工具, 并在不同领域的软件项目中发挥了不可忽视的作用, 但是开发者仍然对静态缺陷检测工具缺乏信心.高误报率是C/C++静态缺陷检测工具难以普及的首要原因.因此, 我们选择现有较为完善的开源C/C++静态缺陷检测工具, 在Juliet基准测试集和37个良好维护的开源软件项目上对特定类型缺陷的检测效果进行了深入研究, 结合检测工具的具体实现归纳了导致静态缺陷检测工具产生误报的关键原因.同时, 我们通过研究静态缺陷检测工具的版本迁移轨迹, 总结出了当下静态分析工具的发展方向和未来趋势, 有助未来静态分析技术的优化和发展, 从而实现静态缺陷检测工具的普及应用.     

Architecting Fault Tolerance with Exception Handling: Verification and Validation

When building dependable systems by integrating untrusted software components that were not originally designed to interact with each other, it is likely the occurrence of architectural mismatches related to assumptions in their failure behaviour. These mismatches, if not prevented during system design, have to be tolerated during runtime. This paper presents an architectural abstraction based on exception handling for structuring fault-tolerant software systems. This abstraction comprises several components and connectors that promote an existing untrusted software element into an idealised fault-tolerant architectural element. Moreover, it is considered in the context of a rigorous software development approach based on formal methods for representing the structure and behaviour of the software architecture. The proposed approach relies on a formal specification and verification for analysing exception propagation, and verifying important dependability properties, such as deadlock freedom, and scenarios of architectural reconfiguration. The formal models are automatically generated using model transformation from UML diagrams: component diagram representing the system structure, and sequence diagrams representing the system behaviour. Finally, the formal models are also used for generating unit and integration test cases that are used for assessing the correctness of the source code. The feasibility of the proposed architectural approach was evaluated on an embedded critical case study. Patrick Brito is supported by Fapesp/Brazil under Grant No. 06/02116–2 and CAPES/Brazil under Grant No. 0722–07–3. Cecília Rubira is partially supported by CNPq/Brazil under Grant Nos. 301446/2006–7 and 484138/2006–5.     

WYSIWIB: exploiting fine‐grained program structure in a scriptable API‐usage protocol‐finding process

Bug‐finding tools rely on specifications of what is correct or incorrect code. As it is difficult for a tool developer or user to anticipate all possible specifications, strategies for inferring specifications have been proposed. These strategies obtain probable specifications by observing common characteristics of code or execution traces, typically focusing on sequences of function calls. To counter the observed high rate of false positives, heuristics have been proposed for ranking or pruning the results. These heuristics, however, can result in false negatives, especially for rarely used functions. In this paper, we propose an alternate approach to specification inference, in which the user guides the inference process using patterns of code that reflect the user's understanding of the conventions and design of the targeted software project. We focus on specifications describing the correct usage of API functions, which we refer to as API protocols. Our approach builds on the Coccinelle program matching and transformation tool, which allows a user to construct patterns that reflect the structure of the code to be matched. We evaluate our approach on the source code of the Linux kernel, which defines a very large number of API functions with varying properties. Linux is also critical software, implying that fixing even bugs involving rarely used protocols is essential. In our experiments, we use our approach to find over 3000 potential API protocols, with an estimated false positive rate of under 15% and use these protocols to find over 360 bugs in the use of API functions. Copyright © 2012 John Wiley & Sons, Ltd.     

Building a push-button RESOLVE verifier: Progress and challenges

A central objective of the verifying compiler grand challenge is to develop a push-button verifier that generates proofs of correctness in a syntax-driven fashion similar to the way an ordinary compiler generates machine code. The software developer??s role is then to provide suitable specifications and annotated code, but otherwise to have no direct involvement in the verification step. However, the general mathematical developments and results upon which software correctness is based may be established through a separate formal proof process in which proofs might be mechanically checked, but not necessarily automatically generated. While many ideas that could conceivably form the basis for software verification have been known ??in principle?? for decades, and several tools to support an aspect of verification have been devised, practical fully automated verification of full software behavior remains a grand challenge. This paper explains how RESOLVE takes a step towards addressing this challenge by integrating foundational and practical elements of software engineering, programming languages, and mathematical logic into a coherent framework. Current versions of the RESOLVE verifier generate verification conditions (VCs) for the correctness of component-based software in a modular fashion??one component at a time. The VCs are currently verified using automated capabilities of the Isabelle proof assistant, the SMT solver Z3, a minimalist rewrite prover, and some specialized decision procedures. Initial experiments with the tools and further analytic considerations show both the progress that has been made and the challenges that remain.     

Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions

Symbolic simulation and uninterpreted functions have long been staple techniques for formal hardware verification. In recent years, we have adapted these techniques for the automatic, formal verification of low-level embedded software—specifically, checking the equivalence of different versions of assembly language programs. Our approach, though limited in scalability, has proven particularly promising for the intricate code optimizations and complex architectures typical of high-performance embedded software, such as for DSPs and VLIW processors. Indeed, one of our key findings was how easy it was to create or retarget our verification tools to different, even very complex, machines. The resulting tools automatically verified or found previously unknown bugs in several small sequences of industrial and published example code. This paper provides an introduction to these techniques and a review of our results.