Cyber & formal methods publications
-
Non-Linear Rewrite Closure and Weak Normalization
In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and…
-
Coordinating Asynchronous and Open Distributed Systems Under Semiring-Based Timing Constraints
We focus on coordinating actors and roles through message manipulations based on event-based timing constraints. In addition, different types of timing constraints are generalized into a semiring-based constraint structure; and…
-
Challenges in Scalable Fault Tolerance
Efficient and effective means are needed that exploit structure inherent in one layer of architecture to provide key properties to enable reliable execution at other levels.
-
Higher-Order and Symbolic Computation: Editorial
Higher-Order and Symbolic Computation is an international journal that presents a broad-spectrum forum for discussion of results and ideas on programming with higher-order and symbolic facilities: first-class functions and continuations,…
-
Panel: Technical, Social and Legal Frameworks for Digital Forensics and Cyberinfrastructure Security
A systematic approach to digital forensic engineering acknowledges the close, intertwine relationship between digital forensics and information security.
-
A Safety-Case Approach for Certifying Adaptive Systems
In this paper, we argue that analysis tools based on recent advances in formal methods (SMT solvers, infinite bounded model checkers, and k-induction) can provide suitable modeling notations, effective analysis,…
-
Malware Characterization Through Alert Pattern Discovery
We present a novel alert correlation approach based on the factor analysis statistical technique for malware characterization. Our approach involves mechanically computing a set of abstract quantities, called factors, for expressing…
-
System Support for Forensic Inference
This paper argues for the development of a formal framework for constructing “digital artifacts” that can serve as proxies for physical evidence; a system so imbued would facilitate sound digital…
-
Unification and Narrowing in Maude 2.4
This paper introduces novel features of Maude 2.4 including support for unification and narrowing. Unification is supported in Core Maude, the core rewriting engine of Maude, with commands and metalevel…
-
Adaptive Security in Broadcast Encryption Systems (With Short Ciphertexts)
We present new techniques for achieving adaptive security in broadcast encryption systems. Previous work on fully collusion resistant broadcast encryption systems with very short ciphertexts was limited to considering only static security.
-
A Beginner’s Example of Proc Mixed for the Analysis of Letter Identification Using Reaction Time
-
An Attacker-Defender Game for Honeynets
We formalize the problem of defending honeynets from systematic mapping (a serious threat to their viability) as a simple two-person game.