Cyber & formal methods publications
-
A Brief Overview of PVS
Abstract PVS is now 15 years old, and has been extensively used in research, industry, and teaching. The system is very expressive, with unique features such as predicate subtypes, recursive…
-
A Framework for Efficient and Composable Oblivious Transfer
We propose a simple and general framework for constructing oblivious transfer (OT) protocols that are efficient, universally composable, and generally realizable under any one of a variety of standard number-theoretic…
-
Delegating Capabilities in Predicate Encryption Systems
We formally define delegation in predicate encryption systems, propose a new security definition for delegation, and give an efficient construction supporting conjunctive queries.
-
Eureka: a Framework for Enabling Static Malware Analysis
We introduce Eureka, a framework for enabling static analysis on Internet malware binaries. Eureka incorporates a novel binary unpacking strategy based on statistical bigram analysis and coarse-grained execution tracing.
-
Sampling Stable Properties of Massive Track Datasets
In this paper, we explore ways in which stable properties of sensor observations can be extracted and visualized using a statistical sampling of features from a very large track dataset,…
-
Conflict Negotiation Among Personal Calendar Agents
We will demonstrate distributed conflict resolution in the context of personalized meeting scheduling. The demonstration will show how distributed constraint optimization can be used to facilitate interaction between cognitive agents…
-
Compositionality for Tightly Coupled Systems: a New Application of the Propositions-As-Types Interpretation
Although compositional techniques are being successfully employed in practice, the use of such techniques is often rather informal and intuitive, and typically a justification for correct behaviour of the composed…
-
Event Recognition in Airborne Motion Imagery
A system is described that detects high-level events of interest in airborne motion imagery.
-
Generation of fast interpreters for Huffman compressed bytecode
Our approach uses canonical Huffman codes to generate compact opcodes with custom-sized operand fields and with a virtual machine that directly executes this compact code. In effect, this automatically creates…
-
Report on the 2004 DARPA Workshop on Self-Aware Computer Systems
This report captures some of the salient points discussed during the DARPA workshop on Self-Aware Computer Systems held on April 27-28, 2004 in Washington D.C.
-
Rewrite Systems for Symbolic Evaluation of C-like Preprocessing
We present convergent rewrite systems over conditional values that can interact with macro expansion and evaluation and transform them into Boolean expressions.
-
RegReg: a Lightweight Generator of Robust Parsers for Irregular Languages
We present a lightweight tool, called RegReg, based on a hierarchy of lexers described by tagged regular expressions. By using tags, the automatically generated parse tree can be easily manipulated.