Stages de la spécialité SAR: Use of formal methods to improve monitoring strategies

Introduction

This stage takes place within a collaboration between Université P. & M. Curie and Rutgers University. This will be joint work with a student from each institution. Interaction over the Atlantic is expected ;-).

Rutgers University With more than 50,000 students, Rutgers, The State University of New Jersey, is one of the US major state university. Chartered in 1766, as Queens’ College, Rutgers is the eights institution of higher education to be founded in America before the IndependenceWar. The Department of Computer Science offers Bachelors’, Master and Ph.D. degrees in Computer Science, with emphasis in distributed systems, mobile networking, compilers, theoretical computer science, computer vision and bioinformatics. The Distributed Computing (Disco) Laboratory was created in 1998 to conduct research on network-centric computing, particularly in remote healing systems and outdoor distributed computing. Supported by National Science Foundation grants, Disco Lab groups ten Ph.D. students, several visiting students and a couple of undergraduate students each year, under the supervision of Liviu Iftode, Associate Professor of Computer Science at Rutgers and Head of the Disco Lab. More information about Disco Lab can be found at http://discolab.rutgers.edu.

Université P. & M. Curie (LIP6-SRC) Research of the SRC group focuses on systems made of interacting components. This includes :
- system design within the context of international standards such as the "Open Distributed Processing Reference Model" (RM-ODP)
- design and implementation of verification tools to increase reliability
- computer aided system deployment and implementation
- Design and implementation of reconfigurable platforms based on virtual machines
- design and implementation of enhanced services such as fault tolerance of migration

The SRC group actively participates in normalization committees such as OMG (Object management Group) or ISO. Numerous research centers are using the tools we developed for the verification of distributed application and algorithms by means of Petri Nets [3].

Context

Monitoring and maintenance of computer systems is not only prohibitively expensive, but is unacceptably slow due to the complexity of software systems today. Even with a large and expensive workforce, human administrators cannot respond effectively to the monitoring and management requirements due to the speed of failure and attack propagation, the number of failure incidences, and the increasing sophistication of attacks on the infrastructure. The ultimate goal of our current research is to develop highly-effective self-defending computer systems that can perform automated monitoring, detection, diagnosis and repair actions on themselves or on other cooperating systems.

The basic block of the envisaged defensive architecture is the programmable backdoor [2, 3]. In our approach, a backdoor is a trusted piece of hardware or a software mechanism that can be programmed to execute defensive activities on the memory of a computer system, such as monitoring, identification and enforcement of invariants, and repairing when these invariants are violated. A backdoor can execute defensive tasks standalone or in cooperation with other backdoors [1]. The challenge is to express the properties to be monitored and the actions to be taken in a rigorous way in order to guarantee their effectiveness.

Work to be done

The objective of this stage is to evaluate the potential of using formal methods to define monitoring and repairing actions, which can be executed automatically in the backdoor of a computer system.

To achieve this goal, the system would have to be formally specified using Petri Nets [4]. As shown in Figure 1, the specification should be divided in two parts :
- the system, it does not describe the system itself but expected relationships between the parameters to be checked regularly by the monitor (e.g. to detect a problem such as a potential attack of the system),
- the monitor, that detects unexpected relationships between parameters and triggers an alert as soon as some unexpected event is discovered. Alerts are typed (emergency priority, type of potential failure or attack, new strange behavior, etc.)


FIG. 1 - Structure of the specification.

Once the specification is elaborated, some relationship of the specification should be changed (or deleted) in order to evaluate new potential behavior and check if the monitor detect new classes of potential problems.

Main milestones of the work should be :

- 1. acquisition of the context and identification of the parameters to be modeled (as well as their relationship)
- 2. specification of the system as presented in Figure 1.
- 3. verification of the model to evaluate if it is accurate (the use of CPN-AMI[5] is recommended) ; a priori, this should mostly consists in reachability analysis (using structural methods or model checking),
- 4. perturbation of the model in order to evaluate the monitor’s behavior in the presence of variations,
- 5. correction of the model to improve monitoring in the presence of variations,
- 6. implementation and evaluation of the model using the backdoor.

Steps 4 to 6 should be repeated several times and a procedure should be defined from the know-how acquired during this experience. The main idea is to have a semiautomated cycle to help monitor designers in building more efficient monitors.

Based on the results, this work may continue as a PhD.


Mot-clé: SAR hors ATIAM, recherche
Responsable:

- Fabrice Kordon (UPMC) - 01 44 27 88 20 - Fabrice.Kordon@lip6.fr
- Liviu Iftode (Rutgers) - iftode@cs.rutgers.edu


Organisme:
site web de SRC

Lieu:

LIP6-SRC)


Dates:
du 3/4/2006 au 30/09/2006

Bibliographie:

[1] Baliga A., Bohra A., and Iftode L. Orion : Looking for constellations in physi- cal memory. In Rutgers University, Department of Computer Science Technical Report, 2005.

[2] Aniruddha Bohra, Iulian Neamtiu, Pascal Gallard, Florin Sultan, and Liviu Iftode. Remote repair of operating system state using backdoors. In ICAC, pages 256-263. IEEE Computer Society, 2004.

[3] Sultan F., Bohra A., Pan Y. Smaldone S. and, Gallard P., Neamtiu I., , and Iftode L. Ieee internet computing. 2005.

[4] C. Girault and R. Valk. Petri Nets for Systems Engineering. Springer Verlag, 2003.

[5] LIP6-SRC. The Mars project homepage, http://www.lip6.fr/mars, 2002.





logo-spip E. Saint-James & F. Kordon - Master Informatique - UPMC Valid XHTML 1.0!
Calculé le 20 octobre 2018 à 20h01min