Formal specification and verification of resource bound security using PVS

Resource usage abuse is a major security concern for computer systems that run programs uploaded from other computers. In the absence of any guarantee on resource usage bounds, we cannot have any confidence that the external codes have been supplied by trustworthy computers or the codes have not been tempered with by a third party. In a previous report [1], we described the TINMAN security architecture and a tool set for enforcing resource safety of external C code. In this paper, we detail the formalization of resource specification and verification of the resource safety properties. This formal framework is based on an extended Hoare logic with resource usage variables. We formalize the construct (tasks) and resource safety assertions (resource specifications) in a proof system that is built on the PVS theorem prover. We also discuss the proof strategies for different types of resource usage verification tasks that are important for the mechanization of TINMAN.