Comprehensive Exam Presentation - Chibuzo Ukegbu

Chibuzo Ukegbu – Cyber Security

Zoom Link

Title: Programmable Logic Controller (PLC) Software Verification Approaches Using Block Encoding and Symbolic Methods

Abstract:

The objective of this synthesis paper is to review embedded software verification approaches with the intention of creating a domain-specific approach for Programmable Logic Controller (PLC) software verification. PLC control software, unlike other conventional software, runs in cycles and does not have observable intermediate states; its
observable state is at its output. In this scenario, to verify the software, the right modeling technique is to be adopted that correctly models and abstracts the state space and logically characterizes the semantics of the software for verification. Classical bounded-model checking encodes the program’s control flow automata in steps, and their
specification treats the PLC program as a single step by only considering the controller’s observable state at the end of the execution cycle. Bounded model checkers (BMCs) disassemble loops statically, thereby characterizing the control programs in shorter steps. This does not provide the correct verification and as such does not assure the safety
and security of PLC programs. Considering the safety-critical nature of PLC control programs and the consequences of unwanted behaviors in industrial control applications, this paper looks at various approaches to build a domain-specific verification tool that is tailored for the PLC control software and evaluates it with various other BMC tools to
measure the performance and identify the import of the differences. Symbolic execution, incremental solving, single block encoding, large block encoding, and dynamic large block encoding are the various techniques reviewed from which dynamic large block encoding-based-cycle-BMC is realized. The results reveal that the Efficient SMT-based
Bounded Model Checker (ESBMC)-INC is the closest BMC tool to DLBE-cycleBMC, whereas Symbiotic, a recent BMC tool, matches and performs better than the state-of-the-art DLBE-cycleBMC. Furthermore, the trajectory of research in this area focuses on the use of enhanced symbolic methods with other encoding algorithms to develop more
efficient verification tools that would take less time to identify the reachability or otherwise of unwanted behaviors in industrial control software systems.

Committee:

Dr. Hoda Mehrpouyan (Chair)
Dr. Nasir Eisty
Dr. Yantian Hou
Dr. Jidong Xiao (CompEE)