工业控制网络互联互通的安全问题

针对工业控制系统使用的OPC(Object Linking and Embedding for Process Control)通信协议的安全防护,通过分析OPC客户机和服务器之间的网络流,用截获的网络帧说明如何开放动态生成的TCP连接会话、如何识别同步读写帧,怎样对数据读写操作过滤;强调指出,这种传统的防火墙保护模式,仍可能存在利用暴露的密码攻击、假冒应用要求恶意增加访问次数破坏控制系统运行、借助不明信息流渗透攻击的隐患,为此给出一个防火墙多端口分区保护纵深防御的方案。     

一种基于虚拟组织的网格安全协议形式化验证方法

虚拟组织是网格计算的基本管理单元,而协同计算组是虚拟组织形成的基础。对应于网格计算的复杂性,网格安全协议的分析与证明十分复杂。通过引入网格计算信道的概念,在传统Strand Space理论的基础上提出了一种基于虚拟组织的网格安全协议形式化验证方法,实现了网格环境下多用户协同计算安全协议的分析与证明。     

A formal methodology for integral security design and verification of network protocols

In this work we propose a methodology for incorporating the verification of the security properties of network protocols as a fundamental component of their design. This methodology can be separated in two main parts: context and requirements analysis along with its informal verification; and formal representation of protocols and the corresponding procedural verification. Although the procedural verification phase does not require any specific tool or approach, automated tools for model checking and/or theorem proving offer a good trade-off between effort and results. In general, any security protocol design methodology should be an iterative process addressing in each step critical contexts of increasing complexity as result of the considered protocol goals and the underlying threats. The effort required for detecting flaws is proportional to the complexity of the critical context under evaluation, and thus our methodology avoids wasting valuable system resources by analyzing simple flaws in the first stages of the design process. In this work we provide a methodology in coherence with the step-by-step goals definition and threat analysis using informal and formal procedures, being our main concern to highlight the adequacy of such a methodology for promoting trust in the accordingly implemented communication protocols. Our proposal is illustrated by its application to three communication protocols: MANA III, WEP's Shared Key Authentication and CHAT-SRP.     

Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.     

Ready for testing: ensuring conformance to industrial standards through formal verification

The design of distributed, safety-critical real-time systems is challenging due to their high complexity, the potentially large number of components, and complicated requirements and environment assumptions that stem from international standards. We present a case study that shows that despite those challenges, the automated formal verification of such systems is not only possible, but practicable even in the context of small to medium-sized enterprises. We considered a wireless fire alarm system, regulated by the EN 54 standard. We performed formal requirements engineering, modeling and verification and uncovered severe design flaws that would have prevented its certification. For an improved design, we provided dependable verification results which in particular ensure that certification tests for a relevant regulation standard will be passed. In general we observe that if system tests are specified by generalized test procedures, then verifying that a system will pass any test following those test procedures is a cost-efficient approach to improve the product quality based on formal methods. Based on our experience, we propose an approach useful to integrate the application of formal methods to product development in SME.     

Application of formal verification and behaviour abstraction to the service interaction problem in intelligent networks

One of the major drawbacks for the use of formal methods is the excessive size of the state-spaces representing behaviours of industrial-sized specifications of concrete systems. Existing verification algorithms simply are often not applicable to the large systems of practical relevance. One can improve the applicability of verification methods by orders of magnitude by ignoring parts of a behaviour which contain no information with respect to a given verification task. We focus on exactly such an abstraction based way of dealing with large, so called industrial-sized systems and discuss its application in an industrial project aiming at the detection of service interactions in Intelligent Networks on the specification level. The concrete application of the abstraction and verification method is presented mainly by considering an example taken from the service interaction project.     

A formal role-based access control model for security policies in multi-domain mobile networks

Mobile users present challenges for security in multi-domain mobile networks. The actions of mobile users moving across security domains need to be specified and checked against domain and inter-domain policies. We propose a new formal security policy model for multi-domain mobile networks, called FPM-RBAC, Formal Policy Model for Mobility with Role Based Access Control. FPM-RBAC supports the specification of mobility and location constraints, role hierarchy mapping, inter-domain services, inter-domain access rights and separation of duty. Associated with FPM-RBAC, we also present a formal security policy constraint specification language for domain and inter-domain security policies. Formal policy constraint specifications are based on ambient logic and predicate logic. We also use ambient calculus to specify the current state of a mobile network and actions within security policies for evaluation of access requests according to security policies. A novel aspect of the proposed policy model is the support for formal and automated analysis of security policies related to mobility within multiple security domains.     

Automated formal verification of visual modeling languages by model checking

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level.     

A framework for formal analysis and simulative evaluation of security attacks in wireless sensor networks

Journal of Computer Virology and Hacking Techniques - When designing Wireless Sensor Networks it is important to analyze their security risks and provide adequate solutions for protecting them from...     

A correctness proof of sorting by means of formal procedures

We consider a recursive sorting algorithm in which, in each invocation, a new variable and a new procedure (using the variable globally) are defined and the procedure is passed to recursive calls. This algorithm is proved correct with Hoare-style pre- and postassertions. We also discuss the same algorithm expressed as a functional program.     

