Modern malware applies a rich arsenal of evasion techniques to render dynamic analysis ineffective. In turn, dynamic analysis tools take great pains to hide themselves from malware; typically this entails trying to be as faithful as possible to the behavior of a real run. We present a novel approach to malware analysis that turns this idea on its head, using an extreme abstraction of the operating system that intentionally strays from real behavior. The key insight is that the presence of malicious behavior is sufficient evidence of malicious intent, even if the path taken is not one that could occur during a real run of the sample. By exploring multiple paths in a system that only approximates the behavior of a real system, we can discover behavior that would often be hard to elicit otherwise. We aggregate features from multiple paths and use a funnel-like configuration of machine learning classifiers to achieve high accuracy without incurring too much of a performance penalty. We describe our system, TAMALES (The Abstract Malware Analysis LEarning System), in detail and present machine learning results using a 330K sample set showing an FPR (False Positive Rate) of 0.10% with a TPR (True Positive Rate) of 99.11%, demonstrating that extreme abstraction can be extraordinarily effective in providing data that allows a classifier to accurately detect malware.

We present a characterization that shows what it means for a formula to be a weak or strong version of another formula. We show that the weak version of a formula is not the same as Alpern and Schneider's safety component, but can be achieved by taking the closure in the Cantor topology over an augmented alphabet in which every formula is satisfiable. The resulting characterization allows us to show that the set of semantically weak formulas is exactly the set of nonpathological safety formulas. Furthermore, we use the characterization to show that the original versions of the ieee standard temporal logics psl and sva are broken, and we show that the source of the problem lies in the semantics of the sere intersection and fusion operators. Finally, we use the topological characterization to show the internal consistency of the alternative semantics adopted by the latest version of the psl standard.

We examine the problem of defining equivalence between two functions (pieces of code) that are intended to perform analogous tasks, but whose interfaces do not correspond in a straightforward way, even to the point of ambiguity. We formalize the notion of what equivalence means in such a case and show how to check it using constraints on a model checking problem. We show that the presence of constraints complicates the issue of predicate abstraction, and show that nevertheless we can use predicates no finer than those needed in the absence of constraints. Our solution is being used to verify the migration of tens of millions of lines of health insurance claims processing code from icd- 9 to icd-10, two versions of the International Statistical Classification of Diseases and Related Health Problems (icd), whose correspondence is complex and ambiguous in both directions. We present experimental results on 90,000 real life functions.

We study the relation between logical contradictions such as p ∧ ¬p and structural contradictions such as p ∩ (p.q). Intuitively, we expect the two to be treated similarly, but they are not by PSL, nor by SVA. We provide a solution that treats both kinds of contradictions in a consistent manner. The solution reveals that not all structural contradictions are created equal: we must distinguish between them in order to preserve important characteristics of the logic. A happy result of our solution is that it provides the semantics over the natural alphabet 2 P , as opposed to the current semantics of PSL/SVA that use an inflated alphabet including the cryptic letters ⊤ and . We show that the complexity of model checking PSL/SVA is not affected by our proposed semantics.

In this paper we consider the problem of exploiting infeasible clock gating functions. Analysis of industrial designs reveals a large margin of potential for power saving based on clock gating functions that initially appear to be useless due to timing violation or excessive power consumption. We propose two optimization techniques for resurrecting such functions that can be used as a generic post-processing phase in an automatic clock gating tool. The first provides timing-aware approximation and the second aims at generating large gating domains by clustering similar clock gating functions. Our experimental results show that the combination of these two techniques yields an additional power saving of up to 78% in industrial designs.

Power gating is a technique for low power design in which whole sections of the chip are powered off when they are not needed, and powered back on when they are. Functional correctness of power gating is usually checked as part of system-level verification, where the most widely used technique is simulation using pseudo-random stimuli. We propose instead to perform a sequential equivalence check between the power gated design and a version of itself in which power gating is disabled. We take a compositional approach that looks for partial equivalence of each unit under a suitable set of assumptions, guaranteed by the neighboring units. We make use of so-called circular reasoning rules to compose the partial equivalences proved on the individual units back into total equivalence on the whole chip.

The semantics of temporal logic is usually defined with respect to a word representing a computation path over a set of atomic propositions. A temporal logic formula does not control the behavior of the atomic propositions, it merely observes their behavior. Local variables are a twist on this approach, in which the user can declare variables local to the formula and control their behavior from within the formula itself. Local variables were introduced in 2002, and a formal semantics was given to them in the context of SVA, the assertion language of SystemVerilog, in 2004. That semantics suffers from several drawbacks. In particular, it breaks distributivity of the operators corresponding to intersection and union. In this paper we present a formal semantics for local variables that solves that problem and others, and compare it to the previous solution.

Policies can be understood as specifications; therefore they can be translated more or less easily into formal languages and then be verified by formal techniques such as model checking. In this paper, we focus on formal verification of real-life industrial policies of the IBM Tivoli System Automation for Multi-Platform (TSA). We use PSL to model the system and describe the desired behavior and the RuleBase PE model checker to verify it.

In this document we extend Proposal A’ for augmenting the formal semantics of PSL with local variables to all of PSL (issue 67). Proposal A’ provides semantics for PSL without truncated words, abort and clock operators. In this proposal we augment the entire formal semantics of PSL (including the above constructs) with local variables. In addition, we add semantics for procedural blocks (issue 66), for built-in functions that refer to the past (issue 117) and for clock alignment operators (issue 137). This document presents the semantics gradually. First it presents the semantics of the base logic, which is the set of FL formulas that (i) do not use the clock operator (ii) do not refer to the past (i.e., do not use past built-in functions) and (iii) do not use local variables or procedural blocks. Then it presents the semantics of the base logic extended with either the clock operator or references to the past or local variables and procedural blocks. Last it presents the overall semantics of linear formulas with no restrictions.

We present a hybrid method for software model checking that combines explicit-state and symbolic techniques. Our method traverses the control flow graph of the program explicitly, and encodes the data values in a CNF formula, which we solve using a SAT solver. In order to avoid traversing control flow paths that do not correspond to a valid execution of the program we introduce the idea of a representative of a control path. We present favorable experimental results, which show that our method scales well both with regards to the non-deterministic data and the number of threads.

PSL is a property specification language recently standardized as IEEE 1850 (TM)-2005 PSL. It includes as its temporal layer a linear temporal logic that enhances LTL with regular expressions and other useful features. PSL and its precursor, Sugar, have been used by the IBM Haifa Research Laboratory for formal verification of hardware since 1993, and for informal (dynamic, simulation runtime) verification of hardware since 1997. More recently both Sugar and PSL have been used for formal, dynamic, and runtime verification of software. In this paper I will introduce PSL and briefly touch on theoretical and practical issues in the use of PSL for dynamic and runtime verification.

In previous work [1] we argue that in order for temporal logic to be useful in incomplete verification methods such as simulation or bounded model checking, it is necessary to define semantics over truncated paths. A truncated path is a path which is finite, but not necessarily maximal. The semantics on truncated paths is based on three views: the weak view, the neutral view and the strong view. In [1] we have defined the semantics explicitly for each view. That is, the semantics of formulas is interpreted over a pair consisting of a word over 2 (where P is the set of atomic propositions) and a view which is either weak or neutral or strong. Here we suggest an alternative, more concise, approach for giving the semantics, which is achieved by interpreting the formulas over words from the alphabet 2 ∪ {>,⊥} where > and ⊥ are