Towards Behavioral Maude: Behavioral Membership Equational Logic

How can algebraic and coalgebraic specifications be integrated? How can behavioral equivalence be addressed in an algebraic specification language? The hidden-sorted approach, originating in work of Goguen and Meseguer in the early 80's, and further developed into the hidden-sorted logic approach by researchers at Oxford, UC San Diego, and Kanazawa offers some attractive answers, and has been implemented in both BOBJ and CafeOBJ. In this work we investigate both further extensions of hidden logic, and an extension of the Maude specification language called BMaude supporting this extended hidden-sorted semantics.Maude's underlying equational logic, membership equational logic, generalizes and increases the expressive power of many-sorted and order-sorted equational logics. We develop a hidden-sorted extension of membership equational logic, and give conditions under which theories have both an algebraic and a coalgebraic semantics, including final (co-)algebras. We also discuss the language design of BMaude, based on such an extended logic and using categorical notions in and across the different institutions involved. We also explain how Maude's reflective semantics provides a systematic method to extend Maude to BMaude within Maude, including module composition operations, evaluation, and automated proof methods.     

Recent Advances in Real-Time Maude

This paper gives an overview of recent advances in Real-Time Maude. Real-Time Maude extends the Maude rewriting logic tool to support formal specification and analysis of object-based real-time systems. It emphasizes ease and generality of specification and supports a spectrum of analysis methods, including symbolic simulation, unbounded and time-bounded reachability analysis, and LTL model checking. Real-Time Maude can be used to specify and analyze many systems that, due to their unbounded features, such as unbounded data structures or dynamic object and message creation, cannot be modeled by current timed/hybrid automaton-based tools. We illustrate this expressiveness and generality by summarizing two case studies: (i) an advanced scheduling algorithm with unbounded queues; and (ii) a state-of-the-art wireless sensor network algorithm. Finally, we give some (often easily checkable) conditions that ensure that Real-Time Maude's analysis methods are complete, also for dense time, for object-based real-time systems. In practice, our result implies that Real-Time Maude's time-bounded search and model checking of LTL time-bounded formulas are complete decision procedures for a large and useful class of non-Zeno real-time systems that fall outside the scope of systems that can be modeled in decidable fragments of hybrid automata, including the sensor network case study discussed in this paper.     

Maude: specification and programming in rewriting logic

Maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. Since rewriting logic contains equational logic, Maude also supports equational specification and programming in its sublanguage of functional modules and theories. The underlying equational logic chosen for Maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. Rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. Reflection is systematically exploited in Maude endowing the language with powerful metaprogramming capabilities, including both user-definable module operations and declarative strategies to guide the deduction process. This paper explains and illustrates with examples the main concepts of Maude's language design, including its underlying logic, functional, system and object-oriented modules, as well as parameterized modules, theories, and views. We also explain how Maude supports reflection, metaprogramming and internal strategies. The paper outlines the principles underlying the Maude system implementation, including its semicompilation techniques. We conclude with some remarks about applications, work on a formal environment for Maude, and a mobile language extension of Maude.     

非线性代数规范的直接实现技术

代数规范是支持软件规格说明和设计的一种有效的方法，代数规范的直接实现技术是该研究领域的一个主要分支，目前这方面的研究基本上局限于线性代数规范，本文介绍一个实现非线性代数规范的转换过程，从该过程可自然是导出针对不同程序设计语言的转换系统，我们已实现了一个基于Ｐａｓｃａｌ语言的转换系统。     

Detection of metamorphic computer viruses using algebraic specification

This paper describes a new approach towards the detection of metamorphic computer viruses through the algebraic specification of an assembly language. Metamorphic computer viruses are computer viruses that apply a variety of syntax-mutating, behaviour-preserving metamorphoses to their code in order to defend themselves against static analysis based detection methods. An overview of these metamorphoses is given. Then, in order to identify behaviourally equivalent instruction sequences, the syntax and semantics of a subset of the IA-32 assembly language instruction set is specified formally using OBJ – an algebraic specification formalism and theorem prover based on order-sorted equational logic. The concepts of equivalence and semi-equivalence are given formally, and a means of proving equivalence from semi-equivalence is given. The OBJ specification is shown to be useful for proving the equivalence or semi-equivalence of IA-32 instruction sequences by applying reductions – sequences of equational rewrites in OBJ. These proof methods are then applied to fragments of two different metamorphic computer viruses, Win95/Bistro and Win9x.Zmorph.A, in order to prove their (semi-)equivalence. Finally, the application of these methods to the detection of metamorphic computer viruses in general is discussed.     

Metamorphic worm that carries its own morphing engine

