A Logical Framework of Proof-Carrying Survivability

Users often need to acquire external software systems or link other software components to their existing systems. It is crucial that those software objects are trustworthy and will not compromise the survivability of the existing systems, particularly for those systems used to support mission-critical services in national defense, healthcare, and financial services. This paper presents a logical framework for proof-carrying survivability: (1) a system user publishes their survivability requirement policy for the system in which they are interested, (2) a system provider collects verification evidence from third-party evaluators, formulates survivability compliance, and compiles a proof to show that their system satisfies the user´s requirements, and finally, (3) the system user verifies that the proof is valid. If so, the system can be safely acquired or linked without sacrificing the survivability of the existing system. We specify an application specific logic to facilitate proof compliance and verification. We implemented the framework to show that the proof can be generated automatically by a prover program and verified mechanically in real time by a trustworthy checker program.