Analysis of Scenario-based Requirements

 Rajeev Alur
University of Pennsylvania

Monday, October 21, 2002,
4:30PM     DRL 4C8

Scenario-based specifications such as message sequence charts offer an intuitive and visual way of describing design requirements. Such specifications focus on message exchanges among communicating entities in distributed software systems, and form an integral part of modern software design environments such as UML. Requirements expressed using MSCs have been given formal semantics, and hence, can be subjected to analysis to reveal inconsistencies. This talk surveys algorithms for a variety of such analyses including detecting race conditions, inferring implied scenarios, and model checking with respect to temporal logic requirements.

Categories of sets and classes

  Steve Awodey
Carnegie Mellon University

Monday, October 14, 2002,
4:45PM     Moore GRW 554

This talk reports on recent work in what has been called "Mac Lane set theory", a categorical set theory with a global membership relation among the objects. In contrast to elementary topos theory, such categories of sets model elementary set theory directly. We use the methods developed by Joyal and Moerdijk, employing an axiomatic notion of a system of small maps in a category of classes, which serve to limit comprehension in a new and flexible way. We show that *every* elementary topos arises as such a category of sets, and that (a certain) elementary set theory is deductively complete with respect to such topos models. An further new result in this connection is that the axiom scheme of full Replacement is conservative over bounded intuitionistic Zermelo set theory.

Beyond Church canons and Turing calculators:
Analyzing Computability without Theses

 Wilfried Sieg
Carnegie Mellon University

Monday, October 7, 2002,
4:30PM     Moore GRW 554

To investigate computability is to analyze symbolic processes that can, in principle, be carried out by calculators.
This is a philosophical lesson we owe to Turing.
Drawing on and recasting work of Alan Turing and Robin Gandy, I formulate finiteness and locality conditions for two types of calculators, human computing agents and mechanical computing devices; the distinctive feature of the latter is that they operate in parallel.

Church's and Turing's Theses assert, dogmatically, that an informal notion of computability (or effective calculability) is captured by a particular precise mathematical concept. I will present a conceptual analysis of computations, which dispenses with theses. The analysis leads instead to axioms for discrete dynamical systems (representing human and machine computations) and allows the reduction of models of these axioms to Turing machines.

Compositionality, System I, and Extensions for Sums

 Geoff Washburn
University of Pennsylvania

Monday, September 30, 2002,
4:30PM     Moore GRW 554

In this talk, we will introduce the concept of a compositional analysis and System I, an intersection type system, that provides such an analysis. Compositional analyses allow for, among other things, efficient incremental analysis and separate compilation. Compositionality in System I is made possible by introducing the notion of expansions and expansion variables. We will conclude with a discussion of work in progress on different proposals for extending System I with with sum types.

Termination of processes

 Davide Sangiorgi
INRIA-Sophia Antipolis, France
and the University of Bologna

Monday, September 23, 2002,
4:30PM     Moore GRW 554

A process terminates if it does not have an infinite sequence of reductions P -> P_1 -> P_2 ...

