Abstract: This paper reduces the satisfiability of noninterference to the solution of a finite set of equations. We use the structure of labelled transition systems, which are the basis for state machines and process algebras, to explicitly model the relationship between states, actions, and outputs. The output constraint equations are developed by constructing a predicate for nondeterministic systems and expressing noninterference as an invariance property of the predicate. The finiteness of the equations comes from a closure property of the predicate and the use of finite state machines.

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 paper gives necessary and sufficient conditions for a system to satisfy intransitive non-interference. Security is defined in terms of allowable flows of information among action domains as represented by an interferes relation /spl sim/>. We examine properties of special sets called basis elements generated from the relation /spl sim/> and introduce the notion of absorbing covers which is associated with the standard unwinding theorems for non-interference. Our approach separates the equivalence relation arguments from the non-interference properties, and as a by product, we develop a decision procedure for non-interference. An upper bound on the number of iterations needed for termination of the procedure is provided.>

This paper introduces necessary and sufficient conditions for solving the Haigh-Young view-identical problem. A decision procedure, based on properties of the state transition matrix and the function relating states to outputs, is used to establish the equivalence between non-interference and the existence of Haigh-Young view-identical relations on the set of states.>