Efficient SAT-based bounded model checking for software verification

This paper discusses our methodology for formal analysis and automatic verification of software programs. It is applicable to a large subset of the C programming language that includes pointer arithmetic and bounded recursion. We consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. We perform this analysis via a translation to a Boolean circuit representation based on modeling basic blocks. The program is then analyzed by a back-end SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program.     

Embedded software verification in hardware–software codesign

Concurrent Embedded Real-Time Software (CERTS) is intrinsically different from traditional, sequential, independent, and temporally unconstrained software. The verification of software is more complex than hardware due to inherent flexibilities (dynamic behavior) that incur a multitude of possible system states. The verification of CERTS is all the more difficult due to its concurrency and embeddedness. The work presented here shows how the complexity of CERTS verification can be reduced significantly through answering common engineering questions such as when, where, and how one must verify embedded software. First, a new Schedule-Verify-Map strategy is proposed to answer the when question. Second, verification under system concurrency is proposed to answer the where question. Finally, a complete symbolic model checking procedure is proposed for CERTS verification. Several application examples illustrate the usefulness of our technique in increasing verification scalability.     

Memory model sensitive bytecode verification

Modern concurrent programming languages like C# and Java have a programming language level memory model, which captures the set of all allowed behaviors of programs on any implementation platform—uni- or multi-processor. Such a memory model is typically weaker than Sequential Consistency and allows reordering of operations within a program thread. Therefore, programs verified correct by assuming Sequential Consistency (that is, each thread proceeds in program order) may not behave correctly on certain platforms! One solution to this problem is to develop program checkers which are memory model sensitive. In this paper, we develop a bytecode level invariant checker for the programming language C#. Our checker identifies program states which are reached only because the C# memory model is more relaxed than Sequential Consistency. It employs partial order reduction strategies to speed up the search. These strategies are different from standard partial order reduction methods since our search also considers execution traces containing bytecode re-orderings. Furthermore, our checker identifies (a) operation re-orderings which cause undesirable states to be reached, and (b) simple program modifications—by inserting memory barrier operations—which prevent such undesirable re-orderings. A preliminary version of this paper appeared as (Huynh and Roychoudhury, in: Formal Methods Symposium, 2006). The conference paper is available from . This work was done when the first author was a Research Assistant at National University of Singapore.     

Coherent clusters in source code

This paper presents the results of a large scale empirical study of coherent dependence clusters. All statements in a coherent dependence cluster depend upon the same set of statements and affect the same set of statements; a coherent cluster's statements have ‘coherent’ shared backward and forward dependence. We introduce an approximation to efficiently locate coherent clusters and show that it has a minimum precision of 97.76%. Our empirical study also finds that, despite their tight coherence constraints, coherent dependence clusters are in abundance: 23 of the 30 programs studied have coherent clusters that contain at least 10% of the whole program. Studying patterns of clustering in these programs reveals that most programs contain multiple substantial coherent clusters. A series of subsequent case studies uncover that all clusters of significant size map to a logical functionality and correspond to a program structure. For example, we show that for the program acct, the top five coherent clusters all map to specific, yet otherwise non-obvious, functionality. Cluster visualization also brings out subtle deficiencies in program structure and identifies potential refactoring candidates. A study of inter-cluster dependence is used to highlight how coherent clusters are connected to each other, revealing higher-level structures, which can be used in reverse engineering. Finally, studies are presented to illustrate how clusters are not correlated with program faults as they remain stable during most system evolution.     

On the Effective Deployment of Functional Formal Verification

We examine IBM's exploitation of formal verification using RuleBase—a formal verification tool developed by the IBM Haifa Research Laboratory. The goal of the paper is methodological. We identify an integrated methodology for the deployment of formal verification which involves three complementary modes: architectural verification, block-level verification, and design exploration.     

支持模型驱动开发的软构件形式化描述方法

针对模型驱动的软件开发(MDSD)中语义特性保持的描述和验证等问题,基于类型范畴理论的形式化框架和进程代数理论,提出了一种软件结构模型的形式化描述方法。在此基础上对模型转换前后构件规范之间应满足的语义约束进行了深入的分析和探讨,从图表结构、端口与配置约束、外部行为以及可替换性等四个方面对特性约束保持的问题进行了描述,并建立了相应的判定标准。该方法能为模型之间转换规则的定义提供指导,并为模型转换的效果分析和正确性验证提供依据。应用研究表明,该方法使得构件模型的语义描述能力显著增强,可作为已有软件建模方法的一个有效补充。     

A framework for the design and verification of software measurement methods

At the core of any engineering discipline is the use of measures, based on ISO standards or on widely recognized conventions, for the development and analysis of the artifacts produced by engineers. In the software domain, many alternatives have been proposed to measure the same attributes, but there is no consensus on a framework for how to analyze or choose among these measures. Furthermore, there is often not even a consensus on the characteristics of the attributes to be measured.In this paper, a framework is proposed for a software measurement life cycle with a particular focus on the design phase of a software measure. The framework includes definitions of the verification criteria that can be used to understand the stages of software measurement design. This framework also integrates the different perspectives of existing measurement approaches. In addition to inputs from the software measurement literature the framework integrates the concepts and vocabulary of metrology. This metrological approach provides a clear definition of the concepts, as well as the activities and products, related to measurement. The aim is to give an integrated view, involving the practical side and the theoretical side, as well as the basic underlying concepts of measurement.     

Formal verification of behaviour networks including sensor failures

The paper deals with the problem of verifying behaviour-based control systems. Although failures in sensor hardware and software can have strong influences on the robot’s operation, they are often neglected in the verification process. Instead, perfect sensing is assumed. Therefore, this paper provides an approach for modelling the sensor chain in a formal way and connecting it to the formal model of the control system. The resulting model can be verified using model checking techniques, which is shown on the examples of the control systems of an autonomous indoor robot and an autonomous off-road robot.     

