MURI Project

(1) Develop a method of attacks and a language for describing attack behavior, similar to the models of naturally occurring faults that have been developed to drive the development of fault-tolerant systems. The model underlying the atack language is the capabilities afforded an attacker due to successful attack behavior and the impact of an attack on system resources, including the resources associated with the protocols developed under the Protocol Engineering Research Center (PERC). Through the attack language, attacks can be composed to define multi-stage attacks, where the composition involves temporal and spatial dimensions. An ontological approach will be taken, wherein vulnerabilities, system resources, and attacks will be formally specified using the Cyc reasoning system. An outcome of this tasks will be a taxonomy of vulnerabilities and attacks, in addition to the attack description language.

(2) Develop a language in which security policies can be stated. Having such a language will permit the formulation of security policies. Such policies will be concerned with resources of a system that could be impacted by attacks, the attacks occurring on the computational resources in support of a mission, in support of infrastructure that executes the protocols the PERC is developing, or in support of security-enhancing features. The language will allow two kinds of policies to be specified: (1) access control, which declare resources that are to be unavailable to users, and (2) quality of service, which declare the availability of resources to tasks. In both cases, the policies are to be specified as a function of the state of the system, the state being concerned with the status of components due to naturally occurring faults or attacks.

(3) Develop tools to support the reasoning about policies, including (1) consistency, (2) completeness, and the projection of policies to enforcement sites. Regarding (1) and (2), this kind of reasoning is undecidable but we will investigate heuristics to perform incomplete but effective reasoning. Regarding (3), a policy must be mapped down to components that can enforce that policy, including components in support of attack detection, reconfiguration, and recovery; some of these components will be developed by other participants in the PERC team. We will assume responsibility for the attack detection components. Our approach will involve planning, some of which will occur off-line, but the impossibility of planning for all attacks and faults will necessitate that any offline plan be tuned in real time. One aspect of our projection effort is a cost model, that reflects the importance of resources to tasks, so that the planning process provides minimal impact to mission-critical tasks.

(4) Develop a verification system to support the formal reasoning of protocols. Recognizing that protocols are best represented as distributed processes, the verification system will support the reasoning about distributed processes, where both safety and liveness properties are relevant. To reflect the quality-of-service requirements of PERC protocols, the reasoning system will allow reasoning about real time properties. We will build on existing UC Davis work on the verification of real time programs and the formal modeling of schedulers for real time systems. The verification system will be mechanized either in the Cambridge HOL system or in SRI International's PVS system, both of which have been used by UC Davis.

(5) To support the testing of protocols, we will develop a tester's assistant (TA). Through the TA, a user provides specifications of a protocol (or its implementation), the specifications serving to drive the testing process in two ways: (1) as oracles, against which the protocol's behavior with test data is evaluated, and (2) as slicing criteria against which critical parts of the protocol are extracted. Through slicing, components of the protocol relevant to the specifications are identified and tested more easily than the entire protocol.