Engineering topics

Etigowni, Sriharsha

Publications and source records attributed to Etigowni, Sriharsha.

3 records

DOE OSTI2024

Formally Verified ZTA Requirements for OT/ICS Environments with Isabelle/HOL

The clean energy transformation includes the integration of distributed energy resources with the power grid, which has led to a substantial increase in the complexity of power grids infrastructure and the underlying operational technology environment. Power grids infrastructure represents an operational technology environment that has become a system of systems, integrating heterogeneous devices which are both software-and hardware-intensive; as a result, there are increasing demands to exploit advances in the commodity of software-hardware infrastructures to improve energy systems requirements such as cybersecurity and resilience. In such a setting, system requirements at different levels mix, which leads to vulnerabilities and undesirable outcomes. The use of formal methods to characterize and prove system requirements removes ambiguity, increases automation, and provides high levels of assurance and reliability. In this paper, we contribute a methodology and a framework for the system-level verification of zero trust architecture requirements in operational technology environments. We define a formal specification for the core functionalities of operational technology environments, the corresponding invariants, and security proofs. Of particular note is our modular approach for the formal verification of asynchronous interactions in operational technology environments. The formal specification and the proofs have been mechanized using the interactive theorem proving environment Isabelle/HOL.

formal methods↗

DOE OSTI2023

Formally Verified ZTA Requirements for OT/ICS Environments with Isabelle/HOL: Preprint

The clean energy transformation led to the integration of distributed energy resources on a top of the grid, and so a substantial increase in the complexity of power grids infrastructure and the underlying operational technology environment. Operational technology environments are becoming a system of systems, integrating heterogeneous devices which are software/hardware intensive, have ever increasing demands to exploit advances in commodity of software/hardware infrastructures, and this for good reasons - improving energy systems requirements such as cybersecurity and resilience. In such a setting, system requirements at different levels mix, thus undesirable outcomes will surely happen. The use of formal methods will remove ambiguity, increase automation and provide high levels of assurance and reliability. In this paper, we contribute a methodology and a framework for the system level verification of zero trust architecture requirements in operational technology environments. We define a formal specification for the core functionalities of operational technology environments, the corresponding invariants, and security proofs. Of particular note is our modular approach for the formal verification of asynchronous interactions in operational technology environments. The formal specification and the proofs have been mechanized using the interactive theorem proving environment Isabelle/HOL.

formal methods↗

DOE OSTI2021

Strategy for distributed controller defence: Leveraging controller roles and control support groups to maintain or regain control in cyber-adversarial power systems

Distributed controllers play a prominent role in electric power grid operation. The coordinated failure or malfunction of these controllers is a serious threat, where the resulting mechanisms and consequences are not yet well-known and planned against. If certain controllers are maliciously compromised by an adversary, they can be manipulated to drive the system to an unsafe state. The authors present a strategy for distributed controller defence (SDCD) for improved grid tolerance under conditions of distributed controller compromise. The work of the authors’ first formalises the roles that distributed controllers play and their control support groups using controllability analysis techniques. With these formally defined roles and groups, the authors then present defence strategies for maintaining or regaining system control during such an attack. A general control response framework is presented here for the compromise or failure of distributed controllers using the remaining, operational set. The SDCD approach is successfully demonstrated with a 7-bus system and the IEEE 118-bus system for single and coordinated distributed controller compromise; the results indicate that SDCD is able to significantly reduce system stress and mitigate compromise consequences.

97 MATHEMATICS AND COMPUTING↗