Network Specification Case Studies: To facilitate the use of the Maude tool for specifying the active networks architecture and mechanisms we are collaborating with the group of Prof. Jose Garcia-Luna at University of California, Santa Cruz, the group of Prof. Carl Gunter at the University of Pennsylvania, and with the ANCORS project led by Livio Ricciulli at SRI International to jointly develop a collection of active network specification case studies to clearly demonstrate the usefulness of our approach and to serve as tutorial material to encourage and facilitate the use of Maude specifications by other research teams in the program.
Mobile Maude Language Design and Implementation: Having formal executable specifications can be a great help in designing and simulating active networks and their components. An even greater help is being able to transform those executable specifications into actual mobile code through provably correct program transformations and then being able to deploy such code in actual testbeds. This is of course an ambitious goal, but the wide-spectrum nature of Maude will make the task much easier than with conventional code, thus yielding very high levels of assurance not just at the specification level, but for code as well. In essence, the goal is to design a next-generation mobile language ideally suited for active networks and for which systematic application of formal methods for verification purposes is a realistic goal. By explicitly providing integration of conventional code via the foreign interface module wrapping mechanism, Mobile Maude will also provide a good migration path from current languages to this next-generation technology. In FY98 we have begun the design of Mobile Maude; a first implementation is planned for FY99.
Security Modeling and Formal Reasoning: Security is of utmost importance for active networks and, given the level of dynamic adaptation and mobility required, achieving it will pose challenging technical problems. New formal security models, new specification formalisms, and new proof techniques are needed. Since rewriting logic is a very good formalism for the formal modeling and specification of distributed open object systems, including their reflective features, it is very fitting to adopt it as a mathematical framework in which to carry out the investigation of the new security models that will be required. Since Maude is also based on rewriting logic, this has the important advantage of making such models executable, and therefore naturally integrated within the overall wide-spectrum refinement approach that we advocate. During FY98 we have begun to demonstrate the usefulness of our approach to security by formally modeling secure communication protocols and finding security violations in them by formal analysis. We have also begun studying the formal semantics of protocol composition as a basis for proving security properties of composed services.
Using Maude as an executable specification language and performing Maude-based model checking, we have uncovered and corrected several important flaws and deadlocks in the initial, informal design of a reliable broadcast protocol in collaboration with the group of Prof. Jose Garcia-Luna at University of California, Santa Cruz. This case study, currently being extended to the dynamic topology case, has demonstrated the great usefulness of using Maude in the early stages of protocol design by showing how many errors can thus be identified and eliminated, and by the naturalness and very intuitive character of the specifications, that can be developed by communication engineers.
In collaboration with Prof. Carl Gunter and his student Yaw Wang at the University of Pennsylvania we have formally specified an active network program in the PLAN language, and have formally analyzed such a program using Maude to validate some basic correctness properties. To our knowledge, this is the first PLAN program to be formally analyzed in a systematic way.
Denker, Talcott and Meseguer have developed a new general formal modelling methodology for security protocols in which agents and attackers are specified as concurrent objects communicating through messages. This methodology offers important advantages in terms of executability of the protocols for early validation and of new model checking and formal analysis techniques. They have illustrated this methodology by developing an executable formal specification of the Needham-Schroeder cryptographic protocol and of a very general attacker, and using Maude-based formal analysis techniques they have exhibited an attack violating the protocol's security requirements. This work has been presented in June at the Formal Methods and Security Protocols Meeting in Indianapolis. Related work on composition of secure and fault-tolerant protocols and on use of temporal logic in conjunction with Maude specifications is currently underway.
Design work on Mobile Maude has begun with a new design of Maude's metalevel that allows a natural extension to a mobile and distributed version. The first application programs for Mobile Maude, based on the idea of parallel search strategies, have also begun to be developed. More design work is planned for the following months.
Last updated by
Carolyn Talcott clt@cs.stanford.edu
13 July 1998.