Multiset Rewriting and the Complexity of Bounded Protocols

  Andre Scedrov,
University of Pennsylvania

Monday, December 4, 2000, 4:30 PM     Part 1
Monday, December 11, 2000, 4:30 PM     Part 2
Moore 554

Most current formal approaches to the analysis of cryptographic protocols use the same basic model of adversary capabilities, which appears to have developed from positions taken by Needham and Schroeder and a model presented by Dolev and Yao. In this idealized setting, a protocol adversary is allowed to nondeterministically choose among possible actions. Messages are composed of indivisible abstract values, not sequences of bits, and encryption is modeled in an idealized way. Adversary may only send messages comprised of data it "knows" as the result of overhearing previous messages.

Perhaps the simplest interpretation of protocol transitions is to consider them as a form of rewriting, so that protocol execution could be carried out symbolically. In addition to rewriting to effect state transitions, one also needs a way to choose new values, such as nonces or keys. While this seems difficult to achieve directly in standard rewriting formalisms, the logical inference rules associated with existential quantification appear to be just what is required. Therefore, we have adopted a notation that may be regarded as an extension of multiset rewriting with existential quantification. This formalism is closely related to the so-called existential Horn fragment of linear logic.

Using this formalism, it is shown that protocol security is undecidable even when rather severe restrictions are placed on protocols. In particular, even if data constructors, message depth, message width, number of distinct roles, role length, and depth of encryption are bounded by constants, secrecy is an undecidable property. If protocols are further restricted to have no new data (nonces), then secrecy is DEXPTIME-complete. If, in addition, the number of roles is bounded, then secrecy is NP-complete. Hardness is obtained by encoding decision problems from existential Horn theories without function symbols into our protocol framework. The way that encryption and adversary behavior are used in the reduction shed some light on protocol analysis.

This is joint work with Cervesato, Durgin, Lincoln, and Mitchell (12-th IEEE Computer Security Foundations Workshop, 1999).

The Church-Rosser Technique and a High-School Proof for Euler's Partition Theorem

 Max Kanovich,
University of Pennsylvania

Monday, November 27, 2000, 4:30 PM
Moore 554

This topic has been arisen in my 500 course "Programming Languages and Techniques". It has been inspired by the homework problem by Peter Buneman - that of writing down a recurrence relation for the number of partitions of n in which
(a) all the parts are odd, (e.g. 10 = 3+3+1+1+1+1),
(b) all the parts are distinct, (e.g. 10 = 6+4).

Notwithstanding the different recurrence relations, the Euler's generating functions provide us with the same numbers of odd partitions and distinct partitions for a given n.

The next question is to find an explicit bijection between partitions into odd parts and partitions into distinct parts.

Kathy O'Hara came up with the bijective proof based on the following 'local' transformations:
1+1->2, 2+2->4, 3+3->6, 4+4->8, 5+5->10, ...
E.g., 3+3+1+1+1+1 -> 3+3+2+1+1 -> 6+2+1+1 -> 6+2+2 -> 6+4

The key to her approach is that the mapping that it produces is an actual total bijection, in particular, it is independent of the order in which the transformations are chosen - "but this requires a good deal of effort to prove" (cited from Herbert Wilf's "Lectures on Integer Partitions")

For a big variety of partition problems, I will show a direct and transparent proof of that we get the desired bijection:
(1) whatever sequence of the 'local' transformations terminates,
(2) whatever terminated sequence of the 'local' transformations yields one and the same result,
(3) whatever sequence of the inverse 'local' transformations terminates,
(4) and, whatever terminated sequence of the inverse 'local' transformations yields one and the same result.

Automata for Event Monitoring

 Karthikeyan Bhargavan,
University of Pennsylvania

Monday, November 20, 2000, 4:30 PM
Moore 554

We consider the problem of monitoring an interactive device, such as an implementation of a network protocol, in order to check whether its execution is consistent with its specification. At first glance, it appears that a monitor could simply follow the input-output trace of the device and check it against the specification. However, if the monitor is able to observe inputs and outputs only from a vantage point externa} to the device---as is typically the case---the problem becomes surprisingly difficult. This is because events may be buffered, and even lost, between the monitor and the device, in which case, even for a correctly running device, the trace observed at the monitor could be inconsistent with the specification.

