共查询到20条相似文献,搜索用时 15 毫秒
1.
2.
虚拟组织是网格计算的基本管理单元,而协同计算组是虚拟组织形成的基础。对应于网格计算的复杂性,网格安全协议的分析与证明十分复杂。通过引入网格计算信道的概念,在传统Strand Space理论的基础上提出了一种基于虚拟组织的网格安全协议形式化验证方法,实现了网格环境下多用户协同计算安全协议的分析与证明。 相似文献
3.
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. 相似文献
4.
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. 相似文献
5.
6.
Sergio Feo-Arenis Bernd Westphal Daniel Dietsch Marco Muñiz Siyar Andisha Andreas Podelski 《Formal Aspects of Computing》2016,28(3):499-527
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. 相似文献
7.
Application of formal verification and behaviour abstraction to the service interaction problem in intelligent networks 总被引:1,自引:0,他引:1
Ulrich Nitsche 《Journal of Systems and Software》1998,40(3):227-248
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. 相似文献
8.
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. 相似文献
9.
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. 相似文献
10.
Bernardeschi Cinzia Dini Gianluca Palmieri Maurizio Racciatti Francesco 《Journal in Computer Virology》2021,17(3):249-263
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... 相似文献
11.
《Science of Computer Programming》1987,9(3):263-269
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. 相似文献
12.
《Information Processing Letters》2001,77(2-4):209-212
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. 相似文献
13.
Pavel V. Zbitskiy 《Journal in Computer Virology》2009,5(3):199-207
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. 相似文献
14.
Sara Gradara Antonella Santone Gigliola Vaglini Maria Luisa Villani 《Software Testing, Verification and Reliability》2008,18(1):5-28
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. 相似文献
15.
A. S. Varosyan 《Cybernetics and Systems Analysis》2011,47(2):228-240
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. 相似文献
16.
为保证SCADE软件开发的安全性,研究了SCADE形式化验证技术,指出其不足,提出了基于代码生成器的解决方法.该方法对安全特性属性引入了逻辑描述,并利用SCADE编辑器及代码生成器的特点,对SCADE形式化验证技术进行改进,降低了模型正确性确认时人为的主观性.通过实例阐述了应用该方法进行形式化验证的一般步骤,表明了该方法是有效可行的. 相似文献
17.
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. 相似文献
18.
Georgia Penido Safe Claudionor Coelho Jr. Luiz Filipe M. Vieira Celina Gomes Do Val Jose Augusto Nacif Antonio Otavio Fernandes 《International Journal on Software Tools for Technology Transfer (STTT)》2012,14(1):95-108
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. 相似文献
19.
Holger Hermanns Jens Palsberg 《International Journal on Software Tools for Technology Transfer (STTT)》2008,10(2):111-112
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. 相似文献
20.
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. 相似文献