SDRL
Systems Design Research Lab
 
 

Question or Comment
Contact: Valentina Sokolskaya
Last updated: January 31, 07

Fall 1999 Seminars

We have seminars together with Logic and Computation Group
each Monday at 4:30PM
University of Pennsylvania, Moore 554

 

 

Back to seminars 2000 list

 

 

Interval Duration Logic: Expressiveness and Decidability

Paritosh Pandya
Tata Institute, Mumbai

Tuesday, December 7, 1999, 10 - 11 a.m.
Theory Lab 

Interval Duration Logic is a form of Interval Temporal Logic where formulae are evaluated at time intervals rather than at time points. The duration of a proposition gives the amount of (real) time for which the proposition remains true in an interval. Basing itself upon these primitives, logic IDL provides a novel vocabulary for describing reactive and real-time systems.

In this talk we will present the foundations of logic IDL. While the full logic is undecidable, we will give an automata theoretic decision procedure for a subset of IDL consisting only of "located time constraints". This fragment LIDL is shown to be expressively complete with respect to the Event Clock Automata. A modelchecker, called DCVALID, implementing this decision procedure will be described.

 

Analysis of Software Accidents, Attacks, and Disagreements
Part II: Software Engineering Standards

Michael McDougall
University of Pennsylvania

Monday, December  6, 1999, 4:30 PM
Moore 554

In 1992 the London Ambulance Service (LAS) switched from a manual dispatch system to a software controlled system. The system promptly failed, resulting in the loss of emergency calls and slow ambulance response times. Software engineering standards are designed to prevent such software disasters, but these standards force a developer to spend time and money meeting the requirements of the standard. Standards do not guarantee that a given project will be successful, and developers often decide that their time and money could be better spent on other things. This talk will cover an analysis of the LAS failure with respect to the ISO 12207 software engineering standard. I will try to answer the following questions: Would adherence to ISO 12207 have prevented the failure? Would ISO 12207 have made any difference at all? 

 

Analysis of Software Accidents, Attacks, and Disagreements
Part I: Fundamentals and Models

Carl Gunter
University of Pennsylvania

Monday, November 29, 1999, 4:30 PM
Moore 554

In some areas of engineering, like commercial aviation, diligent analysis of accidents has led to steady improvements in safety. Analysis of software failures is a topic of common interest among computer professionals too, as evidenced by sources like the ACM Risks column. This talk will describe a software engineering perspective on fundamental concepts of analysis and three case studies. Fundamentals include the concepts of causality, liability, and evidence. We consider two "classic" case studies: Leveson and Turner's study of the Therac 25 accidents, and Spafford's study of the Morris Internet worm attack. I will provide an additional study based on disagreements (lawsuits) about breach of contract and fraud. The focus in these studies concerns the obligations implied by commercial software specifications in terms of the software reference model developed by myself, Elsa L. Gunter, Michael Jackson, and Pamela Zave. 

 

A Formal Framework and Evaluation Method for Network Denial of Service

Catherine Meadows
Naval Research Laboratory

Monday, November 22, 1999, 4:30 PM
Moore 554
 
Denial of service is becoming a growing concern. As our systems communicate more and more with others that we know less and less, they become increasingly vulnerable to hostile intruders who may take advantage of the very protocols intended for the establishment and authentication of communication to tie up our resources and disable our servers. Since these attacks occur before parties are authenticated to each other, we cannot rely upon enforcement of the appropriate access control policy to protect us. Instead we must build our defenses, as much as possible, into the protocols themselves. This paper shows how some principles that have already been used to make protocols more resistant to denial of service can be formalized, and indicates the ways in which existing cryptographic protocol analysis tools could be modified to operate within this formal framework.

Back to seminars list

 

Strand Spaces

Alfred Maneki
National Security Agency

Wednesday, November 17, 1999, 3:00 PM
 Moore 212

