V.A. Desnitsky - Research Scientist, St. Petersburg Institute for Informatics and Automation of the Russian Academy of Sciences (SPIIRAS). E-mail: desnitsky@comsec.spb.ru
I.V. Kotenko - Research Scientist, St. Petersburg Institute for Informatics and Automation of the Russian Academy of Sciences (SPIIRAS). E-mail: ivkote@comsec.spb.ru
A.A. Chechulin - Head of Laboratory, St. Petersburg Institute for Informatics and Automation of the Russian Academy of Sciences (SPIIRAS). E-mail: chechulin@comsec.spb.ru

The presence of hardware resource constraints on embedded devices causes complexity of application of traditional cryptographic and other protection means used to provide security of personal computers and servers. Therefore security of information systems with embedded devices requires specific approaches to design security mechanisms providing resistance of the system to attacks not only through extra protection means, but at the expense of peculiarities of the architecture of the system. As a way to achieve this goal an analysis of information system with embedded devices at all design stages allows avoiding architectural defects lessening security level of the system. An important result of the work is a verification technique to check information flows. The goal of the technique is to evaluate security of the developed system with embedded devices, check correctness of the security policy and determine the level of accordance of information flows of the real system to the assigned policies. We applied model checking to verify security policy rules describing information flows by means of software tool SPIN. Such verification is related to the methods of static system analysis. Its fulfillment at initial stages of the system design provides earlier revelation of contradictions within the security policy as well as inconsistencies of the information system topology. In contrast to dynamic analysis comprising testing implemented devices on the basis of testing attack vectors the proposed verification approach allows lessening the amounts of actions to be conducted repeatedly after correction of detected design errors. We singled out one of the most important anomaly types, shadowing anomaly, which the verification is oriented to. A presence of this anomaly supposes the rule is never held due to a fact that there is one of a number of other rules overriding it. The anomaly witnesses a probable error in the policy, which should be revised. An advantage of the proposed verification is the possibility to ensure security of the system if the model behavior agreed with the real system one. The drawbacks includes a great volume of computational resources involved in analysis of complex models, false positive alarms (i.e. warnings about potential information flows that will not be in the real system) and incompleteness, since a model (not the real system) is checked.