We present a trust management kernel that clearly separates authorization and structured distributed naming. Given an access request and supporting credentials, the kernel determines whether the request is authorized. We prove soundness and completeness of the authorization system without names and prove that naming is orthogonal to authorization in a precise sense. The orthogonality theorem gives us simple soundness and completeness proofs for the entire kernel. The kernel is formally verified in PVS, allowing for the automatic generation of a verified implementation of a reference monitor. By separating naming and authorization primitives, we arrive at a compositional model and avoid concepts such as “speaks-for” that have led to anomalies in logical characterizations of other trust management systems.

We address the problem of establishing a group key amongst a dynamic group of users over an unreliable, or lossy, network. We term our key distribution mechanisms self-healing because users are capable of recovering lost group keys on their own, without requesting additional transmissions from the group manager thus cutting back on network traffic, decreasing the load on the group manager and reducing the risk of user exposure through traffic analysis. A user must be a member both before and after the session in which a particular key is sent in order to be able to recover the key through self-healing. Binding the ability to recover keys to membership status enables the group manager to use short broadcasts to establish group keys, independent of the group size. In addition, the self-healing approach to key distribution is stateless, meaning that a group member who has been off-line for some time is able to recover new session keys immediately after coming back on-line.

We present a new solution to the problem of determining the path a packet traversed over the Internet (called the traceback problem) during a denial-of-service attack. This article reframes the traceback problem as a polynomial reconstruction problem and uses algebraic techniques from coding theory and learning theory to provide robust methods of transmission and reconstruction.

We use a state-transition approach to analyze and compare the core access control mechanisms that are characteristic of a variety of trust management, access control list, and capability-based systems. The framework, which characterizes the set of rights a subject has over an object after any sequence of actions, is based on abstract system states, state transitions, and logical deduction of access control judgments. We present abstract models representing the access control portion of trust management, access control lists, and two versions of capabilities, proving various correspondence and simulation relations between these models. The main results include an equivalence between access control lists (ACLs) and capabilities viewed as rows of the Lampson access matrix and the (proper) subsumption of a form of ACLs by an "unforgeable reference" form of capabilities. The access control mechanism at the heart of distributed trust management systems is formally shown to provide a tractable compromise between unrestricted capability passing from the capability models and easy revocation provided by access control lists. The underlying simulations show how trust management compares with more established access control mechanisms, independent of features such as local name spaces and certificate authorization hierarchies.

One of the primary challenges in intrusion detection is modelling typical application behavior so that we can recognize attacks by their atypical effects without raising too many false alarms. We show how static analysis may be used to automatically derive a model of application behavior. The result is a host-based intrusion detection system with three advantages: a high degree of automation, protection against a broad class of attacks based on corrupted code, and the elimination of false alarms. We report on our experience with a prototype implementation of this technique.

We describe the design and implementation of a security infrastructure for a distributed Java application. This work is inspired by SDSI/SPKI, but has a few twists of its own. We define a logic for access control, such that access is granted iff a proof that it should be granted is derivable in the logic. Our logic supports linked local name spaces, privilege delegation across administrative domains, and attribute certificates. We use SSL to establish secure channels through which principals can "speak", and have implemented our access control system in Java. While we implemented our infrastructure for the Placeless Documents System, our design is applicable to other applications as well. We discuss general issues related to building secure, distributed Java applications that we discovered.

Dynamic linking is a requirement for portable executable content. Executable content cannot know, ahead of time, where it is going to be executed, nor know the proper operating system interface. This imposes a requirement for dynamic linking. At the same time, we would like languages supporting executable content to be statically typable, for increased efficiency and security. Static typing and dynamic linking interact in a security-relevant way. This interaction is the subject of this paper. One solution is modeled in PVS, and formally proven to be safe.

Mobile code technologies such as Java, JavaScript, and ActiveX generally limit all programs to a single security policy. However, software-based protection can allow for more flexible security models, with potentially significant performance improvements over traditional hardware-based solutions. We describe and analyze three implementation strategies for interposing flexible security policies in software-based security systems. Implementations exist for all three strategies: several vendors have adapted capabilities to Java, Netscape Communicator extended Java's stack introspection, and we built a typehiding system as an add-on to Microsoft Internet Explorer. 1 Introduction The growth of the World Wide Web has enabled the Internet to reach new levels of popularity and ease of use. We are now seeing the arrival of HTML-enabled mail and news-reading tools, heralding the complete acceptance of Web documents as a medium of exchange. As Web applications have blossomed, developers have bee...

This paper introduces a panel discussion on establishing assurance evidence that mobile code applications perform as expected by the user, without the side effects that have been demonstrated as possible in constructed examples of malicious or "rogue" applets. The paper's principal authors, Schaefer and Pinsky, have been engaged in cooperative research with the JavaSoft community to gain understanding of the complexities of assurance for mobile code applications. The paper discusses part of this on-going research. The panel adds the voices and experience of a continuing researcher, Dean, and of active practitioners from the principal vendors of mobile-code-enabled (and enabling) products. The panel actively debates the issues of providing compelling assurance evidence relating to the control of such code.

The introduction of Java applets has taken the World Wide Web by storm. Information servers can customize the presentation of their content with server-supplied code which executes inside the Web browser. We examine the Java language and both the HotJava and Netscape browsers which support it, and find a significant number of flaws which compromise their security. These flaws arise for several reasons, including implementation errors, unintended interactions between browser features, differences between the Java language and bytecode semantics, and weaknesses in the design of the language and the bytecode format. On a deeper level, these flaws arise because of weaknesses in the design methodology used in creating Java and the browsers. In addition to the flaws, we discuss the underlying tension between the openness desired by Web application writers and the security needs of their users, and we suggest how both might be accommodated.