The software model checker Blast

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs.     

物联网应用中访问控制智能合约的形式化验证

蓝牙、WiFi等网络技术的进步推动物联网(IoT)的发展,然而IoT在方便了人们生活的同时也存在严重的安全隐患.若无安全的访问控制,非法接入IoT的访问可能给用户带来各方面的损失.传统的访问控制方法需要一个可信任的中心节点,不适合节点分散的IoT环境.区块链及智能合约的出现为IoT应用的访问控制提供了更有效的解决方案,...     

基于Spin的安全协议形式化验证技术

针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑（ LTL）公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法：模型检测过程中的存储状态数减少,使模型复杂度降低约40';迁移状态数减少,使验证效率提升约44'。     

一种自动的形式化验证技术-模型检测

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.     

Improved verification of hardware designs through antecedent conditioned slicing

Static slicing has shown itself to be a valuable tool, facilitating the verification of hardware designs. In this paper, we present a sharpened notion, antecedent conditioned slicing that provides a more effective abstraction for reducing the size of the state space. In antecedent conditioned slicing, extra information from the antecedent is used to permit greater pruning of the state space. In a previous version of this paper, we applied antecedent conditioned slicing to safety properties of the form G(antecedent ⇒ consequent) where antecedent and consequent were written in propositional logic. In this paper, we use antecedent conditioned slicing to handle safety and bounded liveness property specifications written in linear time temporal logic. We present a theoretical justification of our technique. We provide experimental results on a Verilog RTL implementation of the USB 2.0 functional core, which is a large design with about 1,100 state elements (10³³¹ states). The results demonstrate that the technique provides significant performance benefits over static program slicing using state-of-the-art model checkers.     

Automatic software model checking via constraint logic

This paper proposes the use of constraint logic to perform model checking of imperative, infinite-state programs. We present a semantics-preserving translation from an imperative language with recursive procedures and heap-allocated mutable data structures into constraint logic. The constraint logic formulation provides a clean way to reason about the behavior and correctness of the original program. In addition, it enables the use of existing constraint logic implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration.     

基于梯形逻辑的联锁系统形式化验证方法

铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。     

Introductory paper

The computer-assisted resuscitation algorithm (CARA) is the software component of an automatic infusion pump system being designed by US Armys Walter Reed Institute of Research (WRAIR) to be used in the battlefields of tomorrow. Such medical devices are safety critical, and their use needs to be approved by the US Food and Drug Administration (FDA) – a process on which formal methods can have a great impact. In this special section, six papers on the analysis of CARAs requirements are presented. In the rest of this introduction, we present the framework and summary of results from those papers.     

基于TLA的事件图模型形式化验证方法*

针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法.该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型...     

An empirical study of the relationship between the concepts expressed in source code and dependence

Programs express domain-level concepts in their source code. It might be expected that such concepts would have a degree of semantic cohesion. This cohesion ought to manifest itself in the dependence between statements all of which contribute to the computation of the same concept. This paper addresses a set of research questions that capture this informal observation. It presents the results of experiments on 10 programs that explore the relationship between domain-level concepts and dependence in source code. The results show that code associated with concepts has a greater degree of coherence, with tighter dependence. This finding has positive implications for the analysis of concepts as it provides an approach to decompose a program into smaller executable units, each of which captures the behaviour of the program with respect to a domain-level concept.     

Formal verification of static software models in MDE: A systematic review

ContextModel-driven Engineering (MDE) promotes the utilization of models as primary artifacts in all software engineering activities. Therefore, mechanisms to ensure model correctness become crucial, specially when applying MDE to the development of software, where software is the result of a chain of (semi)automatic model transformations that refine initial abstract models to lower level ones from which the final code is eventually generated. Clearly, in this context, an error in the model/s is propagated to the code endangering the soundness of the resulting software. Formal verification of software models is a promising approach that advocates the employment of formal methods to achieve model correctness, and it has received a considerable amount of attention in the last few years.ObjectiveThe objective of this paper is to analyze the state of the art in the field of formal verification of models, restricting the analysis to those approaches applied over static software models complemented or not with constraints expressed in textual languages, typically the Object Constraint Language (OCL).MethodWe have conducted a Systematic Literature Review (SLR) of the published works in this field, describing their main characteristics.ResultsThe study is based on a set of 48 resources that have been grouped in 18 different approaches according to their affinity. For each of them we have analyzed, among other issues, the formalism used, the support given to OCL, the correctness properties addressed or the feedback yielded by the verification process.ConclusionsOne of the most important conclusions obtained is that current model verification approaches are strongly influenced by the support given to OCL. Another important finding is that in general, current verification tools present important flaws like the lack of integration into the model designer tool chain or the lack of efficiency when verifying large, real-life models.     

Integrated static code analysis and runtime verification

Static code analysis tools automatically generate alerts for potential software faults that can lead to failures. However, these tools usually generate a very large number of alerts, some of which are subject to false positives. Because of limited resources, it is usually hard to inspect all the alerts. As a complementary approach, runtime verification techniques verify dynamic system behavior with respect to a set of specifications. However, these specifications are usually created manually based on system requirements and constraints. In this paper, we introduce a noval approach and a toolchain for integrated static code analysis and runtime verification. Alerts that are generated by static code analysis tools are utilized for automatically generating runtime verification specifications. On the other hand, runtime verification results are used for automatically generating filters for static code analysis tools to eliminate false positives. The approach is illustrated for the static analysis and runtime verification of an open‐source bibliography reference manager software. Copyright © 2014 John Wiley & Sons, Ltd.