, the risk it creates, and why the algorithm succeeds under well-known constraints.

Conditions are given under which a one-way function can be used safely in a programming language. The security proof involves showing that secrets cannot be leaked easily by any program meeting the conditions unless breaking the one-way function is easy. The result is applied to a password system where passwords are stored in a public file as images under a one-way function.

Systems that authenticate a user based on a shared secret (such as a password or PIN) normally allow anyone to query whether the secret is a given value. For example, an ATM machine allows one to ask whether a string is the secret PIN of a (lost or stolen) ATM card. Yet such queries are prohibited in any model whose programs satisfy an information-flow property like Noninterference. But there is complexity-based justification for allowing these queries. A type system is given that provides the access control needed to prove that no well-typed program can leak secrets in polynomial time, or even leak them with nonnegligible probability if secrets are of sufficient length and randomly chosen. However, there are well-typed deterministic programs in a synchronous concurrent model capable of leaking secrets in linear time.

After looking at the security literature, you will find secrecy is formalized in different ways, depending on the application. Applications have threat models that influence our choice of secrecy properties. A property may be reasonable in one context and completely unsatisfactory in another if other threats exist. The primary goal of this paper is to foster discussion on what sorts of secrecy properties are appropriate for different applications and to investigate what they have in common. We also want to explore what is meant by secrecy in different contexts. Perhaps there is enough overlap among our threat models that we can begin to identify some key secrecy properties for wider application. Currently, secrecy is treated in rather ad hoc ways. With some agreement among calculi for expressing protocols and systems, we might even be able to use one another's proof techniques for proving secrecy.

In previous work (Smith and Volpano, Proceedings 25th Symposium on Principles of Programming Languages, San Diego, CA, 1998, pp. 355–364), we give a type system that guarantees that well-typed multi-threaded programs are possibilistically noninterfer

The authors previously give a type system that guarantees that well-typed multi-threaded programs are possibilistically noninterfering. If thread scheduling is probabilistic, however, then well-typed programs may have probabilistic timing channels. They describe how they can be eliminated without making the type system more restrictive. They show that well-typed concurrent programs are probabilistically noninterfering if every total command with a high guard executes atomically. The proof uses the concept of a probabilistic state of a computation, following the work of Kozen (1981).

Previously, we developed a type system to ensure secure information flow in a sequential, imperative programming language [VSI96]. Program variables are classified as either high or low security; intuitively, we wish to prevent information from flowing from high variables to low variables. Here, we extend the analysis to deal with a multithreaded language. We show that the previous type system is insufficient to ensure a desirable security property called noninterference. Noninterference basically means that the final values of low variables are independent of the initial values of high variables. By modifying the sequential type system, we are able to guarantee noninterference for concurrent programs. Crucial to this result, however, is the use of purely nondeterministic thread scheduling. Since implementing such scheduling is problematic, we also show how a more restrictive type system can guarantee noninterference, given a more deterministic (and easily implementable) scheduling policy, such as round-robin time slicing. Finally, we consider the consequences of adding a clock to the language.

Advanced polymorphic type systems have come to play an important role in the world of functional programming. But, so far, these type systems have had little impact upon widely used imperative programming languages like C and C++. We show that ML-style polymorphism can be integrated smoothly into a dialect of C, which we call Polymorphic C. It has the same pointer operations as C, including the address-of operator &, the dereferencing operator ∗, and pointer arithmetic. We give a natural semantics for Polymorphic C, and prove a type soundness theorem that gives a rigorous and useful characterization of what can go wrong when a well-typed Polymorphic C program is executed. For example, a well-typed Polymorphic C program may fail to terminate, or it may abort due to a dangling pointer error. Proving such a type soundness theorem requires a notion of an attempted program execution; we show that a natural semantics gives rise quite naturally to a transition semantics, which we call a natural transition semantics, that models program execution in terms of transformations of partial derivation trees. This technique should be generally useful in proving type soundness theorems for languages defined using natural semantics.

A type system is given that eliminates two kinds of covert flows in an imperative programming language. The first kind arises from nontermination and the other from partial operations that can raise exceptions. The key idea is to limit the source of nontermination in the language to constructs with minimum typings, and to evaluate partial operations within expressions of try commands which also have minimum typings. A mutual progress theorem is proved that basically states that no two executions of a well-typed program can be distinguished on the basis of nontermination versus abnormal termination due to a partial operation. The proof uses a new style of programming language semantics which we call a natural transition semantics. 1. Introduction In [9], we gave a type system for secure information flow in a core imperative language. The type system is composed of a set of types and typing rules for deducing the types of expressions and commands. Types correspond to partially-ordered s...

Ensuring secure information flow within programs in the context of multiple sensitivity levels has been widely studied. Especially noteworthy is Denning's work in secure flow analysis and the lattice model [6,7]. Until now, however, the soundness of

In this article we consider the polymorphic type checking of an imperative language. Our language contains variables , first-class references (pointers), and first-class functions. Variables, as in traditional imperative languages, are implicitly dereferenced, and their addresses ( L -values) are not first-class values. Variables are easier to type check than references and, in many cases, lead to more general polymorphic types. We present a polymorphic type system for our language and prove that it is sound. Programs that use variables sometimes require weak types, as in Tofte's type system for Standard ML, but such weak types arise far less frequently with variables than with references

No abstract available.