共查询到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.
Steven M. German 《Formal Methods in System Design》2003,22(2):133-141
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.
Konstantinos Barlas Eleni Berki Petros Stefaneas George Koletsos 《Innovations in Systems and Software Engineering》2017,13(1):51-66
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
Alexandra Poulovassilis Swarup Reddi Carol Small 《Journal of Intelligent Information Systems》1996,7(2):151-172
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.
Formal specification and analysis of distributed systems 总被引:1,自引:0,他引:1
HENRIKAS PRANEVICIUS 《Journal of Intelligent Manufacturing》1998,9(6):559-569
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
逐步描述、变换及证明的软件开发过程包含两个转换,一是从非形式的用户需求到形式描述,一是从形式描述到算法实现。开发过程中的关键是如何做出设计决定。为了更好地维护、重用软件以及程序证明,不仅仅要对软件的形式描述及实现做文档记录,也要记下开发过程中所做的每一步决定。我 们用两个例子来说明如上这种逐步求精的方法以及设计决定在其中所起的作用,并且我们实现了一个包括SPEC、OOMM、PROT、VERI几个子系统组成的环境来支持上述过程。 相似文献