Formal Verification of the Race Condition Vulnerability in Ladder Programs

Ladder diagram is a widely used language for programming PLCs (Programmable Logic Controllers). The presence of a vulnerability in these programs and its exploitation by an attacker can have drastic consequences. The vulnerability of Race Condition is one of the most critical vulnerabilities in Ladder programs. The behavior of Ladder program with Race Condition is unpredictable and potentially dangerous. In this paper, we propose the formal modeling of this vulnerability allowing its detection by model checking. Concretely, our approach consists in translating the Ladder programs into a network of timed automata. The Race Condition vulnerability is then modeled as a CTL (Computational Tree Logic) property and the UPPAAL model checker is applied to verify the presence of Race Condition in those Ladder programs by verifying that CTL property. Contrary to other approaches proposed in the literature, our solution allows the Race Condition detection in all its forms and thus reinforces the robustness of Ladder programs against this type of attack.