Metamorphic malware changes its internal structure across generations, but its functionality remains unchanged. Well-designed metamorphic malware will evade signature detection. Recent research has revealed techniques based on hidden Markov models (HMMs) for detecting many types of metamorphic malware, as well as techniques for evading such detection. A worm is a type of malware that actively spreads across a network to other host systems. In this project we design and implement a prototype metamorphic worm that carries its own morphing engine. This is challenging, since the morphing engine itself must be morphed across replications, which imposes restrictions on the structure of the worm. Our design employs previously developed techniques to evade detection. We provide test results to confirm that this worm effectively evades signature and HMM-based detection, and we consider possible detection strategies. This worm provides a concrete example that should prove useful for additional metamorphic detection research.     

Metamorphic malware identification using engine-specific patterns based on co-opcode graphs

A metamorphic virus is a type of malware that modifies its code using a morphing engine. Morphing engines are used to generate a large number of metamorphic malware variants by performing different obfuscation techniques. Since each metamorphic malware has its own unique structure, signature based anti-virus programs are ineffective to detect these metamorphic variants. Therefore, detection of these kind of viruses becomes an increasingly important task. Recently, many researchers have focused on extracting common patterns of metamorphic variants that can be used as micro-signatures to identify the metamorphic malware executables. With the similar motivation, in this work, we propose a novel metamorphic malware identification method, named HLES-MMI (Higher-level Engine Signature based Metamorphic Malware Identification). The proposed method firstly constructs a unique graph structure, called as co-opcode graph, for each metamorphic family, then extracts engine-specific opcode patterns from the graphs. Finally, it generates higher-level signature belonging to each family by representing the extracted opcode-patterns with a binary vector. Experimental results on four datasets produced by different morphing engines demonstrate the effectiveness and efficiency of the proposed method by comparing with several existing malware identification methods.     

恶意代码的变形技术研究

恶意代码常常使用一些隐形技术来躲避反病毒软件的检测。然而,采用加密和多态技术的恶意代码已经难以躲避基于特征码和代码仿真技术的检测,而变形技术却呈现出较强的反检测能力。通过对变形技术作深入的分析,详细介绍了变形引擎及其所采用的代码混淆技术,以及当前的变形恶意代码检测技术,并简要分析了变形技术在软件防护领域的应用。     

Simple substitution distance and metamorphic detection

To evade signature-based detection, metamorphic viruses transform their code before each new infection. Software similarity measures are a potentially useful means of detecting such malware. We can compare a given file to a known sample of metamorphic malware and compute their similarity—if they are sufficiently similar, we classify the file as malware of the same family. In this paper, we analyze an opcode-based software similarity measure inspired by simple substitution cipher cryptanalysis. We show that the technique provides a useful means of classifying metamorphic malware.     

Chi-squared distance and metamorphic virus detection

Metamorphic malware changes its internal structure with each generation, while maintaining its original behavior. Current commercial antivirus software generally scan for known malware signatures; therefore, they are not able to detect metamorphic malware that sufficiently morphs its internal structure. Machine learning methods such as hidden Markov models (HMM) have shown promise for detecting hacker-produced metamorphic malware. However, previous research has shown that it is possible to evade HMM-based detection by carefully morphing with content from benign files. In this paper, we combine HMM detection with a statistical technique based on the chi-squared test to build an improved detection method. We discuss our technique in detail and provide experimental evidence to support our claim of improved detection.     

基于重写逻辑的Web服务事务处理形式化描述

Web服务的事务处理研究越来越活跃,对于Web服务中的长、短事务进行形式化描述与验证是很重要的,但目前还没有成熟的方法．该文提出了一种基于重写逻辑的Web服务事务处理形式化描述方法,采用重写逻辑工具Maude,对于描述Web事务的细胞膜演算,给出一个事务处理的通用框架,采用重写逻辑中的规则描述事务的具体活动,并且引入事务补偿机制刻画长事务的运行;并应用该模型形式化描述文中的Web事务经典例子,得到一个可执行的重写逻辑模型,便于以后采用Maude线性时序逻辑分析器进行形式化分析．     

Recognizing malicious software behaviors with tree automata inference

We explore how formal methods and tools of the verification trade could be used for malware detection and analysis. In particular, we propose a new approach to learning and generalizing from observed malware behaviors based on tree automata inference. Our approach infers k-testable tree automata from system call dataflow dependency graphs. We show how inferred automata can be used for malware recognition and classification.     

A Tutorial on Specifying Data Structures in Maude

