首页 | 官方网站   微博 | 高级检索  
相似文献
 共查询到10条相似文献,搜索用时 153 毫秒
1.
We present an overview of the latest developments in the detection of metamorphic and virtualization-based malware using an algebraic specification of the Intel 64 assembly programming language. After giving an overview of related work, we describe the development of a specification of a subset of the Intel 64 instruction set in Maude, an advanced formal algebraic specification tool. We develop the technique of metamorphic malware detection based on equivalence-in-context so that it is applicable to imperative programming languages in general, and we give two detailed examples of how this might be used in a practical setting to detect metamorphic malware. We discuss the application of these techniques within anti-virus software, and give a proof-of-concept system for defeating detection counter-measures used by virtualization-based malware, which is based on our Maude specification of Intel 64. Finally, we compare formal and informal approaches to malware detection, and give some directions for future research.  相似文献   

2.
We describe the formal design techniques currently used in IBM to develop cache protocol controllers for high-end servers. In our approach to formal design, formal specification and verification methods are incorporated into the hardware design process, starting from the earliest stages of a hardware project. We describe collaborations between a formal methods expert and hardware designers on two high performance server projects. Properties of the design are verified using both manual proof techniques and model checking. We discuss the modelling and model checking techniques we have developed and indicate future directions.  相似文献   

3.
Open standardization seems to be very popular among software developers as it simplifies the standard’s adoption by the software engineering. Formal specification methods, while very promising, are being adopted slowly as the industry seems to have little motivation to move into this territory. In this paper the authors present (1) the idea of applying formal specification techniques to open standards’ specifications, and (2) an example of a formal specification of the Rich Site Summary (RSS) v2.0 open standard. The authors provide evidence for the advantages of the open standards formal specification over natural language documentations: formal specifications are more concise, less ambiguous, more complete with respect to the original documentation and, when using certain kinds of specification languages, executable and reusable as they support module inheritance. The merging of formal specification methods and open standards allows (1) a more concrete standard design; (2) an improved understanding of the environment under design; (3) an enforced certain level of precision into the specification, and also (4) provides software engineers with extended property checking/verification capabilities, especially if they opt to use any algebraic specification language. The authors showcase how the RSS standard can be formally specified using an algebraic specification language and demonstrate how can that be beneficial.  相似文献   

4.
A formal semantics for an active functional DBPL   总被引:1,自引:1,他引:0  
We describe how the functional database programming language PFL is extended with an active component without compromising either its declarative semantics or its syntax. We give a formal specification of the active component using PFL itself, including event specification and detection, parameter-binding, reaction scheduling and abort handling. We describe how a user-specified function can be cast as a primitive event, and discuss the expressiveness of events and the optimisation of event detection.  相似文献   

5.
6.
Mechanised support for sound refinement tactics   总被引:1,自引:0,他引:1  
ArcAngel is a tactic language devised to facilitate and automate program developments using Morgan’s refinement calculus. It is especially well suited for the specification of high-level refinement strategies, and equipped with a formal semantics that additionally permits reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine the interplay between ArcAngel tactics and the native reasoning support of the prover. We also discuss several extensions of ArcAngel that have been entailed by our implementation effort. They are of practical importance and provide a unification of the related tactic languages Angel and ArcAngel C. Our main result is a mechanisation that reflects directly the ArcAngel semantics, and can be used with any programming model for refinement. The approach can be used to support other formal tactic languages using other theorem provers.  相似文献   

7.
8.
We propose a run-time monitoring and checking architecture for network protocols called Network Event Recognition. Our framework is based on passively monitoring the packet trace produced by a protocol implementation and checking it for properties written in a formal specification language, NERL. In this paper, we describe the design requirements for NERL. We show how the unique requirements of network protocol monitoring impact design and implementation options. Finally we outline our prototype implementation of NERL and discuss two case studies: checking the correctness of network protocol simulations and privacy issues in packet-mode surveillance.  相似文献   

9.
10.
基于设计决定的逐步求精方法及环境   总被引:4,自引:1,他引:3  
缪旭  唐稚松 《软件学报》1990,1(3):15-25
逐步描述、变换及证明的软件开发过程包含两个转换,一是从非形式的用户需求到形式描述,一是从形式描述到算法实现。开发过程中的关键是如何做出设计决定。为了更好地维护、重用软件以及程序证明,不仅仅要对软件的形式描述及实现做文档记录,也要记下开发过程中所做的每一步决定。我 们用两个例子来说明如上这种逐步求精的方法以及设计决定在其中所起的作用,并且我们实现了一个包括SPEC、OOMM、PROT、VERI几个子系统组成的环境来支持上述过程。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司    京ICP备09084417号-23

京公网安备 11010802026262号