In this talk we present the latest developments on the Maude environment for CafeOBJ. This environment allows CafeOBJ specifications to be loaded into the Full Maude database, hence providing a simple way to use Maude tools in CafeOBJ specification. This is specially interesting when using Proof Scores including search predicates, since Maude can traverse the search space in a very efficient way and provide results that in some cases are beyond CafeOBJ performance.
The effectiveness of the generic proof scores is demonstrated by applying them to two simple but non-trivial examples QLOCK and ABP.
Developing correct low-level concurrent code is well-known to be especially difficult under a weak memory model, where code behavior can be surprising. Building reliable concurrent software using C/C++ low-level atomic operations will likely require tools that help developers discover unexpected program behaviors.
In this paper we present CDSChecker, a tool for exhaustively exploring the behaviors of concurrent code under the C/C++ memory model. We develop several novel techniques for modeling the relaxed behaviors allowed by the memory model and for minimizing the number of execution behaviors that CDSChecker must explore. We have used CDSChecker to exhaustively unit test several concurrent data structure implementations on specific inputs and have discovered errors in both a recently published C11 implementation of a work-stealing queue and a single producer, single consumer queue implementation.
In this talk, we will introduce a novel counterexample-guided approach to designing intended dynamic updates by identifying safe update points and defining correct state transformation function. In our approach, we formalize dynamic updates as state machines, and verify their correctness by model checking a set of desired properties which should be satisfied by the system after being updated. Guided by the counterexamples that are found by model checking, we can finally identify a set of update points and refine a state transformation function until all the properties are successfully verified.
The first half of the talk overviews typical malware techniques, consisting of 3 steps: intrusion, infection, and concealment. We focus on malware for Windows on x86 (32 bits). Intrusion correspond to the protection of Win 95 / XP / 7. After short summary of infection, we mention recent polymorphic techniques for concealment, such as mutation engine. The latter half introduces our current collaboration (between HCMUT and JAIST) on binary analysis, which consists of two steps: pushdown model generation and pushdown model checking. Different from high-level programming languages, it is not easy to generate a model for binary codes. For instance, (1) disassembly is decided dynamically, (2) jump destination addresses can be values on registers or memory (indirect jumps), (3) binary code loaded on memory can be dynamically modified (self-modification). We tackle this problem with on-the-fly model generation using concolic testing on a binary emulater, which are implemented as BE-PUM (Binary Emulator for PUshdown Model generation). We report our current experimantal results of pushdown model generation (including 1700 malwares from VX Heaven), and our ongoing investigation on its weighted pushdown model checking.
As an example of the development, we present a specification of Dijkstra's binary semaphore, a protocol to guarantee exclusive access to a resource. For this protocol we will give three different properties, one being the mutual exclusion (or safety) property, and two more regarding different forms of liveness, which we call progress property and entrance property. These three properties are verified in a computational (by term rewriting) way uniformly based on the new development.
Besides being a case study of modeling meta-properties in CafeOBJ, we provide an initial characterization of strength of various properties. Furthermore, this method can serve as a blue-print for other specifications, in particular those based on Abstract State Systems.
Bio : Bor-Yuh Evan Chang is an Assistant Professor of Computer Science at the University of Colorado Boulder. He is interested in tools and techniques for building, understanding, and ensuring reliable computational systems. His techniques target using novel ways of interacting with the programmer to design more precise and practical program analyses. He is a recipient of an NSF CAREER award. He received his M.S. and Ph.D. from the University of California Berkeley and his B.S. from Carnegie Mellon University.
The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a top most sort State, and the transitions are defined with conditional rewrite rules over the quotient set. A property to be verified is either (1) an invariant (i.e. a state predicate that is valid for all reachable states) or (2) a (p leads-to q) property for two state predicates p and q. Where (p leads-to q) means that from any reachable state s with (p(s) = true) the system will get into a state t with (q(t) = true) no matter what transition sequence is taken.
Verification is achieved by developing proof scores in CafeOBJ. Sufficient verification conditions are formalized for verifying invariants and (p leads-to q) properties. For each verification condition, a proof score is constructed to (1) generate a finite set of state patterns that covers all possible infinite states and (2) check validity of the verification condition for all the covering state patterns by reductions.
The method achieves significant automation of proof score developments.
input: A nondeterministic Turing machine M and a natural number n in unary. parameter: |M|, i.e., the size of M question: does M accept the empty input in at most n steps?Our recent work (2010-11) reveals that it is even equivalent to an open problem in proof complexity, i.e., whether there is a polynomial optimal proof system for the set TAUT of tautologies of propositional logic. In this talk, I will discuss all these equivalences and their extensions to some other complexity classes beside PTIME. It turns out that Levin's optimal inverters (1973) play a central role in the proofs. This is joint work with Joerg Flum.