This tutorial describes the equational specification of a series of typical data structures in Maude. We start with the well-known stacks, queues, and lists, to continue with binary and search trees. Not only are the simple versions considered but also advanced ones such as AVL and 2-3-4 trees. The operator attributes available in Maude allow the specification of data based on constructors that satisfy some equational properties, like concatenation of lists which is associative and has the empty list as identity, as opposed to the free constructors available in other functional programming languages. Moreover, the expressive version of equational logic in which Maude is based, namely membership equational logic, allows the faithful specification of types whose data are defined not only by means of constructors, but also by the satisfaction of additional properties, like sorted lists or search trees. In the second part of the paper we describe the use of an inductive theorem prover, the ITP, which itself is developed and integrated in Maude by means of the powerful metalevel and metalanguage features offered by the latter, to prove properties of the data structures. This is work in progress because the ITP is still under development and, as soon as the data gets a bit complex, the proof of their properties gets even more complex.     

A formal semantics for an active functional DBPL

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.     

Slicing from formal semantics: Chisel—a tool for generic program slicing

We describe Chisel, a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics \(\mathcal {S}\). \(\mathcal {S}\) is assumed to be a rewriting logic specification, given in Maude, while the program is a ground term of this specification. Chisel takes \(\mathcal {S}\) and synthesizes language constructs, i.e., instructions, that produce features relevant for slicing, e.g., data dependency. We implement syntheses adjusted to each feature as model checking properties over an abstract representation of \(\mathcal {S}\). The syntheses results are used by a traditional interprocedural slicing algorithm that we parameterize by the synthesized language features. We present the tool on two language paradigms: high-level, imperative and low-level, assembly languages. Computing program slices for these languages allows for extracting traceability properties in standard compilation chains and makes our tool fitting for the validation of embedded system designs. Chisel’s slicing benchmark evaluation is based on benchmarks used in avionics.     

Structural entropy and metamorphic malware

Metamorphic malware is capable of changing its internal structure without altering its functionality. A common signature is nonexistent in highly metamorphic malware and, consequently, such malware can remain undetected under standard signature scanning. In this paper, we apply previous work on structural entropy to the metamorphic detection problem. This technique relies on an analysis of variations in the complexity of data within a file. The process consists of two stages, namely, file segmentation and sequence comparison. In the segmentation stage, we use entropy measurements and wavelet analysis to segment files. The second stage measures the similarity of file pairs by computing an edit distance between the sequences of segments obtained in the first stage. We apply this similarity measure to the metamorphic detection problem and show that we obtain strong results in certain challenging cases.     

EPMDroid: Efficient and privacy-preserving malware detection based on SGX through data fusion

Android has stood at a predominant position in mobile operating systems for many years. However, its popularity and openness make it a desirable target of malicious attackers. There is an increasing need for mobile malware detection. Existing analysis methods fall into two categories, i.e., static analysis and dynamic analysis. The dynamic analysis is more effective and timely than the static one, but it incurs a high computational overhead, thus cannot be deployed in resource-constrained mobile devices. Existing studies solve this issue by outsourcing malware detection to the cloud. However, the privacy of mobile app runtime data uploaded to the cloud is not well preserved during both detection model training and malware detection. Numerous efforts have been made to preserve privacy with cryptography, which suffers from high computational overhead and low flexibility. To address these issues, in this paper, we propose an Intel SGX-empowered mobile malware detection scheme called EPMDroid. We also design a probabilistic data structure based on cuckoo filters, named CuckooTable, to effectively fuse features for detection and achieve high space efficiency. We conduct both theoretical analysis and real-world data based tests on EPMDroid performance. Experimental results show that EPMDroid can speed up malware detection by up to 43.8 times and save memory space by up to 3.7 times with the same accuracy, as compared to a baseline method.     

BASIS: A behavioral approach to the specification of information systems

This paper is an overview of BASIS (Behavioral Approach to the Specification of Information Systems), a multi-step formal method used for information systems design and development. The steps include information analysis, semantic specification, verification of the specification, concrete implementation, and verification of the implementation. In this way, BASIS can be used to provide a formal basis for information systems development. We provide an example showing how BASIS can be used in conjunction with implementation in the programming language PLAIN.     

Using Maude to write and execute ODP information viewpoint specifications

The aim of the open distributed processing (ODP) information viewpoint is to describe the semantics of the information and of the information processing in a system, from a global point of view, without having to worry about other considerations, such as how the information will be finally distributed or implemented or the technology used to achieve such implementation. Although several notations have been proposed to model this ODP viewpoint, they are not expressive enough to faithfully represent all the information concepts, or they tend to suffer from a lack of (formal) support, or both. In this paper, we explore the use of Maude as a formal notation for writing ODP information specifications. Maude is an executable rewriting logic language especially well suited for the specification of object-oriented open and distributed systems. We show how Maude offers a simple, natural, and accurate way of modeling the ODP information viewpoint concepts, allows the execution of the specifications produced, and offers good tool support for reasoning about them.