In a communications network, cryptographic protocols are used either to verify the authenticity of communicating parties or to establish cryptographic keys shared by these parties for the purpose of secret communications. Typically, each party in a network holds long term "secret" keys. Parties wishing to verify the identity of other parties (authentication) or to establish session keys (secrecy) will employ a specific cryptographic protocol (a prescribed sequence of exchanged messages using one's long term secret key and sometimes the services of a trusted network server) for these purposes.

With the rapid development and deployment of communications networks, many cryptographic protocols have been designed and implemented. Given their widespread use, and our dependence on these for providing critical security functions, the evaluation of these protocols has consist of a search for vulnerabilities; i.e., the development of attacks by other parties in the network who may wish to interfere with the communications between legitimate parties or to recover the information being shared between legitimate parties. If the evaluation does not yield the existence of such vulnerabilities, then the evaluator is faced with the daunting task of "proving" the correctness of the security features of the protocol.

Since cryptography is used in these protocols their evaluation depends heavily on an understanding of how the underlying cryptography is used. Beyond that, the evaluator must keep an open mind to the misuses of the protocol and must be willing to employ a wide variety of techniques from the field of mathematics, logic, and computer science. As a measure of the difficulty of the task of evaluating a protocol,
many widely used protocols, thought to be secure for many years, were ultimately shown to be flawed.

A number of researchers have proposed methodologies for protocol evaluation. In this lecture we will describe the theory of strand spaces proposed by Joshua Guttman and his colleagues at MITRE. As a methodology for evaluating cryptographic protocols, strand spaces have the advantage of incorporating techniques developed by Millen, Meadows, Roscoe, Lowe, and others. Further investigations have shown that strand space theory can be extended and generalized in many ways. In this lecture, we present the basic definitions, motivate the fundamental theorems, and give an outline of their proofs. We will conclude the lecture by applying strand space theory to the TMN protocol.

Back to seminars list

 

A Decision Procedure for Noninterference

Sylvan Pinsky
National Security Agency

Wednesday, November 17, 1999, 3:00 PM
Moore 212

Noninterference was introduced by Goguen and Meseguer to provide a foundation for the specification and analysis of security policies. The intuitive notion that a security domain U is noninterfering with a security domain V is conveyed by stating that no action performed by U can influence subsequent outputs seen by V. This lecture gives an introductory formulation of this concept and provides necessary and
sufficient conditions for a system to satisfy noninterference. Security is defined in terms of allowable flows of information among security domains. We examine properties of special sets called basis elements which are generated from the interference relationship defined from the allowable flows of information. We present a decision procedure for noninterference when the system is deterministic.

Back to seminars list

 

Finite Bisimulations of Linear Differential Equations

George Pappas

Monday, November 15, 1999, 4:30 PM
 Moore 554

In this talk, I will focus on algorithmic methods for exactly computing the reachable states of hybrid systems. Current state of the art methods perform reachability computation for untimed, timed, multirate, and rectangular hybrid automata before reaching undecidability barriers. Using the very recent notion of order minimality from geometric model theory, the first class of hybrid systems with linear differential equations having a decidable reachability problem is obtained. This importance of this result is immediate given the wide applicability of linear differential equations in systems theory and applications.

Joint work with Gerardo Lafferriere, Shankar Sasrty, and Sergio Yovine.

Back to seminars list

 

Reasoning About Secrecy for Active Networks

Pankaj Kakkar

Monday, November 8, 1999, 4:30 PM
Moore 554

In this talk, we present a language of mobile agents called uPLAN for describing capabilities of active (programmable) networks. We demonstrate, using a formal semantics for uPLAN, how capabilities provided for programming the network can impact the security of the network and the potential flows of information between users. We formalize a concept of security against attacks on secrecy by an `outsider' and show how basic protections of this kind are preserved in the presence of programmable network functions like user-customized labeled routing. Finally, we show how this relates to some well-known concepts of information flow in mobile calculi. 

Joint work with Carl A. Gunter and Martin Abadi

Back to seminars list

 

    Formal Verification of Distance Vector Routing Protocols

    Davor Obradovic

Monday, November 1, 1999, 
4:30 PM, Moore 554

The purpose of routing protocols is to devise routes (i.e. paths) between hosts of a network. It is important that this procedure converges to a stable set of routes to desired destinations and to do so with real-time bounds. The Routing Information Protocol (RIP) is a widely-used routing protocol on small internets. The Ad Hoc On-Demand Distance Vector (AODV) Protocol is a proposed standard for Wireless Networks. Both are instances of Distance Vector Routing. We aim to provide a framework for formal reasoning about these protocols. We show how to use an interactive theorem prover, HOL, together with a model checker, SPIN, to prove key properties of distance vector routing protocols. We do three case studies: correctness of the RIP standard, a sharp real-time bound on RIP stability, and preservation of loop-freedom in AODV. We develop verification techniques suited to routing protocols generally. These case studies show significant benefits from automated support in reduced verification workload and assistance in finding new insights and gaps for standard specifications.

Joint work with Karthikeyan Bhargavan, Carl Gunter, U of Penn.

[1] Formal Verification of Standards for Distance Vector Routing Protocols, Karthikeyan Bhargavan, Carl Gunter and Davor Obradovic, August 1999, Under Review.

Back to seminars list

 

Featherweight Java: a minimal core calculus for Java and GJ

Atsushi Igarashi

Monday, October 25, 1999, 4:30 PM
Moore 554

Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy.

Featherweight Java bears a similar relation to full Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational ``feel,'' providing classes, methods, fields, inheritance, and dynamic typecasts, with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The syntax, type rules, and operational semantics of Featherweight Java fit on one page, making it easier to understand the consequences of extensions and variations.

As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and sketch a proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

Back to seminars list

 

Translation Validation

Amir Pnueli
Weizmann Institute of Science

Tuesday, October 19, 1999
Moore School - Room 216
3:00 - 4:30 p.m.

National and International regulations require that the development of software for safety-critical systems is conducted by a process that achieves very high standards of rigor and quality assurance. In particular, it requires that every stage in the process be certified and any tool used (such as code-generator or compiler) be qualified by an external authority appointed by appropriate government agencies. This puts an additional heavy burden on the developers of such software and, in many cases, prevents them from using state-of-the-art technologies and forces them to use outdated techniques and tools.

In this talk, we present a new approach to the task of ensuring the correctness of the code-generator tool (translator). Rather than verifying the translator once and for all, we construct a "validator tool" which verifies each translation as it is produced. The validator accepts as inputs the source and the target code, as it was produced by the translator, and attempts to verify formally that the produced target code is a correct implementation of the source. In case of failure, the validator produces a counter example, indicating a possible mismatch between the source and the target.

We start with a short introduction to synchronous specification languages and their natural "event-based" semantics, and identify the special properties of these languages and their translators which made a fully automatic validation of several thousands line programs possible. We then explain the main algorithmic approach to the verification process which is based on equality logic of uninterpreted functions, and its efficient resolution by small-model instantiation.

The resulting efficient decision procedure has been effectively utilized also for the verification of out-of-order super-scalar processor designs, as we will briefly outline. Under future research, we will discuss the extensions necessary for extending this successful technology to more complex source languages and optimizing compilers.

Brief Biography

Amir Pnueli is a Professor at the Weizmann Institute of Science in the Department of Applied Mathematics & Computer Science. Dr. Pnueli's research focuses on the verification of reactive, real-time, and hybrid systems. In his pioneering paper in 1977, Prof. Pnueli proposed to use temporal logic for specification of correctness requirements. He is considered to be the leading authority in formal verification, and was awarded the A.M.Turing award by ACM, the most prestigious award in computer science. He is the author over 100 publications, has served on various program committees and editorial boards, and is on the steering committees of various conferences including the International Conference on Computer-Aided Verification.

Back to seminars list

 

Run-time Assurance Based On Formal Specifications

Insup Lee
University of Pennsylvania

Monday, September 20, 1999, 4:30 PM
Moore 554

We describe the Monitoring and Checking (MaC) framework that assures the correctness of the current execution at run-time. Monitoring is performed based on a formal specification of system requirements. Our framework is to bridge the gap between formal verification and testing. The former is used to ensure the correctness of a design specification rather than an implementation, whereas the latter is to used to validate an implementation. An important aspect of the framework is clear separation between implementation-dependent description of monitored objects and high-level requirements specification. Another salient feature is automatic instrumentation of executable code. The paper presents an overview of the framework and two languages for specifying events and conditions and their three-value logic semantics. These two languages are used to specify what to observe in the program and the requirements that the program must satisfy, respectively. This talk also briefly describes our current prototype implementation in Java as well as future work such as steering and applying the framework to simulation and security.

Joint work with Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, and Mahesh Viswanathan.

Back to seminars list

Back to seminars home page