Cyber & formal methods publications
-
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.
-
What Were You Thinking? Filling in Missing Dataflow Through Inference in Learning from Demonstration
This paper addresses the problem of learning from demonstrations involving unobservable (e.g., mental) actions. We explore the use of knowledge base inference to complete missing dataflow and investigate the approach…
-
Combining Equational Reasoning
Given a theory 𝕋T, a set of equations E, and a single equation e, the uniform word problem (UWP) is to determine if 𝐸⇒𝑒E⇒e in the theory 𝕋T.
-
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…
-
Planning and Learning Algorithms for Routing in Disruption-Tolerant Networks
We give an overview of algorithms that we have been developing in the DARPA disruption-tolerant networking program, which aims at improving communication in networks with intermittent and episodic connectivity.
-
Information Assurance Aspects of Rapid Software Reprogramming
This paper describes RSR in the context of a general vulnerability management cycle (VMC), familiarizes the reader with the applicable information assurance (IA) properties, and discusses how to use existing…
-
On the Impossibility of Basing Identity Based Encryption on Trapdoor Permutations
We show that there is no black-box construction of IBE from Trapdoor Permutations (TDP) or even from Chosen Ciphertext Secure Public Key Encryption (CCA-PKE).