jose nov 04

CONTESSA : CONTESSA A Logical Framework for Adaptive Systems Interoperability UMBC Review Meeting, November 19, 2004 José Meseguer University of Illinois at Urbana-Champaign


Today’s Agenda : Today’s Agenda


The CONTESSA Team : The CONTESSA Team Gul Agha (UIUC) Carl A. Gunter (UIUC, previously UPenn) José Meseguer (UIUC) Gruia-Catalin Roman (WUSTL) Nalini Venkatasubramanian (UCI)


Postdocs and Students : Postdocs and Students Postdocs: 5 Roberto Bruni Santiago Escobar Peter Csaba Ölveczky Mark-Oliver Stehr Prasanna Thati Kaijun Tan Research Faculty: 1 Michael Greenwald Ph.D. Students: 21 M.S. Students: 9 B.S. Students: 7


CONTESSA Web Page: formal.cs.uiuc.edu/contessa : CONTESSA Web Page: formal.cs.uiuc.edu/contessa


Research Challenges : Research Challenges Adaptation & Interoperation Trends Internet Nomadic Ad Hoc Sensor Standalone Heterogeneous Systems Systems of Systems 3 years 2 years Models & Analysis Middle- ware Support Crosscutting Concerns: Security Reliability Rapid Development


Project Goals : Project Goals Address Fundamental Problems of System Interoperation, Integration, Composition, and Adaptation Key Problem: Lack of Semantic Models and Predictive Power in the Design of Complex Systems


Key Idea : Key Idea In order to properly interoperate systems it is crucial to Develop executable formal models of these systems and their operating environment Interoperate those models We use Rewriting Logic as a Logical Framework and its Implementation in Maude


Methodology : Methodology Requirements Formal Executable Specifications Code Formal Analysis Formal Analysis Rewriting Logic Analysis Results


Enabling Technologies : Enabling Technologies Mobile Agents Adaptive Middleware Composable Network Protocols Applications Middleware Services Network Infrastructure


Mobile Agents for Interoperability : Mobile Agents for Interoperability Models of Mobile Interoperability Coordination Technologies Mobile Ad Hoc Networks Mobility in Sensor Networks


Adaptive Middleware : Adaptive Middleware Russian Dolls Model Two-Level Actor Model (TLAM) Adaptation and Context-Awareness Service Provision Grid Computing Secure Group Communication Power-Aware Middleware


Composable Network Protocols : Composable Network Protocols Composition of Secure Tunnels Spatiotemporal Communication Services Power-Aware Routing WSEmail & Workflow


Security and Reliability as Crosscutting Aspects : Security and Reliability as Crosscutting Aspects Applications Middleware Services Network Infrastructure Formal Models Security & ReliabilityProperties ? Formal Analysis Tools


Formal Security Analysis : Formal Security Analysis Execution Environment for MSR (NRL) Modeling and Analysis of Network Protocols Probabilistic Extension of Dolev-Yao Modeling and Analysis of DoS Threats and Counter-Measures Narrowing Analysis of Crypto-Protocols Secure Group Communication (Secure Spread and Cliques) Formal Models and Analysis of Intrusion Detection


Scalable Formal Methods : Scalable Formal Methods Executable Specifications Specification-Based Monitoring Statistical Verification of Probabilistic Models State Space Exploration Model Checking of Abstractions


The CONTESSA Network : The CONTESSA Network


The CONTESSA Network : The CONTESSA Network Group Communication: Adaptivity, Security, Network Abstraction Security Gateway Configuration: Sectrace, L3A, SIKE Cryptoprotocol Specification & Analysis: Maude, MSR Probabilistic Models: Probabilistic Rewriting, Models for DoS Spatiotemporal Models: Spatiotemporal Specifications/Communication Agents and Coordination: Agent Systems, Models of Interoperation Mobile Systems and Protocols: Sensor Networks, Ad Hoc Networks Middleware: Reflection Adaptation & Context Awareness Service Provision


What can we do what we could not do three years ago ? : What can we do what we could not do three years ago ? DoS countermeasures and formal analysis Logical simulation and analysis of network potocols Probabilistic models and analysis of large distributed systems Reasoning about adaptive communication Adaptive middleware services for mobile and sensor systems


Project Metrics : Project Metrics Research Output, Quality, and Impact Strong Research Interactions Educational Impact DoD and Industry Relevance Transferable Technologies


Research Output Statistics : Research Output Statistics Published Papers: 113 Technical Reports: 33 Software Systems: 12 Formal Analysis Tools: 12 Experiments, Simulations, and Case Studies: 23 Ph.D. degrees: 4 M.S. degrees: 9


