There is an increasing need to study the vulnerability of communication protocols in distributed systems to malicious attacks that attempt to violate properties such as safety or liveness. In this paper, we propose a common methodology for formal synthesis of successful attacks against two well-known protocols, the Alternating Bit Protocol (ABP) and the Transmission Control Protocol (TCP), where the attacker can always eventually win, called For-all attacks. This generalizes previous work on the synthesis of There-exists attacks for TCP, where the attacker can sometimes win. We model the ABP and TCP protocols and system architecture by finite-state automata and employ the supervisory control theory of discrete event systems to pose and solve the synthesis of For-all attacks, where the attacker has partial observability and controllability of the system events. We consider several scenarios of person-in-themiddle attacks against ABP and TCP and present the results of attack synthesis using our methodology for each case.
翻译:越来越需要研究分布式系统中通信协议在恶意攻击中的脆弱性,这些恶意攻击企图侵犯安全或生活等财产。在本文件中,我们提出一种共同方法,正式综合对两个众所周知的议定书,即《交替比特议定书》和《传输控制议定书》的袭击,攻击者最终总能赢,称为 " 万能攻击 " 。这概括了以前为TCP综合 " 现场攻击(攻击者有时能赢)的工作。我们用有限状态自动数据模拟 " ABP " 和 " TCP " 协议和系统结构,并采用独立事件系统的监督控制理论,在攻击者对系统事件有部分可视性和可控性的情况下,提出和解决 " 万能攻击者 " 袭击的综合。我们考虑了针对ABP和TCP的几起人中攻击情景,并用我们的方法对每个案件介绍攻击综合的结果。