Cyber & formal methods publications

We are developing a completely decentralized system with each computer maintaining the authoritative repository of the provenance gathered on it.

The principle underlying the card trick can be proved in a number of ways. We present the argument as a series of transformations that demystify the trick and describe its…

In this paper, we discuss the evolution of user space file systems with an emphasis on FUSE, and measure its performance using a variety of test cases.

We describe Mendel, a protocol with a three-pronged strategy that combines eager signature verification, lazy trust establishment, and cryptographic ordering witnesses to yield fast lineage verification in distributed multi-domain environments.

We discuss a range of issues at the intersection of rewriting and inference. How can other inference procedures be combined with rewriting? Can rewriting be used to describe inference procedures?

In this paper, we examine what real vendors do to ensure that their products are reasonably secure. Our conclusion is that software vendors put significant energy into software security, but…

This paper reflects on many risks in the development and use of computer-related systems. It considers past and future alternatives, suggests some remedial approaches, and offers a few broad conclusions.

We describe a complementary approach that uses Web Ontology Language (OWL) and Semantic Web Rule Language (SWRL) to capture information about the roles and capabilities required to complete a task,…

This paper presents a graphical user interface (GUI) for the Maude-NPA, a crypto protocol analysis tool that takes into account algebraic properties of cryptosystems not supported by other tools, such…

We review this idea and show how it provides a bridge between correctness, which is the goal of software verification (and especially formal verification), and the probabilistic properties such as…

We propose an ambitious and long-term research program toward the construction of error-free software systems.

We introduce some of the basic deduction techniques used in software and hardware verification and outline the theoretical and engineering issues in building deductive verification tools.