Statistic complexity metrics as a basis for formal probabilistic model checking

Abstract

The paper proposes a new technique for detecting malware threats in autonomic component ensembles. The technique is based on the statistic
complexity metrics, which relates objects to random variables and (unlike other complexity measures considering objects as individual symbol
strings) are ensemble based. This transforms the classic problem of assessing the complexity of an object into the realm of statistics. The
proposed technique requires the implementation of the process X (which generates ‘healthy’ flows containing no malware threats) and objects
generated by the actual (possible infected) process Y. The component flows files are used as objects of the processes X and Y. The result of
the proposed procedure gives us the distribution of probabilities of malware infection among autonomic components. Quantitative verification
techniques are implemented within PRISM, a probabilistic model checker, which provides direct support for DTMCs, MDPs and CTMCs. The
distribution of malware threats probabilities, obtained by the above-described procedure serves as a starting point for formal reasoning about
the behavior of the Autonomic components ensembles.