Termination is a useful property in concurrency. For instance, termination may be useful to show that when a given service is interrogated, it will eventually produce an answer. Similarly, a terminating applet, when loaded on a machine, will not run for ever on the machine, possibly absorbing all computing resources (a `denial of service' attack).

We ensure termination of a non-trivial subset of the pi-calculus by a combination of conditions based on types and on the syntax.

The proof of termination is in two parts. The first uses the technique of logical relation -- a well-know technique of lambda-calculi -- on a small set of `functional' processes. The second part of the proof uses techniques of process calculi, in particular techniques of behavioural preorders.

Abstraction-based Model Checking using Modal Transition Systems

 Radha Jagadeesan
Loyola University, Chicago

Wednesday, June 12, 2002,
4:00PM     Moore GRW 554

Abstraction based methods extend the applicability of model checking to programs written in general-purpose programming languages by extracting abstract (finite state) models from the source program. Such methods are generally unsound since abstraction usually introduces unrealistic behaviors.

This talk develops methods to perform automatic abstraction in such a way that it yields verification results whose soundness can be guaranteed. Our framework is based on modal transition systems (MTSs) to allow the sound transfer of properties and counter-examples (for mu-calculus properties) from the abstract program to the concrete program. MTSs arise naturally in three value program analysis and have robust semantic foundations based on a mixed powerdomain of states.

We describe algorithms to automatically generate an abstract MTS by adapting existing predicate and cartesian abstraction techniques, and algorithms for model checking abstract MTSs. These algorithms and can be implemented in combination with existing abstraction techniques without incurring significant computational overhead. The accuracy of verification results is improved by the use of Generalized model checking, a technique to improve the precision of reasoning about partial state spaces of concurrent reactive systems.

The talk is based on joint work with Godefroid, Huth and Schmidt.

Bijective Proofs in Combinatorics by Two-Directional Rewriting Techniques

  Max Kanovich
University of Pennsylvania

Monday, April 22, 2002,
4:31PM     DRL 4C8

The novelty of our approach to the combinatorics is in the use of rewriting techniques for the purpose of establishing explicit bijections between combinatorial objects of two different types.

One basic activity in combinatorics is to establish combinatorial identities by so-called `bijective proofs,' which consist in constructing explicit bijections between two types of the combinatorial objects under consideration.

We show how such bijective proofs can be established, and how the bijections are computed by means of multiset rewriting, for a variety of combinatorial problems involving partitions.

In particular, we fully characterizes all equinumerous partition ideals with `disjointly supported' complements. As a corollary, a new proof, the 'bijective' one, is given for all equinumerous classes of the partition ideals of order 1 from the classical book ``The Theory of Partitions'' by G.Andrews.

Establishing the required bijections involves novel two-directional reductions in the sense that forward and backward application of rewrite rules head for two different normal forms (representing the two combinatorial types).

It is well-known that non-overlapping multiset rules are confluent. As for termination, it generally fails even for multiset rewriting systems that satisfy certain natural balance conditions (imposed by the essence of the combinatorial problem). The main technical development of the paper, which is important for establishing that the mapping yielding the combinatorial bijection is functional, is that the `restricted' two-directional strong normalization holds for these multiset rewriting systems.

A formal analysis of some properties of Kerberos 5 using MSR

  Aaron D. Jaggard
University of Pennsylvania

Monday, April 1, 2002,
4:31PM     DRL 4C8

We present initial results of an ongoing analysis (joint work with F. Butler, I. Cervesato, and A. Scedrov) of Kerberos 5 using the MultiSet Rewriting (MSR) framework.

Kerberos 5 is intended to allow the repeated authentication of a client to multiple servers using a single login. We give MSR formalizations of this protocol at two levels of detail. This indicates the utility of the MSR framework in analyzing real world protocols and allows us to prove, in our abstract formalization, some authentication properties of this protocol. In the process, we find some anomalous behavior in the protocol. Our proofs of authentication properties use notions of rank and corank inspired by Schneider, and may suggest reasoning methods which are well suited to MSR.

Advantage and abuse-freeness in contract-signing protocols

  Rohit Chadha
University of Pennsylvania

Monday, March 18, 2002,
4:31PM     DRL 4C8

Distributed contract signing over a network involves many challenges in mimicking the features of paper contract signing. For instance, a paper contract is usually signed by both parties at the same time and at the same place, but distributed electronic transactions over a network is inherently asymmetric in that someone has to send the first message.

Several digital contract-signing protocols have been devised in order to overcome this basic asymmetry and to achieve symmetric properties such as fairness, namely: 1) if nothing goes wrong, both participants receive a valid contract, 2) every participant may complete the protocol, and 3) either both participants receive a valid contract or neither one does. Such protocols often involve a trusted third party that can enforce the contract after it witnesses a partial completion of the protocol. In optimistic contract-signing protocols the trusted third party is contacted only in case of a dispute, otherwise the protocol can be completed without involving the third party. Such protocols involve several subprotocols that allow a contract to be signed normally or aborted or resolved by the trusted third party.

Another kind of symmetry desirable in distributed contract signing was identified by Garay, Jakobsson, and MacKenzie: a fair protocol is said to be abuse-free if, at any stage of the protocol, it is impossible for any participant, say A, to be able to prove to an outside challenger that A has the power to choose between completing the contract and aborting it. A formal analysis of the Garay-Jakobsson- MacKenzie two-party contract-signing protocol was carried out by Mitchell and Shmatikov using a finite state verification tool. They showed that negligence of the trusted third party may lead to loss of abuse-freeness or fairness. Based on their analysis, Mitchell and Shmatikov also suggested a revision of the protocol. This revised version is our reference point.

We study an approximation of the abuse-freeness property, namely, at any stage of a fair protocol, any protocol participant does not have both the power to complete the contract as well as the power to abort it. As noted by Mitchell and Shmatikov, this property is not trace- based. We use a multiset-rewriting formalism for protocol analysis to formally state this property in terms of a certain recursive property of the protocol execution tree, which we then prove by inductive methods. Our proof relies on a strong notion of fairness adopted from which itself we formally state in the multiset-rewriting formalism and prove by inductive methods. We also show that our approximation of abuse- freeness, even though it is not a trace-based property, it may nevertheless be represented in by means of provability in a logical system, in the multiplicative additive fragment of linear logic, in which formal derivations correspond to full protocol execution trees and vice versa. This work was carried out in collaboration with Max Kanovich and Andre Scedrov.

We also discuss current work in progress with John Mitchell, Andre Scedrov, and Vitaly Shmatikov. We strengthen the definition of abuse-freeness in two ways. We consider strategies against honest participants interested in completing the contract and whose actions display a bias toward a positive outcome. We suggest a formulation of "evidence to an outside participant" by means of epistemic logic.

The Stable Paths Problem as a Model of BGP Routing

  Timothy Griffin
AT&T Research

Monday, March 4, 2002,
4:31PM     DRL 4C8

Inter-domain routing in the Internet is currently implemented with the Border Gateway Protocol (BGP). This protocol allows every autonomous administrative domain to define local routing policies that are consistent with its own interests. Such locally defined policies can interact in ways that cause various kinds of global routing anomalies --- nondeterministic routing and protocol divergence ("live lock") --- and these anomalies can span multiple autonomous domains making them very difficult to debug and correct. Analysis of BGP is complicated by the fact that route messages carry a number of semantically rich attributes that play a role in the BGP route selection algorithm and in the implementation of local routing policies. The talk will begin with a short tutorial on BGP, and so no previous knowledge will be assumed (don't panic!).

I'll present a simple static semantics for BGP called the Stable Paths Problem (SPP). This formalism can be viewed as a simple kind of game or as a generalization of the stable matching problem. I'll argue that the BGP protocol can be modeled as a distributed algorithm that attempts to solve instances of the Stable Paths Problem. If the Stable Paths Problem has no solution, the protocol will not converge. The protocol can also diverge when there is a solution but it gets "trapped" down a blind alley. Nondeterministic routing is associated with Stable Path Problems that have multiple solutions. I'll also show that several interesting questions related to SPP (and BGP) solvability are NP-complete, and I'll describe a recent extension to SPP needed to model BGP's ability to do "cold potato routing".

I'll survey joint work that I 've done with Lixin Gao (UMASS), Jennifer Rexford (AT&T Research) , F. Bruce Shepherd (Bell Labs), and Gordon Wilfong (Bell Labs). Papers can be found at http://www.research.att.com/~griffin/bgpresearch.html. An extended BGP tutorial can be found at http://www.research.att.com/~griffin/sigcomm2001_bgp_tutorial/abstract.htm.

Native XML processing in a statically typed language:
A progress report on the Xtatic design

  Benjamin C. Pierce
University of Pennsylvania

Monday, February 18, 2002,
4:31PM     DRL 4C8

The recent rush to adopt XML can be attributed in part to the hope that the static typing provided by DTDs (or more sophisticated mechanisms such as XML-Schema) will improve the robustness of data exchange and processing. However, although XML _documents_ can be checked for conformance with DTDs, current XML processing languages offer no way of verifying that _programs_ operating on XML structures will always produce conforming outputs.

In previous work, we have designed and implemented a domain-specific language for XML processing, called XDuce. The main novelties of XDuce are:
1) A type system based on REGULAR EXPRESSION TYPES. Regular expression types are a natural generalization of DTDs, describing structures in XML documents using regular expression operators (*, ?, |, etc.) and supporting a powerful form of subtyping.
2) A corresponding mechanism for REGULAR EXPRESSION PATTERN MATCHING, which supports concise "grep-style" patterns for extracting information from inside structured sequences.

The lessons learned from XDuce are now being incorporated in a new language, called Xtatic, whose design focuses on smooth integration of these novel XML-processing features into mainstream, object-oriented languages such as C#. The current vision is that Xtatic will be engineered as a lightweight extension to C#, offering native support for regular expression types and patterns and completely interoperable at the binary level with ordinary C# programs and APIs.

The talk will describe the basic design principles of Xtatic, the technical issues that have been addressed so far (in particular, the integration of regular expression types with the type structures of objects and classes), and the issues still requiring work.

A probabilistic polynomial-time calculus
for analysis of cryptographic protocols

  Andre Scedrov
University of Pennsylvania

Monday, February 11, 2002,
4:31PM     DRL 4C8

We describe properties of a process calculus that has been developed for the purpose of analyzing security protocols. The process calculus is a restricted form of pi-calculus, with bounded replication and probabilistic polynomial-time expressions allowed in messages and boolean tests. In order to avoid problems expressing security in the presence of nondeterminism, messages are scheduled probabilistically instead of nondeterministically. We prove that evaluation may be completed in probabilistic polynomial time and develop properties of a form of asymptotic protocol equivalence that allows security to be specified using observational equivalence, a standard relation from programming language theory that involves quantifying over possible environments that might interact with the protocol. We also relate process equivalence to cryptographic concepts such as pseudo-random number generators and polynomial-time statistical tests. The work has been carried out in collaboration with P. Lincoln, J. Mitchell, M. Mitchell, A. Ramanathan, and V. Teague.

On the continuity of the roots: old and new

  Florian Pop
IAS

Monday, January 28, 2002,
4PM     DRL 4N30

We will show how the classical theorem on the continuity of the roots of algebraic functions in one variable can be reduced via some ``easy'' model theory to an ``obvious fact''. This also leads to a vast generalisation of the result in discussion. Some questions about higher dimensional variants will be also asked/discussed.