The well-known Principle of Least Privilege states that a program should run with the minimal authority that it requires to get the job done, and no more. However, application of the principle has been left to software developers, developers of installation procedures, and system administrators with few tools to assist them. How much privilege does a given program need? How do you know if you write a program that uses too much privilege or install a program with too little? Empirical privilege profiling provides a partial answer to this question by tracking a program's actual use of resources, which can be used as a guide during program development and installation, as well as for detecting intrusions and providing assurance for mobile code. In this paper, we introduce the concept of dealing with privilege as a measurable quantity, rather than in terms of a "rule of thumb."

This panel highlights a selection of the most interesting and provocative papers from the 2004 New Security Paradigms Workshop. This workshop was held September 2004 - the URL for more information is (http://www.nspw.org). The panel consists of authors of the selected papers, and the session is moderated by the workshop's general chairs. We present selected papers focusing on exciting major themes that emerged from the workshop. These are the papers that will provoke the most interesting discussion at ACSAC.

This panel highlights a selection of the most interesting and provocative papers from the 2003 New Security Paradigms Workshop. This workshop was held August 2003 - the URL for more information is . The panel consists of authors of the selected papers, and the session is moderated by the workshop’s general chairs. We present selected papers focusing on exciting major themes that emerged from the workshop. These are the papers that will provoke the most interesting discussion at ACSAC.

Reducing the risks introduced with large new systems requires rethinking the way we build systems. Today's computer systems are built according to traditional engineering models, which emphasize simplicity and efficiency but which introduce an unacceptable risk of misuse in large-scale systems. We need a new paradigm that results in "messy" systems that evolve through small incremental changes and localized failures.

Some recent advances in intrusion detection are based on detecting anomalies in program behavior, as characterized by the sequence of kernel calls the program makes. Specifically, traces of kernel calls are collected during a training period. The substrings of fixed length N (for some N) of those traces are called N-grams. The set of N-grams occurring during normal execution has been found to discriminate effectively between normal behavior of a program and the behavior of the program under attack. The N-gram characterization, while effective, requires the user to choose a suitable value for N. This paper presents an alternative characterization, as a finite state machine whose states represent predictive sequences of different lengths. An algorithm is presented to construct the finite state machine from training data, based on traditional string-processing data structures but employing some novel techniques.

THETA is a secure distributed operating system designed to run on a variety of hardware platforms. We are currently undertaking an effort to formally specify and implement a new THETA kernel to improve its security properties and to increase its portability. We used a number of "formal methods" tools in developing the specification and analyzing its implementation. The report presents an overview of the THETA kernel architecture, then discusses the methods and tools that we used to develop it. We include a critique of the tools and a discussion of the relative merits of using Ada and C to implement complex secure systems.>

Abstract We used literate programming on a team project to write a 33,000 line program for the Synthesizer Generator. The program, Penelope, was written using WEB, a tool designed for writing literate programs. Unlike other WEB programs, many of which have been written by WEB's developer or by individuals, Penelope was not intended to be published. We used WEB in the hope that both our team and its final product would benefit from the advantages often attributed to literate programming. The WEB source served as good internal documentation throughout development and maintenance, and it continues to document Penelope's design and implementation. Our experience also uncovered a number of problems with WEB.

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy.>

A major drawback to the use of attribute grammars in language-based editors has been that attributes can only depend on neighboring attributes in a program's syntax tree. This paper concerns new attribute-grammar-based methods that, for a suitable class of grammars, overcome this fundamental limitation. The techniques presented allow the updating algorithm to skip over arbitrarily large sections of the tree that more straightforward updating methods visit node by node. These techniques are then extended to deal with aggregate values, so that the attribute updating procedure need only follow dependencies due to a changed component of an aggregate value. Although our methods work only for a restricted class of attribute grammars, satisfying the necessary restrictions should not place an undue burden on the writer of the grammar.