In this paper, we formulate the problem of external monitoring as a language recognition problem. Given a specification that accepts a certain language of input-output sequences, we define another language that corresponds to input-output sequences observable externally. We also give an algorithm to check membership of a string in the derived language. It turns out that without any assumptions on the specification, this algorithm may take unbounded time and space. To address this problem, we define a series of properties of device specifications or protocols that can be exploited to construct efficient language recognizers at the monitor. We characterize these properties and provide complexity bounds for monitoring in each case.

To illustrate our methodology, we describe properties of the Internet Transmission Control Protocol (TCP), and identify features of the protocol that make it challenging to monitor efficiently.

Joint work with Satish Chandra, Pete McCann, Carl Gunter.

Fault Origin Adjudication

 Karthikeyan Bhargavan,
University of Pennsylvania

Monday, November 13, 2000, 4:30 PM
Moore 554

It is generally accepted that non-trivial computer programs will have faults. It is also well known that faults can derive from each of several stages of the software engineering lifecycle. For instance, a program P may deviate from its detailed specification S. But it is also possible that the specification S was incorrect because it failed to ensure high-level user requirements R. In this paper we introduce a technique for automated analysis to determine which of these two possibilities obtains, assuming that high-level requirements have been properly expressed and a deviation from them has been found. We call this process Fault Origin Adjudication (FOA).

To see a characteristic example, suppose a development project is implementing a standard specification S of a communication protocol. This protocol is expected to have a property R, but testing of the program reveals that the program fails to satisfy R for some test input W. Clearly the problem needs to be repaired, but the way it needs to be repaired depends on the origin of the fault. If the program does not conform to the standard, then this may be the cause of the failure: the program should be revised to conform. This conformance should ensure interoperability with other implementations of S. Moreover, the design of S was probably intended to guide the implementor to a program that satisfies R. However, if the standard does not ensure the requirement, then the standard specification may be the origin of the difficulty. In the worst case, no conformant implementation of the standard will satisfy the property R. In a less extreme case, there is a risk that some implementations will conform with the standard but not satisfy R, leading to potential failures. Thus, if the fault lies with S, then the matter needs to be referred to the standards body and a revision of S should be made.

We demonstrate how the SPIN Model Checking Environment can be used along-side a trace generation utility like NS, to carry out Fault Origin Adjudication for Network Protocols.

Joint work with Carl Gunter, Davor Obradovic

Verisim: Formal Analysis of Network Simulations

 Carl A. Gunter
University of Pennsylvania

Monday, November 6, 2000, 4:30 PM
Moore 554

Network protocols are often analyzed using simulations. We demonstrate how to extend such simulations to check propositions expressing safety properties of network event traces in an extended form of linear temporal logic. Our technique uses the NS simulator together with a component of the Java MaC system to provide a uniform framework. We demonstrate its effectiveness by analyzing simulations of the Ad Hoc On-Demand Distance Vector (AODV) routing protocol for packet radio networks. Our analysis finds violations of significant properties, and we discuss the faults that cause them. Novel aspects of our approach include modest integration costs with other simulation objectives such as performance evaluation, greatly increased flexibility in specifying properties to be checked, and techniques for analyzing complex traces of alarms raised by the monitoring software.

This is joint work with Karthikeyan Bhargavan, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, and Mahesh Viswanathan.

Undecidability of Monadic Horn Theories based on Linear and Affine Logics.

 Max Kanovich
University of Pennsylvania

Monday, October 30, 2000, 4:30 PM
Moore 554

Horn theories based on certain refined logical systems (as linear logic and affine logic) have been proven to be adequate logical formalisms for AI planning problems, (timed) transition systems, protocol analysis, and, furthermore, game winning strategies. As for the propositional case, we know that the pure Horn fragment of linear logic is equivalent to the Petri nets, and, hence, it is decidable. The general first-order case is undecidable by the classical reasons of the undecidable first-order classical logic. As for the monadic case, contrary to what might have been expected (due to Buchi, Rabin), we prove the following undecidability results: - there is an undecidable pure Horn theory based on linear logic, which has no functional symbols at all, and

Automatic Abstraction through Syntactic Program Transformations

 Kedar Namjoshi
Bell Labs

Monday, October 23, 2000, 4:30 PM
Moore 554

I will present an algorithm that constructs a finite-state abstract program from a given, possibly infinite-state, concrete program by means of syntactic program transformations. Starting with an initial set of predicates from a specification, the algorithm iteratively computes the predicates required to produce an abstraction relative to that specification. These predicates are represented by boolean variables in the finite-state abstract program.