On the role of formal methods in security

Separation of concerns and layers of abstraction have long been advocated by proponents of programming methodology and have been used effectively for building large scale systems. In this paper, we use recent developments on power analysis attacks on cryptographic implementations to raise some questions about the applicability of these approaches especially to cryptography and security.     

Code mutation techniques by means of formal grammars and automatons

The paper describes formalization of existing code mutation techniques widely used in a viruses (polymorphism and metamorphism) by means of formal grammars and automatons. New model of metamorphic viruses and new classification of this type of viruses are suggested. The statement about undetectable viruses of this type is proved. In that paper are shown iterative approach toward construct complex formal grammars from the simplest initial rules for building metamorphic generator. Also there are some samples of applied usage of formal grammar model. The experiment for system call tracing of some viruses and worms is described. Possibility of using system call sequences for viruses detecting is shown.     

Modular formal verification of specifications of concurrent systems

In this paper, we propose a bottom‐up approach for the verification of systems with modular structure: we prove that when the modules are composed in specific ways, the complete software system verifies a composition of the properties each component does. We focus on the process of upgrading systems with new functionalities, where the validity of old requirements needs to be ensured, but also an understanding of the new properties the upgraded system would enjoy is useful. In this work, we assume each component to be specified by a CCS process, and the properties to be expressed by selective mu‐calculus formulae. Copyright © 2007 John Wiley & Sons, Ltd.     

Algorithm for formal verification of business process templates

A formal definition of a business process template is presented that is based on an analysis of ITIL and MOF libraries. Definitions of an initialization precondition and an execution postcondition are introduced. The solvability of the formal verification problem for business process templates is shown under some given initialization precondition and execution postcondition. This research is planned to be continued with a view to (i) using a formal verification algorithm with other business process template libraries and (ii) examining other business process libraries to identify new classes of business processes.     

基于SCADE的形式化验证技术的改进研究

为保证SCADE软件开发的安全性,研究了SCADE形式化验证技术,指出其不足,提出了基于代码生成器的解决方法.该方法对安全特性属性引入了逻辑描述,并利用SCADE编辑器及代码生成器的特点,对SCADE形式化验证技术进行改进,降低了模型正确性确认时人为的主观性.通过实例阐述了应用该方法进行形式化验证的一般步骤,表明了该方法是有效可行的.     

Object-oriented specification and formal verification of real-time systems

An object-oriented approach for specification and verification of real-time systems is described in this paper. It is motivated by taking advantage of object-oriented techniques to produce real-time software that is easy to understand, maintain, and reuse. The approach specifies the structural, behavioral, and control aspects of objects in one model with a textual representation as well as a graphical representation. For ease to comprehend and use, the model encapsulates object states and allows an analyst to focus on specifying object operations one at a time. System behavior from individual objects can be deduced and analyzed. For safety considerations, the approach supports specification of failures to object behavior and their resultant faults. The approach also supports modeling of timed temporal constraints for specifying and verifying desirable real-time properties. An object timed temporal logic OTTL is defined for expressing the syntax and semantics of these constraints. Decision procedures for their verification are also presented.     

Selection of formal verification heuristics for parallel execution

Functional verification is “the” major design-phase bottleneck for silicon productivity. Since functional verification is an NP-complete problem, it relies on a large number of heuristics with associated parameters (engines). With the advent of parallel processing, formal verification can be optimized by selecting the best n engines to run in parallel, increasing the chance of reaching successful termination of the verification task. In this paper, we will present a methodology to build engine estimators based on structural metrics and to select n engines to run in parallel. The methodology considers both engines’ estimated performance and engines’ correlation. Results confirmed that the methodology can be a very quick selection mechanism for parallelization of engines in order to increase the chance of running the best engines to solve the problem.     

Improving the effectiveness of system verification

This special section presents three extended and revised papers which originally appeared in the proceedings of the 12th edition of the conference “Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006” held in Braga, Portugal late March 2006 as a constituent event of the “European joint conferences on Theory and Practice of Software”. All three papers deal with very promising extensions and integrations of formal verification techniques.     

Automated verification of security pattern compositions

Software security becomes a critically important issue for software development when more and more malicious attacks explore the security holes in software systems. To avoid security problems, a large software system design may reuse good security solutions by applying security patterns. Security patterns document expert solutions to common security problems and capture best practices on secure software design and development. Although each security pattern describes a good design guideline, the compositions of these security patterns may be inconsistent and encounter problems and flaws. Therefore, the compositions of security patterns may be even insecure. In this paper, we present an approach to automated verification of the compositions of security patterns by model checking. We formally define the behavioral aspect of security patterns in CCS through their sequence diagrams. We also prove the faithfulness of the transformation from a sequence diagram to its CCS representation. In this way, the properties of the security patterns can be checked by a model checker when they are composed. Composition errors and problems can be discovered early in the design stage. We also use two case studies to illustrate our approach and show its capability to detect composition errors.