ABSTRACT

This research aims to develop a logic-based framework for proof-carrying survivability: a system user publishes their survivability requirements, a system provider compiles and submits a proof-carrying code, and finally the user applies a simple and fast program to verify the proof.  If the proof is validated, all the requirements are guaranteed to be satisfied.  By shifting the responsibilities of the survivability proof from a user to a system provider, the user only needs a lightweight checker to verify that a system possesses a set of safety and security properties for system survivability. Any system that does not meet the user’s requirements will be detected before the system is deployed, thus avoiding a situation where the user has to fix problems and recover the system after damages have already been caused.

Our work included two main thrusts.  First, we developed the necessary approaches and algorithms for the user to quantify system survivability.  Attack modeling and impact quantification allow the user to identify the critical system properties necessary for a system to survive malicious attacks.  The survivability requirements are specified based on the qualitative analysis of system properties and modeling of attacks. We studied the inherent survivability properties of critical information systems in general and the distributed enterprise RFID system in particular.

In the second thrust, we developed the logic constructs for survivability proof-carrying.  An application-specific logic was designed with sound formal properties.  In particular, the logic framework facilitates constrained reasoning -- possibilistic uncertainty and survivability requirement constraints are effectively linked to a logical reasoning process.  The framework makes it possible to express fuzzy pattern matching and arbitrary user-defined constraints in formal proofs.