Model Checking Grid Security

Grid computing is one of the leading forms of high performance computing. Security in the grid environment is a challenging issue that can be characterized as a complex system involving many subtleties that may lead designers into error. This is similar to what happens with security protocols where automatic verification techniques (specially model checking) have been proved to be very useful at design time. This paper proposes a formal verification methodology based on model checking that can be applied to host security verification for grid systems. The proposed methodology must take into account that a grid system can be described as a parameterized model, and security requirements can be described as hyperproperties. Unfortunately, both parameterized model checking and hyperproperty verification are, in general, undecidable. However, it has been proved that this problem becomes decidable when jobs have some regularities in their organization. Therefore, this paper presents a verification methodology that reduces a given grid system model to a model to which it is possible to apply a ‘‘cutoff’’ theorem (i.e., a requirement is satisfied by a system with an arbitrary number of jobs if and only if it is satisfied by a system with a finite number of jobs up to a cutoff size). This methodology is supported by a set of theorems, whose proofs are presented in this paper. The methodology is explained by means of a case study: the Condor system.