Research Quality and Impact : Research Quality and Impact Invited Talks in International Meetings: 17 PC Memberships in Intl. Conferences: 74 Conferences and Workshops organized: 7 Membership in Journal Editorial Boards: 5 Download Statistics: Maude: 1398 hosts in the last 16 months


Research Quality and Impact : Research Quality and Impact Journals and Conferences in which we publish: International Conference on Formal Methods and Models for Co-Design International Conference on Automata, Languages, and Programming International Conference on Rewriting Techniques and Applications International SPIN Workshop International Conference on Automated Deduction International Symposium on Logic-based Program Synthesis and Transformation International Formal Methods Europe Symposium International Workshop on Rewriting Logic and its Applications IFIP International Conference on Formal Methods for Open Object-based Distributed Systems International Conference on Fundamental Approaches to Software Engineering IEEE International Workshop on Object-Oriented Real-Time Dependable Systems ACM SIGSOFT Symposium on Foundations of Software Engineering International Conference on Tools and Algorithms for the Construction and Analysis of Systems


Research Quality and Impact : Research Quality and Impact Journals and Conferences in which we publish (continued): Asian Computing Science Conference Workshop on Runtime Verification International Conference on Software Engineering International Workshop on Security Issues in Coordination Models, Languages, and Systems International Conference on Pervasive Computing International Conference on Coordination Models and Languages International Workshop on Mobile Computing Middleware International Conference on Coordination Models and Languages International Conference on Fundamental Approaches to Software Engineering International Workshop on Abstract State Machines International Workshop on Software Engineering for Large-Scale Multi-Agent Systems International Workshop on Foundations of Coordination Languages and Software Architectures International Conference on Service Oriented Computing


Research Quality and Impact : Research Quality and Impact Journals and Conferences in which we publish (continued): Annual Network and Distributed System Security Symposium European Conference on Object-Oriented Programming Communication Networks and Distributed Systems Modeling and Simulation Conference ACM Multimedia IEEE International Conference on Mobile and Wireless Communications Networks ACM/IEEE/IFIP Workshop on Embedded Systems for Real-Time Multimedia IEEE Design and Test, Special Issue on Mobile Multimedia International Symposium on Distributed Objects and Applications Journal of High Speed Networks IEEE Real-Time Systems Symposium IEEE International Conference on High Performance Distributed Computing International Conference on Distributed Computing Systems


Strong Research Interactions : Strong Research Interactions


External Collaborations : External Collaborations DoD Naval Research Labs NSA Rome Labs Industry SRI International Hewlett-Packard Company IBM Corporation (T.J. Watson Research Center) Microsoft Ford Academia Universidad Complutense de Madrid Universidad de Málaga Université Paris-Sud Universitat Politècnica de València University of Virginia University of Bolognia, Italy University of California, San Diego Universitat de Girona, Spain Instituto Tecnologico Autonomode Mexico (ITAM)


Educational Impact : Educational Impact Students supported: 37 Postdocs/Research Faculty supported: 6 PhD’s transitioned to Tenure-Track: Christine Julien -> University of Texas at Austin Prasanna Thati -> Simon Fraser University Miguel Palomino -> Universidad Complutense de Madrid PhD’s transitioned to Research Labs: Qingfeng Huang -> PARC


Educational Impact : Educational Impact CONTESSA related courses: Marktoberdorf Lectures Pisa Program Verification Course UIUC Course on Program Verification UIUC Course on Topics in Automated Deduction UIUC Course on Distributed Systems Summer School on Software Security: Theory to Practice UPenn and UIUC Courses on Advanced Topics in Security UCI Course on Distributed Systems Middleware UCI Course on Multimedia Systems and Applications UCI Seminar Course on Systems Support for Sensor Networks


DoD Impact : DoD Impact Supporting the network-centric vision MSR execution environment for NRL Use of Maude for security protocol analysis at NSA Use of Maude for sensor networks at Rome Labs Relevance of secure group communication for dynamic coalitions Secure networking protocols enhancing IPsec DoS counter-measures aid defense for information warfare Sensor and embedded systems networks


Industry and DoD Endorsements : Industry and DoD Endorsements Microsoft IBM Lucent Ford SRI International Metanetworks Rome Labs


Transferable Technologies : Transferable Technologies Models: TLAM Russian Dolls Context UNITY Shared Channel Model Real-Time Rewrite Theories Probabilistic Rewriting Theories Abstraction Models


Transferable Technologies : Transferable Technologies Specifications: L3A Protocol Stack Sectrace Spread, Cliques, and Secure Spread Adaptive Group Communication DoS-resistant TCP/IP Executable Semantics of Java, JVM, ML Security Protocol Specifications for MSR Tool Case Studies for other Maude-based Tools QoS Brokerage Service