We show that the method is sound, in that the abstract program is always guaranteed to simulate the original. We also show that the method is complete, in that, if the concrete program has a finite abstraction with respect to simulation (bisimulation) equivalence, the algorithm can produce a finite simulation-equivalent (bisimulation-equivalent) abstract program. Syntactic abstraction has two key advantages: it can be applied to infinite state programs or to programs with large data domains, and it permits the effective application of other reduction methods for model checking. We show that our method generalizes several known algorithms for analyzing syntactically restricted, data-insensitive programs.

Joint work with Bob Kurshan, Bell Labs

Relating Cryptography and Polymorphism

Eijiro Sumii
University of Pennsylvania

Monday, September 25, 2000, 4:30 PM
Moore 556

Cryptography is information hiding. Polymorphism is also information hiding. So is cryptography polymorphic? Is polymorphism cryptographic?

To investigate these questions, we define the _cryptographic lambda-calculus_, a simply typed lambda-calculus with shared-key cryptographic primitives. Although this calculus is simply typed, it is powerful enough to encode recursive functions, recursive types, and dynamic typing. We then develop a theory of relational parametricity for our calculus as Reynolds did for the polymorphic lambda-calculus.
This theory is useful for proving equivalences in our calculus; for instance, it implies the non-interference property: values encrypted by a key cannot be distinguished from one another by any function ignorant of the key. We close with an encoding of the polymorphic lambda-calculus into the cryptographic calculus that uses cryptography to protect type abstraction.

Our results shed a new light upon the relationship between cryptography and polymorphism, and offer a first step toward extending programming idioms based on type abstraction (such as modules and packages) from the civilized world of polymorphism, where only well-typed programs are allowed, to the unstructured world of cryptography, where friendly programs must cohabit with malicious attackers.

Joint work with Benjamin Pierce. A full paper is available.

Advanced Module Systems: A Guide for the Perplexed

Benjamin Pierce
University of Pennsylvania

Monday, September 11, 2000, 4:30 PM
Moore 556

 The past three decades have seen a plethora of language features for large-scale software composition. Some of these are fairly simple, others quite sophisticated. Each embodies an implicit claim that its particular combination of features is both necessary and sufficient for some problem domain. But there have been few attempts to compare module systems, or to explain the practical and theoretical issues that motivate the choices they embody. This can make it difficult to evaluate which features are really needed for a given setting, and which may be overkill. We offer here an overview of the design space of module systems, with reference to those of some well-known languages (especially the ML family and Java), and record the motivating examples and crucial design choices underlying some central features. In particular:

