Cyber & formal methods publications

Tracing the history of exposing and elucidating the wide variety of system problems and associated social implications of uses and misuses of computing technology.

This paper presents a constraint-based technique for discovering a rich class of inductive invariants (boolean combinations of polynomial inequalities of bounded degree) for verification of hybrid systems.

To reduce the risk of successful cryptanalysis, new keys must be established (rekeying). We have designed a rekeying scheme that provides both backward and forward secrecy.

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…

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…

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…

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…

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.

We present convergent rewrite systems over conditional values that can interact with macro expansion and evaluation and transform them into Boolean expressions.

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.