Transferable Technologies : Transferable Technologies Middleware L3A WSEmail Egospaces Limone Agilla Service Extensions of LIME/Limone Compose-Q extensions CRCF Communications Framework MapGrid AutoSec Dynamo


Transferable Technologies : Transferable Technologies Formal Analysis Tools Maude ITP Maude LTL Model Checker Sufficient Completeness Tool Termination Tool Predicate Abstraction Tool Real-Time Maude and PMaude Markov Chain Model Checker Statistical TL Tool for Probabilistic Systems Open Calculus of Constructions (OCC) MSR Execution Environment Tool for TL-Based Runtime Verification and Monitoring Java Formal Analyzer (JavaFAN)


What are we positioned to do in the next two years ? : What are we positioned to do in the next two years ? Design methodology based on our modeling and analysis techniques to develop new interoperable middleware Develop new modeling and analysis techniques to support critical interoperability areas


Design Methodology for Interoperable Middleware (I) : Design Methodology for Interoperable Middleware (I) Security negotiation in middleware Long-lived applications over ad hoc networks Programmability of context-aware mobile applications Predictable sensor-based applications QoS interoperability across heterogeneous wireless technologies


Design Methodology for Interoperable Middleware (II) : Design Methodology for Interoperable Middleware (II) Web service framework for integrated messaging, data, and workflow Composable network protocols Larger system demonstrations on challenge problems


Modeling and Analysis of Critical Interoperability Areas : Modeling and Analysis of Critical Interoperability Areas Composable DoS countermeasures Tunnel calculus to aid reasoning about tunnel configuration protocols Models for QoS interoperability New methods for security and network protocol verification Languages for provably secure mobile programming


Modeling and Analysis (I) : Modeling and Analysis (I) Probabilistic System Modeling and Analysis Methods and Tools Mature version of PMaude and statistical analysis tools for TL properties Models of wireless communication security Availability, performance, and QoS Models Probabilistic extensions of Dolev-Yao Protection against traffic analysis


Modeling and Analysis (II) : Modeling and Analysis (II) Parallel Version of Maude high-performance analysis interoperability of specification and Code in a distributed setting anytime execution of designs/implementations Implementation of Mobile Maude security and verification of mobile code


Today’s Talks: Combining CONTESSA Technologies to Tackle Challenging Applications : Today’s Talks: Combining CONTESSA Technologies to Tackle Challenging Applications DoS Resistant Secure Communication in Heterogeneous Networks Adaptive and Context-Aware Secure Communication in Mobile Environments Probabilistic Formal Models Formal Prototyping & Analysis DoS Resistant Protocols DoS Resistant Secure Tunnels Mobility & Context-Awareness Formal Prototyping & Analysis Power-Awareness Adaptive Reflective Middleware


Today’s Agenda : Today’s Agenda


CONTESSA : CONTESSA Closing Presentation UMBC Review Meeting, November 19, 2004 José Meseguer University of Illinois at Urbana-Champaign


Research Challenges : Research Challenges Adaptation & Interoperation Trends Internet Nomadic Ad Hoc Sensor Standalone Heterogeneous Systems Systems of Systems 3 years 2 years Models & Analysis Middle- ware Support Crosscutting Concerns: Security Reliability Rapid Development


Methodology : Methodology Requirements Formal Executable Specifications Code Formal Analysis Formal Analysis Rewriting Logic Analysis Results


Enabling Technologies : Enabling Technologies Mobile Agents Adaptive Middleware Composable Network Protocols Applications Middleware Services Network Infrastructure


What can we do what we could not do three years ago ? : What can we do what we could not do three years ago ? DoS countermeasures and formal analysis Logical simulation and analysis of network potocols Probabilistic models and analysis of large distributed systems Reasoning about adaptive communication Adaptive middleware services for mobile and sensor systems


Project Metrics : Project Metrics Research Output, Quality, and Impact Strong Research Interactions Educational Impact DoD and Industry Relevance Transferable Technologies


Today’s Talks: Combining CONTESSA Technologies to Tackle Challenging Applications : Today’s Talks: Combining CONTESSA Technologies to Tackle Challenging Applications DoS Resistant Secure Communication in Heterogeneous Networks Adaptive and Context-Aware Secure Communication in Mobile Environments Probabilistic Formal Models Formal Prototyping & Analysis DoS Resistant Protocols DoS Resistant Secure Tunnels Mobility & Context-Awareness Formal Prototyping & Analysis Power-Awareness Adaptive Reflective Middleware


What are we positioned to do in the next two years ? : What are we positioned to do in the next two years ? Design methodology based on our modeling and analysis techniques to develop new interoperable middleware Develop new modeling and analysis techniques to support critical interoperability areas


CONTESSA Web Page: formal.cs.uiuc.edu/contessa : CONTESSA Web Page: formal.cs.uiuc.edu/contessa