Formal Modeling And Analysis Of Mission-Critical Systems For Survivability

With the advent of information age, various mission-critical systems have been widely used, and once the basic services interrupt, an enormous impact will be imposed on the national economy and people' s living standards. Traditional security measures have improved system security, whereas kinds of invasions still occur. As a result, the ability of system to provide users with satisfied services after invasions must be taken into account. Survivability is the best way to deal with all attacks, incursions and destructions.Research on survivability focuses on how to ensure that systems can complete their critical missions in time under attacks, accidents or failures. Two domains are involved in this research: design and analysis of survivability. Among them, survivability analysis, especially the quantitative analysis is an important and fundamental work, focusing on how to assess system survivability. The objective is to provide a normal evaluating scheme, which can assess the current status of system survivability, forecast survivability' s trend in various environments, and further direct the design and realization of survivable system basically. At present, researches on survivability have made some progress, but there is still no uniform analyzing criterion and the research achievements have not taken practical feasibility into account. Aiming at this, survivability analysis is taken as the core, and the modeling and analyzing methods for system survivability are studied deeply in this dissertation.Firstly, index system model of survivability based on composite attribute is studied. Performance metrics of survivability are comprehensively summarized from the following three perspectives: index content, attack phases and evaluating standard. Then a framework for index system which can present survivability is proposed and formalized, furtherly the corresponding mathematical model are abstracted. On the basis, simplification and extension of the index system in various application backgrounds are discussed. Combined with an instance, index system is illuminated in uncertain AHP-Fuzzy survivability evaluation, which provides reasonable evidence for system survivability analysis.Secondly, formal modeling method of system survivability based on performance evaluation process algebra is studied. By analyzing the essential characters affecting survivability, service request and server, intruder and server are described as different components. Namely survivability model which accurately depicts system behaviors and properties is constructed from perspectives of users' service requests and attack impact respectively, and then similarities and differences are compared. Sensitivity analysis for model parameters is performed to make the constructed model perfect. Performance analysis resuluts show that the model can reflect key attributes of system survivability exactly, on the basis of which to achieve specific survivability analysis.Thirdly, quantitative analysis method of system survivability based on probabilistic model checking is studied. Graph theory analysis is combined with numerical solution, statistics and simulation technology. Oriented at the CTMC system probabilistic model with stochastic actions, then formal specification of survivability is identified by continuous stochastic logic according to different disasters degree and service levels. Ultimately, Prism, the probabilistic model checking tool, is used to do statistics and analysis, and automated analysis results are plotted as graphs. Simulation experiment results verify the reasonability and validity of this method in quantitative analysis for survivability, which helps to realize the real-time monitoring for system survivability under different environments.Finally, forecasting method of system survivability based on Sequential Monte Carlo is studied. A dynamic model of system is founded and employed to acquire prior PDF of survivability at current time, and then Bayesian formula is used to update the prior PDF on the basis of observed data and measurement model. Samples with associated weights are used to approximate posterior probability density distribution of survivability in order to forecast survivability at the next moment. Simulation experiment results show that SMC has a higher forecasting precision, and exibit dynamic development trend of system survivability from several time sequences, which changes survivability management from passiveness to initiative.