Cyber & formal methods publications
-
Building Theorem Provers
Abstract This talk discusses some of the challenges of building a usable theorem prover. These include the chasm between theory and code, conflicting requirements, feature interaction, and competitive performance. The…
-
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.
-
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.
-
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).