Analyzing network management effects with spin and ctla

Abstract

Since many security incidents of networked computing infrastructures arise from inadequate technical management actions, we aim at a method supporting the formal analysis of those implications which administration activities rnay have towards system security. We apply the specification language cTLA which supports the modular description ofprocess systems and facilitates the construction of a modeling framework. The framework defines a generic modeling structure and provides re-usable model elements. Due to cTLA's connection to the temporal logic of actions TLA, formal analysis can resort to symbolic reasoning. Supplementarily, automated analysis can be applied. We focus here on automated analysis. It is supported by translation of cTLA specifications into suitable model descriptions for the powernd model checking tool SPIN. We outline the utilized methods and tools, and report on the modeling and SPIN-based analysis of IP-Hijacking. © 2004 by Springer Science+Business Media Dordrecht.