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…
-
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.
-
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…
-
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,…
-
Fast Cryptographic Primitives and Circular-Secure Encryption Based on Hard Learning Problems
Here we demonstrate additional applications that enjoy strong security properties and a high level of efficiency.
-
Intrusion Monitoring in Process Control Systems
Our approach involves a multilayer security architecture for monitoring process control systems to achieve accurate and effective situational awareness.
-
Public-Key Cryptosystems from the Worst-Case Shortest Vector Problem
We construct public-key cryptosystems that are secure assuming theworst-case hardness of approximating the minimum distance on n-dimensional lattices to within small Poly(n) factors.
-
Certainty Closure: Reliable Constraint Reasoning with Incomplete or Erroneous Data
We present a unifying framework that extends the CP formalism in both model and solutions, to tackle ill-defined combinatorial problems with incomplete or erroneous data.
-
Invariant Checking for Programs with Procedure Calls
We explore the theoretical limits for doing automatic invariant checking and show that invariant checking is decidable for a large class of programs that includes some recursive programs.
-
New Techniques for Private Stream Searching
A system for private stream searching, introduced by Ostrovsky and Skeith, allows a client to provide an untrusted server with an encrypted search query.