Towards Provable Security in Industrial Control Systems Via Dynamic Protocol Attestation
- URL: http://arxiv.org/abs/2412.14467v1
- Date: Thu, 19 Dec 2024 02:28:35 GMT
- Title: Towards Provable Security in Industrial Control Systems Via Dynamic Protocol Attestation
- Authors: Arthur Amorim, Trevor Kann, Max Taylor, Lance Joneckis,
- Abstract summary: Cyber attackers can infiltrate industrial control systems (ICSs) and execute malicious actions.
These attacks have resulted in dramatic consequences such as physical damage, economic loss, and environmental catastrophes.
This paper introduces a methodology that restricts actions using protocols.
- Score: 0.0
- License:
- Abstract: Industrial control systems (ICSs) increasingly rely on digital technologies vulnerable to cyber attacks. Cyber attackers can infiltrate ICSs and execute malicious actions. Individually, each action seems innocuous. But taken together, they cause the system to enter an unsafe state. These attacks have resulted in dramatic consequences such as physical damage, economic loss, and environmental catastrophes. This paper introduces a methodology that restricts actions using protocols. These protocols only allow safe actions to execute. Protocols are written in a domain specific language we have embedded in an interactive theorem prover (ITP). The ITP enables formal, machine-checked proofs to ensure protocols maintain safety properties. We use dynamic attestation to ensure ICSs conform to their protocol even if an adversary compromises a component. Since protocol conformance prevents unsafe actions, the previously mentioned cyber attacks become impossible. We demonstrate the effectiveness of our methodology using an example from the Fischertechnik Industry 4.0 platform. We measure dynamic attestation's impact on latency and throughput. Our approach is a starting point for studying how to combine formal methods and protocol design to thwart attacks intended to cripple ICSs.
Related papers
- Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
We propose Authenticated Cyclic Redundancy Integrity Check (ACRIC)
ACRIC preserves backward compatibility without requiring additional hardware and is protocol agnostic.
We show that ACRIC offers robust security with minimal transmission overhead ( 1 ms)
arXiv Detail & Related papers (2024-11-21T18:26:05Z) - Games for AI Control: Models of Safety Evaluations of AI Deployment Protocols [52.40622903199512]
This paper introduces AI-Control Games, a formal decision-making model of the red-teaming exercise as a multi-objective, partially observable game.
We apply our formalism to model, evaluate and synthesise protocols for deploying untrusted language models as programming assistants.
arXiv Detail & Related papers (2024-09-12T12:30:07Z) - SISSA: Real-time Monitoring of Hardware Functional Safety and
Cybersecurity with In-vehicle SOME/IP Ethernet Traffic [49.549771439609046]
We propose SISSA, a SOME/IP communication traffic-based approach for modeling and analyzing in-vehicle functional safety and cyber security.
Specifically, SISSA models hardware failures with the Weibull distribution and addresses five potential attacks on SOME/IP communication.
Extensive experimental results show the effectiveness and efficiency of SISSA.
arXiv Detail & Related papers (2024-02-21T03:31:40Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure.
This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus.
We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
arXiv Detail & Related papers (2024-01-19T14:52:04Z) - ICS-Sniper: A Targeted Blackhole Attack on Encrypted ICS Traffic [7.188557101906752]
We show that an Internet adversary in the path of an ICS's communication can cause damage to the ICS without infiltrating it.
We present ICS-Sniper, a targeted blackhole attack that analyzes the packet metadata to identify the packets carrying critical ICS commands or data, and drops the critical packets to disrupt the ICS's operations.
arXiv Detail & Related papers (2023-12-11T06:02:56Z) - When Authentication Is Not Enough: On the Security of Behavioral-Based Driver Authentication Systems [53.2306792009435]
We develop two lightweight driver authentication systems based on Random Forest and Recurrent Neural Network architectures.
We are the first to propose attacks against these systems by developing two novel evasion attacks, SMARTCAN and GANCAN.
Through our contributions, we aid practitioners in safely adopting these systems, help reduce car thefts, and enhance driver security.
arXiv Detail & Related papers (2023-06-09T14:33:26Z) - Security of differential phase shift QKD from relativistic principles [1.0515831025408138]
This work presents the first full security proof of DPS QKD against general attacks.
The proof combines techniques from quantum information theory, quantum optics, and relativity.
Our results shed light on the range of applicability of state-of-the-art security proof techniques.
arXiv Detail & Related papers (2023-01-26T19:00:00Z) - Poisoning Attacks on Cyber Attack Detectors for Industrial Control
Systems [34.86059492072526]
We are first to demonstrate such poisoning attacks on ICS online neural network detectors.
We propose two distinct attack algorithms, namely, back-gradient based poisoning, and demonstrate their effectiveness on both synthetic and real-world data.
arXiv Detail & Related papers (2020-12-23T14:11:26Z) - Adversarial Machine Learning Attacks and Defense Methods in the Cyber
Security Domain [58.30296637276011]
This paper summarizes the latest research on adversarial attacks against security solutions based on machine learning techniques.
It is the first to discuss the unique challenges of implementing end-to-end adversarial attacks in the cyber security domain.
arXiv Detail & Related papers (2020-07-05T18:22:40Z) - Dispelling Myths on Superposition Attacks: Formal Security Model and
Attack Analyses [0.0]
We propose the first computational security model considering superposition attacks for multiparty protocols.
We show that our new security model is satisfiable by proving the security of the well-known One-Time-Pad protocol.
We use this newly imparted knowledge to construct the first concrete protocol for Secure Two-Party Computation that is resistant to superposition attacks.
arXiv Detail & Related papers (2020-07-01T18:00:54Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.