Proof-Carrying Survivability
Yanjun Zuo · 2013
Abstract : The objective of this project was to develop a logic-based framework for proof-carrying survivability: a user publishes his/her survivability requirement policy; a system provider constructs a proof to show that the system satisfies the user s requirements; and the user verifies if the proof is valid. We have developed techniques that enable users to specify measureable and certifiable survivability requirements and represent their survivability policy. From the perspective of system acquisition and engineering, developing a survivability requirement is the important first step in survivability specification, compliance formulation, and proof verification. An important part of the project is a logic model for survivability requirement representation, compliance proof construction, and user verification. We have developed various techniques for proof evidence search, proof derivation, and proof code checking. Moreover, the logic model facilitates constrained reasoning, i.e., possibilistic uncertainty and survivability requirement constraints are effectively linked to logical reasoning.