* we identify a fundamental distinction between unresolved, resolved, and generic references between modules;
* we compare different ways of handling families of interfaces (in particular, abstracted vs. augmented interfaces);
* we investigate the need for coherence (or "sharing'') constraints and consider different ways of expressing them;
* we confirm a folk theorem that sharing by parameterization doesn't scale as well as sharing by specification; and
* we explain the significance of the phase distinction for the design of first- and second-class module systems, and the distinctions between first-order and higher-order variants of second-class systems.

Joint work with Bob Harper.

Deriving operational congruences for reactive systems

James Leifer
Cambridge University

Monday, August 28, 2000, 4:30 PM
Moore 556

 Assigning mathematical interpretations (semantics) to computer programs allows us to prove that code is correct with respect to a specification, to make precise how a compiler works and what optimisations are valid, to compare language features, etc. Many interpretations exist for sequential computation and typically model a (deterministic) program as a function from memories to memories that  maps each state to the one that holds after the program executes.

The situation is more complex when considering parallel computation, and, in particular, languages presented in terms of reaction rules (characterising the primitive interactions) that cater for communication, distribution, mobility, and security. It is a major challenge to find a compositional semantic interpretation (one that respects the constructions of the language) and, in practice, is either impossible or accomplished in an ad hoc manner with a difficult hand-crafted proof of compositionality bolted on.

I describe new work that begins to address this challenge. I first show how to derive uniformly a labelled transition system (LTS) from a set of reaction rules, taking the labels, or  "observations'', to be those contexts which are just large enough to enable a reaction: a program undergoes a labelled transition exactly when it requires the entire label to react. The key contribution is the precise definition of  "just large enough'' in terms of the categorical notion of relative pushout. I prove using some lightweight reasoning that operational equivalences built from the LTS such as strong and weak bisimilarity and trace equivalence are congruences. Thus the semantic interpretation of programs in terms of these equivalences is guaranteed to be compositional. I conclude by touching on some future work.

Joint work with Robin Milner.

Jen Davoren
Australian National University, Canberra

Monday, August 14, 2000    4:30 PM
Moore 556

 Hybrid systems are heterogeneous dynamical systems characterized by a non-trivial interaction of continuous and discrete dynamics, and typically arise in the embedded software control of physical processes. The widely accepted hybrid automaton model consists of a finite collection of continuous systems defined by differential equations, over a common state space, together with a mechanism which decides when and how the system can switch between these continuous sub-systems. We consider the following type of control problem. Given a finite collection of continuous systems, design and build a hybrid automaton model for that collection so that every hybrid trajectory of the resulting system is guaranteed to satisfy a given list of performance specifications. One novelty of our work is that in addition to the well-studied classes of safety and liveness properties of hybrid trajectories, we also address a quite general class of event sequence properties, by which one can enforce positive behavioural requirements on hybrid trajectories. We develop an abstract algorithm to solve this control problem for which we can guarantee finite termination. A central idea is that in tackling the problem, one needs to reason about sets of continuous states, and to build up complex sets of states using operators on sets induced by the given continuous flows and data from the specifications. We demonstrate how such reasoning and construction of sets can be cleanly and naturally formalized in the language of modal logic. The benefits of using the technical tool of modal logic are two-fold. First, it gives us a formal language in which to formulate our solution algorithm. Second, a proof of correctness can transparently be derived from a theory of modal formulas that are true of any hybrid automaton solution purely in virtue of the statement of the algorithm. The abstract algorithm will be illustrated via a simple example, with output generated by our prototype software implementation.

(Joint work with Dr. Thomas Moor, RSISE, ANU)

Short bio: Jen Davoren is a research fellow in the Computer Sciences Laboratory at the Research School of Information Sciences and Engineering at the Australian National University. She has a PhD in mathematics and an MSc in computer science from Cornell University, after undergraduate studies in mathematics and philosophy at the University of Melbourne, Australia. Prior to starting at the ANU last September, she had a postdoc position at Cornell with extended visits to the Dept. EECS at U.C. Berkeley.

Dependently Types Records for Representing Mathematical Structure

Randy Pollack
University of Durham

Thursday, Aug 10, at 3:00 PM
Moore 556

Randy will be visiting the CIS department on Thursday and Friday. Please contact bcpierce@cis.upenn.edu if you'd like to meet with him. His LCS seminar will continue informally during the PL Club lunch on Friday (12:30-2, in the Theory Lab). 

It is folklore that dependently typed tuples suffice to formalize abstract mathematical structures such as semi-group, monoid, group, ring, field, ... We want natural properties of informal mathematical language to be preserved; e.g. inheritance of properties and sharing of substructures. There is a big literature on the related topic of programming language modules.

This talk develops a notion of dependently typed records by adding field labels to Sigma types. Some obscure features from the literature are simplified and explained. E.g. field variables (local) vs field labels (global) are explained by ordinary lambda-binding. Subtyping is orthogonal to records, and is introduced using Luo's coercive subtyping. (Hence I do not explain the subtyping system in detail, but only show some examples.) 

I discuss the two standard approaches to sharing substructures: "Pebble style" and "manifest types" (ML style). By example, I argue that we really do need manifest types to formalize mathematics. I extend dependently typed records to include manifest types and the "with" notation for adding manifest information to an existing signature.

Most recently, I have been able to directly program records with first-class labels, dependent, manifest signatures and "with" in type theory, using Dybjer's "inductive-recursive" definition. All of the rules (projection, subtyping, "value rules", definition of "with") are derivable from the inductive-recursive definition, which has only three constructors and three corresponding computation rules. 

A preliminary paper is available 

Automatic Verification of Parameterized Cache Coherence Protocols

Giorgio Delzanno
DISI - University of Genova

Thursday, July 24, 2000, 3:00 PM
Moore 554

 We propose a new method for the verification of parameterized cache coherence protocols.
Cache coherence protocols are used to maintain data consistency in multiprocessor systems equipped with local fast caches. 
In our approach we use arithmetic constraints to model possibly infinite sets of global states of a multiprocessor system with many identical caches.
In preliminary experiments using symbolic model checkers for infinite-state systems based on real arithmetics (HyTech and DMC we have automatically verified safety properties for parameterized versions of widely implemented write-invalidate and write-update cache coherence policies like the Mesi, Berkeley, Illinois, Firefly and Dragon protocols.
With this application, we show that symbolic model checking tools originally designed for hybrid and concurrent systems can be applied successfully to a new class of infinite-state systems of practical interest.