Modeling vulnerabilities in cyber-physical spaces

Abstract

There is continuing growth in the need to secure critical infrastructures from malicious adversaries. These adversaries can attack systems from different forms. They can physically break in and steal something important, or they can attack from the cyber realm in order to steal critical information. This project combines the modeling process for physical spaces along with a logic reasoning tool that can identify the state of a networked device in order to analyze large enterprise systems for combined cyber-physical vulnerabilities. Using a pure model checker would not be able to handle the near infinite states that a computer or networked device may be in. Therefore this new approach combines the use of a logic analyzer tool that with a well-defined set of rules that reasons about the security and trustworthiness of devices in the model. While there has been long study of how to secure a building from intrusion, and much research about defense against cyber attacks, there is always a large gap between the two in practice. This approach may no longer be sufficient against today’s adversaries and offers little to no defense against insider threats. Combining the two in this new form allows for a more complete security view and protection against more advanced adversaries. Then this thesis shows how this approach meets a series of requirements for an effective vulnerability analysis. This is achieved by executing a model based on a real world facility with a series of induced faults that would on their own not be enough to be a vulnerability but tied together would have series consequences. This thesis shows how this approach can then be used to detail potentially unseen vulnerabilities and develop fixes for them to help create a more secure facility.