论文标题
具有主动欺骗和时间逻辑规格的安全性逐个合成网络
Secure-by-synthesis network with active deception and temporal logic specifications
论文作者
论文摘要
本文涉及具有主动网络欺骗的网络系统中策略的综合。网络中的主动欺骗采用诱饵系统和其他防御措施来进行防御计划,以防止通过传感系统确认的恶意攻击者的入侵。在这种情况下,辩护人的目标是确保对时间逻辑公式中指定的安全属性的满意度。我们用诱饵系统和其他防御措施制定了欺骗性计划的问题,作为两人游戏,具有不对称信息,并以时间逻辑为单位。我们使用具有时间逻辑目标的Level-2 Hypergame来捕获攻击者对网络系统的不完整/错误知识,以作为回报误解。真正的回报功能是防御者的私人信息。然后,我们扩展了$ Omega $ regardar游戏的解决方案概念,以分析攻击者的理性策略,因为她的信息不完整。通过以正常形式将级别2超级游戏的解决方案推广到广泛的形式,我们将具有安全的时间逻辑目标的游戏解决方案扩展,以确定防御者是否可以确保对概率的安全属性满意,鉴于攻击者认为是合理的策略。此外,我们使用具有共同安全性(可及性)时间逻辑目标的游戏解决方案,以确定防守者是否可以通过将攻击者引导到高保真蜜罐来吸引攻击者。用蜜罐的合成网络系统说明了所提出的合成方法的有效性。
This paper is concerned with the synthesis of strategies in network systems with active cyber deception. Active deception in a network employs decoy systems and other defenses to conduct defensive planning against the intrusion of malicious attackers who have been confirmed by sensing systems. In this setting, the defender's objective is to ensure the satisfaction of security properties specified in temporal logic formulas. We formulate the problem of deceptive planning with decoy systems and other defenses as a two-player games with asymmetrical information and Boolean payoffs in temporal logic. We use level-2 hypergame with temporal logic objectives to capture the incomplete/incorrect knowledge of the attacker about the network system as a payoff misperception. The true payoff function is private information of the defender. Then, we extend the solution concepts of $omega$-regular games to analyze the attacker's rational strategy given her incomplete information. By generalizing the solution of level-2 hypergame in the normal form to extensive form, we extend the solutions of games with safe temporal logic objectives to decide whether the defender can ensure security properties to be satisfied with probability one, given any possible strategy that is perceived to be rational by the attacker. Further, we use the solution of games with co-safe (reachability) temporal logic objectives to determine whether the defender can engage the attacker, by directing the attacker to a high-fidelity honeypot. The effectiveness of the proposed synthesis methods is illustrated with synthetic network systems with honeypots.