Synthesis of information security system by means of smt-solvers

The problem of synthesis of information security system for automated systems in general, is reduced to the optimal choice of such measures of protection that would ensure the functioning of the system at the minimum acceptable risks in terms of the existence of certain threats. Depending on the requirements for the automated system and the nature of its work, the tasks of synthesis would increase. For example, the concept of optimality of information security system can mean maximum efficiency of such system with minimal operation and maintenance, and the extent of its impact on the operation of the automated system. Another reason for the complexity of the problem is the possibility of varying the components which protect automated system. Finally, the main difficulty lies in the formalization of the list of threats and risk values, which can be dependent on various factors. The article examines an original approach to solving the task of information security system’s synthesis in the automated system. The authors propose the method for encoding the initial problem into a formalized one for a SMT solver. The method represents the characteristics of the security measures in the form of functions. The formula corresponding to the original problem is given in UFLRA theory language. The interpretation process of SMT solver’s results is given. Shortcomings of the proposed method are outlined.