Publications

This report summarizes our work on methods for developing high-assurance digital systems. We present an approach for understanding and evaluating trust issues in digital systems, and for us- ing computer-checked proofs as a means for realizing this approach. We describe the theoretical background for programming with proofs based on the Curry-Howard correspondence, connect- ing the field of logic and proof theory to programs. We then describe a series of case studies, intended to demonstrate how this approach might be adopted in practice. In particular, our stud- ies elucidate some of the challenges that arise with this style of certified programming, including induction principles, generic programming, termination requirements, and reasoning over infinite state spaces.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

The amount of publicly available source code on the Internet makes it attractive as a potential message carrier for steganographic applications. Unfortunately, it is often overlooked since embedding information in an undetectable way is challenging. We investigate term rewriting as a method for embedding messages into programs via transformations on source code. We elaborate on several possible transformation strategies and discuss how they might be applied in a steganographic setting. We continue with a discussion on (a) the implications and trade-offs of preserving semantic properties, (b) the relationship between messages and transformations, and (c) how to incorporate existing natural language processing techniques. The goal of this work is to elicit constructive feedback and present ideas that stimulate future work.