Composable Formal Models
for
High-Assurance Fault Tolerant Networks
Investigators
Objective
Current network systems are highly vulnerable to attacks. They are
typically not capable of self-recovery, and even if they can recover they
remain vulnerable to the same attacks in the future. A number of promising
techniques and experimental systems are aimed at monitoring, diagnosing, and
countering network attacks. The very ideas of self-monitoring,
self-diagnosing, and self-repairing are intrinsically reflective; that is,
they involve a system having the capacity to represent some aspects of
itself and its environment and to use this to adapt its behavior to changing
situations. Most existing systems exhibit some implicitly reflective
features, but they lack systematic methods and techniques for taking
advantage of the power of reflection. Furthermore, there is a lack of
formal models for these systems. Having such formal models is key to
gaining high assurance for this critical infrastructure.
The project will develop a formal reflective framework for network recovery
and reconstitution (R and R) and will use this framework to facilitate the
use of formal models and analysis in the design of R and R systems in
collaboration with other teams in the Fault Tolerant Networks (FTN) program.
Besides providing higher assurance for such systems, we expect the proposed
work to have the following additional benefits\:
- a new reflective methodology for designing high-assurance
R and R services for network systems, and
- new compositional formal analysis and proof techniques for such services.
Approach
The project will build on our expertise in formal modeling of reflective
object-based distributed systems, and on our experience in applying formal
methods to the design and analysis of Active Network systems.
The aspects of the appoach include:
- A formal reflective framework for network R and R that is distributed,
adaptive, and based on executable models of the underlying network system,
faults and attacks, R and R services, and their reflective interoperation;
- A family of compositional formal methods especially tailored for
analysis and verification of R and R services, including symbolic
simulation, model checking, and rigorous mathematical or mechanically
assisted proof;
- An implementation of the Mobile Maude language supporting distributed
simulation, prototyping, and implementation of high-assurance R and R
services, including their dynamic deployment.
An important aspect of the effort will involve case studies in collaboration
with other teams in the FTN program. These collaborations will give us a
rich conceptual testbed with which to develop the proposed formal reflective
framework, models, tools and analysis techniques, and will enable higher
assurance in the design of FTN systems by other research teams.