Cyber & formal methods publications

This report describes the monitoring, intrusion detection, and reporting infrastructure of the resulting system highlighting the design principles and lessons learned that are generally applicable to survivable information systems.

A new US law allows warrantless wiretapping whenever one end of the communication is believed to be outside national borders. This creates serious security risks: danger of exploitation of the…

We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract…

In this paper we investigate how to use the alerts from several audit sources to improve the accuracy of the intrusion detection system (IDS). Concentrating on web server attacks, we…

We present novel online index learning algorithms. When compared to other approaches, including one-versus-rest and top-down learning and classification using support vector machines, we find that indexing is highly advantageous…

This tutorial describes the use of PL to model signal transduction processes. It begins with a general discussion of Symbolic Systems Biology, followed by some background on rewriting logic and…

This paper discusses event-based semantics in the context of the emerging concept of Cyber Physical Systems and describes two related formal models concerning policy-based coordination and Interactive Agents.

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains.

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…

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…

We formally define delegation in predicate encryption systems, propose a new security definition for delegation, and give an efficient construction supporting conjunctive queries.

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.