vault backup: 2024-10-22 09:50:32
This commit is contained in:
parent
62ef5fdd94
commit
f75db90bfa
2
.obsidian/graph.json
vendored
2
.obsidian/graph.json
vendored
@ -67,6 +67,6 @@
|
||||
"repelStrength": 12.5,
|
||||
"linkStrength": 1,
|
||||
"linkDistance": 140,
|
||||
"scale": 0.2579747140332347,
|
||||
"scale": 0.3869620710498517,
|
||||
"close": true
|
||||
}
|
||||
8
.obsidian/plugins/colored-tags/data.json
vendored
8
.obsidian/plugins/colored-tags/data.json
vendored
@ -150,7 +150,13 @@
|
||||
"Transfer-functions": 138,
|
||||
"unstructured-uncertainty": 139,
|
||||
"visualized-design": 140,
|
||||
"read": 141
|
||||
"read": 141,
|
||||
"H-Infinity-norm": 142,
|
||||
"PI-controllers": 143,
|
||||
"Robust-performance": 144,
|
||||
"Robust-relative-stability": 145,
|
||||
"Unstructured-multiplicative-uncertainty": 146,
|
||||
"automata": 147
|
||||
},
|
||||
"_version": 3
|
||||
}
|
||||
@ -1,38 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Control Tutorials for MATLAB and Simulink - Introduction: System Modeling"
|
||||
year: Error: `format` can only be applied to dates. Tried for format object
|
||||
authors:
|
||||
|
||||
citekey: "ControlTutorialsMATLAB"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[](https://doi.org/)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
## Tags:
|
||||
|
||||
|
||||
>[!Abstract]
|
||||
>
|
||||
|
||||
>[!note] Markdown Notes
|
||||
>None!
|
||||
|
||||
>[!seealso] Related Papers
|
||||
>
|
||||
|
||||
# Annotations
|
||||
|
||||
### Imported: 2024-10-16 10:10 am
|
||||
|
||||
|
||||
@ -1,49 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Cyber Attack on German Steel Mill Leads to ‘Massive’ Real World Damage"
|
||||
year: 2015
|
||||
authors:
|
||||
|
||||
DOI: ""
|
||||
ISBN: ""
|
||||
citekey: "CyberAttackGerman2015"
|
||||
itemType: "webpage"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[](https://doi.org/)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>.
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> A steel mill in Germany lost control of its blast furnace. Hackers had infiltrated the mill’s control system, according to the German government’s office for information security.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-13T16:36:24.900-04:00 %%
|
||||
@ -1,14 +1,11 @@
|
||||
---
|
||||
status: false
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Introduction to Diffusion Models for Machine Learning"
|
||||
year: 2022
|
||||
authors:
|
||||
|
||||
DOI: ""
|
||||
ISBN: ""
|
||||
citekey: "IntroductionDiffusionModels2022"
|
||||
itemType: "webpage"
|
||||
|
||||
|
||||
|
||||
@ -17,33 +14,25 @@ itemType: "webpage"
|
||||
|
||||
|
||||
---
|
||||
#### DOI
|
||||
](https://doi.org/)
|
||||
#### ISBN
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[](https://doi.org/)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
## Tags:
|
||||
|
||||
|
||||
**Contribution**::
|
||||
>[!Abstract]
|
||||
>The meteoric rise of Diffusion Models is one of the biggest developments in Machine Learning in the past several years. Learn everything you need to know about Diffusion Models in this easy-to-follow guide.
|
||||
|
||||
**Related**::
|
||||
>[!note] Markdown Notes
|
||||
>None!
|
||||
|
||||
> [!LINK]
|
||||
>.
|
||||
>[!seealso] Related Papers
|
||||
>[]()
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> The meteoric rise of Diffusion Models is one of the biggest developments in Machine Learning in the past several years. Learn everything you need to know about Diffusion Models in this easy-to-follow guide.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
# Annotations
|
||||
|
||||
### Imported: 2024-10-22 9:47 am
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T12:05:31.454-04:00 %%
|
||||
|
||||
@ -1,59 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Hardware-in-the-loop simulation"
|
||||
year: 2004
|
||||
authors:
|
||||
|
||||
|
||||
- "Bullock, Darcy"
|
||||
|
||||
- "Johnson, Brian"
|
||||
|
||||
- "Wells, Richard B."
|
||||
|
||||
- "Kyte, Michael"
|
||||
|
||||
- "Li, Zhen"
|
||||
|
||||
|
||||
citekey: "bullockHardwareloopSimulation2004"
|
||||
|
||||
journal: "_Transportation Research Part C: Emerging Technologies_"
|
||||
|
||||
|
||||
volume: 12
|
||||
|
||||
|
||||
issue: 1
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 73-89
|
||||
|
||||
---
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[10.1016/j.trc.2002.10.002](https://doi.org/10.1016/j.trc.2002.10.002)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
## Tags:
|
||||
#Controller, #Equipment, #Hardware, #Signal, #Simulation, #Traffic
|
||||
|
||||
**Related**::
|
||||
|
||||
>[!Abstract]
|
||||
>The current generation of macroscopic and microscopic simulation packages do not have control algorithms that incorporate many of the advanced features now available in commercial traffic control hardware. Consequently, there is a need to develop cost effective procedures for evaluating state of the practice traffic signal control equipment so that informed deployment and design decisions can be made. These same procedures can also be used by researchers to develop new algorithms for applications such as transit priority or adaptive control. In order to achieve that objective, this paper presents the motivation for using hardware-in-the-loop simulation procedures. Hardware-in-the-loop simulation presents a new set of challenges for traffic engineering model developers as the “correctness” of a real-time model not only depends upon the numerical computation, but the timeliness with which the simulation model interacts with external control equipment. This paper reviews the state of practice, summarizes the fundamental technologies necessary for implementing such a system, and uses a simple statistical test for assessing the real-time errors introduced into a simulation model.
|
||||
|
||||
>[!note] Markdown Notes
|
||||
>None!
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-09-04T14:19:36.161-04:00 %%
|
||||
@ -1,83 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Enforcing Memory Safety in Cyber-Physical Systems"
|
||||
year: 2018
|
||||
authors:
|
||||
|
||||
|
||||
- "Chekole, Eyasu Getahun"
|
||||
|
||||
- "Castellanos, John Henry"
|
||||
|
||||
- "Ochoa, Martín"
|
||||
|
||||
- "Yau, David K. Y."
|
||||
|
||||
|
||||
|
||||
- "Katsikas, Sokratis K."
|
||||
|
||||
- "Cuppens, Frédéric"
|
||||
|
||||
- "Cuppens, Nora"
|
||||
|
||||
- "Lambrinoudakis, Costas"
|
||||
|
||||
- "Kalloniatis, Christos"
|
||||
|
||||
- "Mylopoulos, John"
|
||||
|
||||
- "Antón, Annie"
|
||||
|
||||
- "Gritzalis, Stefanos"
|
||||
|
||||
|
||||
DOI: "10.1007/978-3-319-72817-9_9"
|
||||
ISBN: "978-3-319-72817-9"
|
||||
citekey: "chekoleEnforcingMemorySafety2018"
|
||||
itemType: "conferencePaper"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
publisher: "Springer International Publishing"
|
||||
|
||||
|
||||
location: "Cham"
|
||||
|
||||
|
||||
pages: 127-144
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.1007/978-3-319-72817-9_9](https://doi.org/10.1007/978-3-319-72817-9_9)
|
||||
#### ISBN
|
||||
[978-3-319-72817-9](https://www.isbnsearch.org/isbn/978-3-319-72817-9)
|
||||
|
||||
### Tags:
|
||||
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>.
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Cyber-Physical Systems (CPS) integrate computations and communications with physical processes and are being widely adopted in various application areas. However, the increasing prevalence of cyber attacks targeting them poses a growing security concern. In particular, attacks exploiting memory-safety vulnerabilities constitute a major attack vector against CPS, because embedded systems often rely on unsafe but fast programming languages to meet their hard time constraints. A wide range of countermeasures has been developed to provide protection against these attacks. However, the most reliable countermeasures incur in high runtime overheads. In this work, we explore the applicability of strong countermeasures against memory-safety attacks in the context of realistic Industrial Control Systems (ICS). To this end, we design an experimental setup, based on a secure water treatment plant (SWaT) to empirically measure the memory safety overhead (MSO) caused by memory-safe compilation of the Programmable Logic Controller (PLC). We then quantify the tolerability of this overhead in terms of the expected real-time constraints of SWaT. Our results show high effectiveness of the security measure in detecting memory-safety violations and a MSO (197.86 $$\upmu \text {s}$$per scan-cycle) that is also tolerable for the SWaT simulation. We also discuss how different parameters impact the execution time of PLCs and the resulting absolute MSO.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T14:35:33.371-04:00 %%
|
||||
@ -1,63 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "A full-scope, high-fidelity simulator-based hardware-in-the-loop testbed for comprehensive nuclear power plant cybersecurity research"
|
||||
year: 2024
|
||||
authors:
|
||||
|
||||
|
||||
- "Chen, Xiangyi"
|
||||
|
||||
- "Coble, Jamie"
|
||||
|
||||
- "Zhang, Fan"
|
||||
|
||||
|
||||
DOI: "10.1016/j.pnucene.2024.105348"
|
||||
ISBN: ""
|
||||
citekey: "chenFullscopeHighfidelitySimulatorbased2024"
|
||||
itemType: "journalArticle"
|
||||
|
||||
journal: "_Progress in Nuclear Energy_"
|
||||
|
||||
|
||||
volume: 175
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 105348
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.1016/j.pnucene.2024.105348](https://doi.org/10.1016/j.pnucene.2024.105348)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#Cybersecurity, #Hardware-in-the-loop, #Nuclear-power-plants
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>.
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Nuclear power plant (NPP) cybersecurity research often relies on hardware-in-the-loop (HIL) testbeds that integrate real hardware components into simulated environments. These testbeds allow researchers to identify vulnerabilities, evaluate attack impacts, and test security measures in a controlled setting. However, previous HIL testbeds lacked fidelity to accurately represent real nuclear systems, limiting the scope of cybersecurity analysis. This study presents the creation of a HIL testbed, devised upon a full-scope, high-fidelity NPP simulator, to facilitate realistic and comprehensive cybersecurity research. To demonstrate its capabilities, the control logic for the steam generator water level was migrated from the simulator to an external programmable logic controller. As a practical application of the developed testbed, supply chain attack scenarios were simulated by injecting malicious code into the controller logic, and the effects of manipulating sensor inputs and control commands were observed. While this HIL testbed provides more detailed simulations, enhanced realism, and wider applicability compared to other options utilizing a less complex simulator, it is also more intricate and costly. For this reason, we include a detailed comparison with some alternative architectures to aid fellow researchers and practitioners in the selection of a suitable HIL architecture based on specific research objectives.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T14:06:54.985-04:00 %%
|
||||
@ -1,66 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "A Real-Time Hardware-in-the-Loop (HIL) Cybersecurity Testbed for Power Electronics Devices and Systems in Cyber-Physical Environments"
|
||||
year: 2021
|
||||
authors:
|
||||
|
||||
|
||||
- "Choi, Jinchun"
|
||||
|
||||
- "Narayanasamy, Deneesh"
|
||||
|
||||
- "Ahn, Bohyun"
|
||||
|
||||
- "Ahmad, Seerin"
|
||||
|
||||
- "Zeng, Jianwu"
|
||||
|
||||
- "Kim, Taesic"
|
||||
|
||||
|
||||
DOI: "10.1109/PEDG51384.2021.9494202"
|
||||
ISBN: ""
|
||||
citekey: "choiRealTimeHardwareintheLoopHIL2021"
|
||||
itemType: "conferencePaper"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 1-5
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.1109/PEDG51384.2021.9494202](https://doi.org/10.1109/PEDG51384.2021.9494202)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#Control-systems, #Cybersecurity, #Distributed-databases, #false-data-injection-attack, #hardware-in-the-loop-testbed, #man-in-the-middle-attack, #penetration-testing, #power-electronics, #Real-time-systems, #Renewable-energy-sources, #Servers, #Smart-grids, #Tools
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [IEEE Xplore Full Text PDF](file:///home/danesabo/Zotero/storage/QLRZDB5U/Choi%20et%20al.%20-%202021%20-%20A%20Real-Time%20Hardware-in-the-Loop%20(HIL)%20Cybersecuri.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Cybersecurity of power electronics (PE) is increasingly essential as more systems from renewable energy systems, energy storage systems, and electric vehicle charging stations utilize PE devices to connect them into power grids with complex communication and computation systems for advanced control and situational awareness improvement in smart grid environments. However, cybersecurity research and development (R&D) of networked power electronics (PE) is hampered by the lack of real-time security testbed incorporating real cyber events. This paper proposes a real-time hardware-in-the-loop cybersecurity tested for PE systems in cyber-physical environments. The proposed security testbed consists of: 1) a real-time PE system simulator; 2) a real-time cyber system using real network systems and a server; and 3) penetration testing tools generating real Cyber-attacks as cyber events. Several real cyber-attacks are created and their impacts in a PE system are provided to validate the feasibility of the proposed security testbed.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T14:08:17.619-04:00 %%
|
||||
@ -1,74 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Applying Model Checking to Industrial-Sized PLC Programs"
|
||||
year: 2015
|
||||
authors:
|
||||
|
||||
|
||||
- "Fernández Adiego, Borja"
|
||||
|
||||
- "Darvas, Dániel"
|
||||
|
||||
- "Viñuela, Enrique Blanco"
|
||||
|
||||
- "Tournier, Jean-Charles"
|
||||
|
||||
- "Bliudze, Simon"
|
||||
|
||||
- "Blech, Jan Olaf"
|
||||
|
||||
- "González Suárez, Víctor Manuel"
|
||||
|
||||
|
||||
DOI: "10.1109/TII.2015.2489184"
|
||||
ISBN: ""
|
||||
citekey: "fernandezadiegoApplyingModelChecking2015"
|
||||
itemType: "journalArticle"
|
||||
|
||||
journal: "_IEEE Transactions on Industrial Informatics_"
|
||||
|
||||
|
||||
volume: 11
|
||||
|
||||
|
||||
issue: 6
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 1400-1410
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.1109/TII.2015.2489184](https://doi.org/10.1109/TII.2015.2489184)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#automata, #Automata, #Biological-system-modeling, #IEC-61131, #IEC-Standards, #Informatics, #model-checking, #Model-checking, #modeling, #nuXmv, #PLC, #programmable-logic-controller-PLC, #Software, #verification
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [IEEE Xplore Full Text PDF](file:///home/danesabo/Zotero/storage/AG66IMW4/Fernández%20Adiego%20et%20al.%20-%202015%20-%20Applying%20Model%20Checking%20to%20Industrial-Sized%20PLC%20Pr.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Programmable logic controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the correctness of safety-critical software, but is still underused in industry due to the complexity of building and managing formal models of real applications. In this paper, we propose a general methodology to perform automated model checking of complex properties expressed in temporal logics [e.g., computation tree logic (CTL) and linear temporal logic (LTL)] on PLC programs. This methodology is based on an intermediate model (IM) meant to transform PLC programs written in various standard languages [structured text (ST), sequential function chart (SFC), etc.] to different modeling languages of verification tools. We present the syntax and semantics of the IM, and the transformation rules of the ST and SFC languages to the nuXmv model checker passing through the IM. Finally, two real cases studies of the European Organization for Nuclear Research (CERN) PLC programs, written mainly in the ST language, are presented to illustrate and validate the proposed approach.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T14:13:25.972-04:00 %%
|
||||
@ -1,84 +1,100 @@
|
||||
---
|
||||
readstatus: true
|
||||
dateread:
|
||||
title: Formally verified software in the real world
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Formally verified software in the real world"
|
||||
year: 2018
|
||||
authors:
|
||||
- Klein, Gerwin
|
||||
- Andronick, June
|
||||
- Fernandez, Matthew
|
||||
- Kuz, Ihor
|
||||
- Murray, Toby
|
||||
- Heiser, Gernot
|
||||
DOI: 10.1145/3230627
|
||||
ISBN: ""
|
||||
citekey: kleinFormallyVerifiedSoftware2018
|
||||
itemType: journalArticle
|
||||
journal: _Commun. ACM_
|
||||
volume: 61
|
||||
issue: 10
|
||||
pages: 68–77
|
||||
---
|
||||
#### DOI
|
||||
[10.1145/3230627](https://doi.org/10.1145/3230627)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
|
||||
- "Klein, Gerwin"
|
||||
|
||||
- "Andronick, June"
|
||||
|
||||
- "Fernandez, Matthew"
|
||||
|
||||
- "Kuz, Ihor"
|
||||
|
||||
- "Murray, Toby"
|
||||
|
||||
- "Heiser, Gernot"
|
||||
|
||||
|
||||
citekey: "kleinFormallyVerifiedSoftware2018"
|
||||
|
||||
journal: "Commun. ACM"
|
||||
|
||||
|
||||
volume: 61
|
||||
|
||||
|
||||
issue: 10
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 68–77
|
||||
|
||||
---
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[10.1145/3230627](https://doi.org/10.1145/3230627)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
## Tags:
|
||||
#formal-verification, #Control-systems, #Cybersecurity, #penetration-testing, #Formal-methods
|
||||
|
||||
**Contribution**::
|
||||
>[!Abstract]
|
||||
>Verified software secures the Unmanned Little Bird autonomous helicopter against mid-flight cyber attacks.
|
||||
|
||||
**Related**::
|
||||
>[!note] Markdown Notes
|
||||
>None!
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [Full Text PDF](file:///home/danesabo/Zotero/storage/CVGJMIHP/Klein%20et%20al.%20-%202018%20-%20Formally%20verified%20software%20in%20the%20real%20world.pdf).
|
||||
>[!seealso] Related Papers
|
||||
>[]()
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Verified software secures the Unmanned Little Bird autonomous helicopter against mid-flight cyber attacks.
|
||||
>.
|
||||
# Annotations
|
||||
|
||||
>[!attention] Highlight
|
||||
> *key insights ˽ Formal proof based on micro-kernelenforced software architecture can scale to real systems at low cost. ˽ Mixed assurance levels and security levels within one system are possible and desirable; not all code has to be assured to the highest level. ˽ High assurance can be retrofitted to suitable existing systems with only moderate redesign and refactoring.*
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
>[!done] Quote
|
||||
> *Its foundation is our verified microkernel, seL4, discussed later, which guarantees isolation between subsystems except for well-defined communication channels that are subject to the system’s security policy.*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *Note we primarily use formal verification to provide proofs about correctness of code that a system’s safety or security relies on. But it has other benefits as well. For example, code correctness proofs make assumptions about the context in which the code is run (such as behavior of hardware and configuration of software). Since formal verification makes these assumptions explicit, developer effort can focus on ensuring the assumptions hold—through other means of verification like testing. Moreover, in many cases systems consist of a combination of verified and non-verified code, and in them, formal verification acts as a lens, focusing review, testing, and debugging on the system’s critical nonverified code.*
|
||||
>
|
||||
|
||||
>[!done] Quote
|
||||
> *The mechanisms support its use as a hypervisor to, say, host entire Linux operating systems while keeping them isolated from security-critical components that might run alongside, as outlined in Figure 1. In particular, this functionality allows system designers to deploy legacy components that may have latent vulnerabilities alongside highly trustworthy components.*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *The dual of integrity is confidentiality, which states that a component cannot read another component’s data without permission,2*
|
||||
>
|
||||
> >[!note] Note
|
||||
> >Integrity: The inability for process A to mess with process B unless explicitly defined as being allowed to.
|
||||
|
||||
Confidentiality: Process A cannot READ anything that it isn't explicitly allowed to
|
||||
|
||||
>[!attention] Highlight
|
||||
> *the link between Linux and the crypto component in Figure 4 is for message passing only and does not give access to memory. Only authenticated messages can reach the CAN bus, as the crypto component is the only connection to the driver. Untrusted payload software and WiFi are, as part of the Linux VM, encapsulated by component isolation and can communicate to the rest of the system only via the trusted crypto component.*
|
||||
>
|
||||
|
||||
>[!question] Don't Understand
|
||||
> *The mechanisms of the seL4 kernel discussed earlier can achieve this enforcement, but the level of abstraction of the mechanisms is in stark contrast to the boxes and arrows of an architecture diagram; even the more abstract access-control policy still contains far more detail than the architecture diagram. A running system of this size contains tens of thousands of kernel objects and capabilities that are created programmatically, and errors in configuration could lead to security violations. We next discuss how we not only automate the configuration and construction of such code but also how we can automatically prove that architecture boundaries are enforced.*
|
||||
>
|
||||
|
||||
>[!done] Quote
|
||||
> *Due to the isolation provided by seL4 and the componentized architecture, it becomes possible for components of mixed assurance levels to coexist in the system without decreasing the overall assurance to that of the lowest-assurance component or increasing the verification burden of the lowest-assurance components to that of the highest-assurance ones.*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *The right granularity is a trade-off between the strength of isolation on the one hand and the increased overhead and cost of communication between partitions, as well as re-engineering cost, on the other.*
|
||||
>
|
||||
|
||||
### Imported: 2024-10-22 9:47 am
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
### Imported: 2024-08-12 4:55 pm
|
||||
|
||||
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> key insights ˽ Formal proof based on micro-kernelenforced software architecture can scale to real systems at low cost. ˽ Mixed assurance levels and security levels within one system are possible and desirable; not all code has to be assured to the highest level. ˽ High assurance can be retrofitted to suitable existing systems with only moderate redesign and refactoring.
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> Its foundation is our verified microkernel, seL4, discussed later, which guarantees isolation between subsystems except for well-defined communication channels that are subject to the system’s security policy.
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> Note we primarily use formal verification to provide proofs about correctness of code that a system’s safety or security relies on. But it has other benefits as well. For example, code correctness proofs make assumptions about the context in which the code is run (such as behavior of hardware and configuration of software). Since formal verification makes these assumptions explicit, developer effort can focus on ensuring the assumptions hold—through other means of verification like testing. Moreover, in many cases systems consist of a combination of verified and non-verified code, and in them, formal verification acts as a lens, focusing review, testing, and debugging on the system’s critical nonverified code.
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> The mechanisms support its use as a hypervisor to, say, host entire Linux operating systems while keeping them isolated from security-critical components that might run alongside, as outlined in Figure 1. In particular, this functionality allows system designers to deploy legacy components that may have latent vulnerabilities alongside highly trustworthy components.
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> The dual of integrity is confidentiality, which states that a component cannot read another component’s data without permission,2
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> the link between Linux and the crypto component in Figure 4 is for message passing only and does not give access to memory. Only authenticated messages can reach the CAN bus, as the crypto component is the only connection to the driver. Untrusted payload software and WiFi are, as part of the Linux VM, encapsulated by component isolation and can communicate to the rest of the system only via the trusted crypto component.
|
||||
|
||||
<mark style="background-color: #f19837">Quote</mark>
|
||||
> The mechanisms of the seL4 kernel discussed earlier can achieve this enforcement, but the level of abstraction of the mechanisms is in stark contrast to the boxes and arrows of an architecture diagram; even the more abstract access-control policy still contains far more detail than the architecture diagram. A running system of this size contains tens of thousands of kernel objects and capabilities that are created programmatically, and errors in configuration could lead to security violations. We next discuss how we not only automate the configuration and construction of such code but also how we can automatically prove that architecture boundaries are enforced.
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> Due to the isolation provided by seL4 and the componentized architecture, it becomes possible for components of mixed assurance levels to coexist in the system without decreasing the overall assurance to that of the lowest-assurance component or increasing the verification burden of the lowest-assurance components to that of the highest-assurance ones.
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> The right granularity is a trade-off between the strength of isolation on the one hand and the increased overhead and cost of communication between partitions, as well as re-engineering cost, on the other.
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-12T16:55:33.616-04:00 %%
|
||||
|
||||
@ -1,62 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "The real story of stuxnet"
|
||||
year: 2013
|
||||
authors:
|
||||
|
||||
|
||||
- "Kushner, David"
|
||||
|
||||
|
||||
DOI: "10.1109/MSPEC.2013.6471059"
|
||||
ISBN: ""
|
||||
citekey: "kushnerRealStoryStuxnet2013"
|
||||
itemType: "journalArticle"
|
||||
|
||||
journal: "_IEEE Spectrum_"
|
||||
|
||||
|
||||
volume: 50
|
||||
|
||||
|
||||
issue: 3
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 48-53
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.1109/MSPEC.2013.6471059](https://doi.org/10.1109/MSPEC.2013.6471059)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#Companies, #Computer-hacking, #Computer-security, #Computer-viruses, #Cryptography, #Malware
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [IEEE Xplore Full Text PDF](file:///home/danesabo/Zotero/storage/M3CM6S3Z/Kushner%20-%202013%20-%20The%20real%20story%20of%20stuxnet.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> The paper discusses how Kaspersky Lab tracked down the malware that stymied Iran's nuclear-fuel enrichment program.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-13T16:25:59.375-04:00 %%
|
||||
@ -1,85 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Synthetic Lagrangian turbulence by generative diffusion models"
|
||||
year: 2024
|
||||
authors:
|
||||
|
||||
|
||||
- "Li, T."
|
||||
|
||||
- "Biferale, L."
|
||||
|
||||
- "Bonaccorso, F."
|
||||
|
||||
- "Scarpolini, M. A."
|
||||
|
||||
- "Buzzicotti, M."
|
||||
|
||||
|
||||
citekey: "liSyntheticLagrangianTurbulence2024"
|
||||
|
||||
journal: "Nature Machine Intelligence"
|
||||
|
||||
|
||||
volume: 6
|
||||
|
||||
|
||||
issue: 4
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 393-403
|
||||
|
||||
---
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[10.1038/s42256-024-00810-0](https://doi.org/10.1038/s42256-024-00810-0)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
## Tags:
|
||||
#Diffusion, #Turbulence
|
||||
|
||||
>[!Abstract]
|
||||
>Abstract
|
||||
Lagrangian turbulence lies at the core of numerous applied and fundamental problems related to the physics of dispersion and mixing in engineering, biofluids, the atmosphere, oceans and astrophysics. Despite exceptional theoretical, numerical and experimental efforts conducted over the past 30 years, no existing models are capable of faithfully reproducing statistical and topological properties exhibited by particle trajectories in turbulence. We propose a machine learning approach, based on a state-of-the-art diffusion model, to generate single-particle trajectories in three-dimensional turbulence at high Reynolds numbers, thereby bypassing the need for direct numerical simulations or experiments to obtain reliable Lagrangian data. Our model demonstrates the ability to reproduce most statistical benchmarks across time scales, including the fat-tail distribution for velocity increments, the anomalous power law and the increased intermittency around the dissipative scale. Slight deviations are observed below the dissipative scale, particularly in the acceleration and flatness statistics. Surprisingly, the model exhibits strong generalizability for extreme events, producing events of higher intensity and rarity that still match the realistic statistics. This paves the way for producing synthetic high-quality datasets for pretraining various downstream applications of Lagrangian turbulence.
|
||||
|
||||
>[!note] Markdown Notes
|
||||
>None!
|
||||
# Annotations
|
||||
|
||||
>[!fail] Possibly Incorrect
|
||||
> *agrangian turbulence lies at the core of numerous applied and fundamental problems related to the physics of dispersion and mixing in engineering, biofluids, the atmosphere, oceans and astrophysics. Despite exceptional theoretical, numerical and experimental efforts conducted over the past 30 years, no existing models are capable of faithfully reproducing statistical and topological properties exhibited by particle tr*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *me scales, including the fat-tail distribution for velocity increments, the anomalous power law and the increased intermittency around the dissipative scale. Slight deviations are observed below the dissipative scale, particularly in the acceleration and flatness statistics. Surprisingly, the model exhibits strong generalizability for ext*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *stion, industrial mixing, pollutant dispersion, quantum fluids, protoplanetary disks accretion, cloud formation*
|
||||
>
|
||||
> >[!note] Note
|
||||
> >This, is a coment. that is a test!
|
||||
|
||||
>[!fail] Possibly Incorrect
|
||||
> *table-top*
|
||||
>
|
||||
|
||||
>[!done] Quote
|
||||
> *laboratory*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *flows*
|
||||
>
|
||||
|
||||
>[!question] Don't Understand
|
||||
> *at*
|
||||
>
|
||||
|
||||
### Imported: 2024-09-04 4:14 pm
|
||||
|
||||
|
||||
@ -1,65 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller"
|
||||
year: 2022
|
||||
authors:
|
||||
|
||||
|
||||
- "Lopez-Miguel, Ignacio D."
|
||||
|
||||
- "Tournier, Jean-Charles"
|
||||
|
||||
- "Adiego, Borja Fernandez"
|
||||
|
||||
|
||||
DOI: "10.18429/JACoW-ICALEPCS2021-MOPV042"
|
||||
ISBN: ""
|
||||
citekey: "lopez-miguelPLCverifStatusFormal2022"
|
||||
itemType: "journalArticle"
|
||||
|
||||
journal: "_Proceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems_"
|
||||
|
||||
|
||||
volume: ICALEPCS2021
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 5 pages, 0.147 MB
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.18429/JACoW-ICALEPCS2021-MOPV042](https://doi.org/10.18429/JACoW-ICALEPCS2021-MOPV042)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#Computer-Science---Software-Engineering
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [arXiv Fulltext PDF](file:///home/danesabo/Zotero/storage/FPPDGM5D/Lopez-Miguel%20et%20al.%20-%202022%20-%20PLCverif%20Status%20of%20a%20Formal%20Verification%20Tool%20for.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of validating the PLC control system logic, CERN developed a model checking platform to go one step further and formally verify PLC logic. This platform, called PLCverif, first released internally for CERN usage in 2019, is now available to anyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>
|
||||
>Comment: 18th International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS2021).
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T14:14:45.686-04:00 %%
|
||||
@ -1,47 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: ADVANCED REACTOR CYBER ANALYSIS AND DEVELOPMENT ENVIRONMENT (ARCADE) FOR UNIVERSITY RESEARCH
|
||||
authors:
|
||||
- Maccarone, L T
|
||||
- Hahn, A S
|
||||
- Valme, R
|
||||
- Rowland, M T
|
||||
- Kapuria, A
|
||||
- Zhang, Y
|
||||
- Cole, D G
|
||||
DOI: ""
|
||||
ISBN: ""
|
||||
citekey: maccaroneADVANCEDREACTORCYBER
|
||||
itemType: journalArticle
|
||||
journal: __
|
||||
---
|
||||
#### DOI
|
||||
[](https://doi.org/)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [Maccarone et al. - ADVANCED REACTOR CYBER ANALYSIS AND DEVELOPMENT EN.pdf](file:///home/danesabo/Zotero/storage/7UDGTJ8S/Maccarone%20et%20al.%20-%20ADVANCED%20REACTOR%20CYBER%20ANALYSIS%20AND%20DEVELOPMENT%20EN.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-12T17:10:36.208-04:00 %%
|
||||
66
200 Library Papers/matusuRegionsRobustRelative2023.md
Normal file
66
200 Library Papers/matusuRegionsRobustRelative2023.md
Normal file
@ -0,0 +1,66 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Regions of robust relative stability for PI controllers and LTI plants with unstructured multiplicative uncertainty: A second-order-based example"
|
||||
year: 2023
|
||||
authors:
|
||||
|
||||
|
||||
- "Matušů, Radek"
|
||||
|
||||
- "Senol, Bilal"
|
||||
|
||||
- "Pekař, Libor"
|
||||
|
||||
|
||||
citekey: "matusuRegionsRobustRelative2023"
|
||||
|
||||
journal: "Heliyon"
|
||||
|
||||
|
||||
volume: 9
|
||||
|
||||
|
||||
issue: 8
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[10.1016/j.heliyon.2023.e18924](https://doi.org/10.1016/j.heliyon.2023.e18924)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
## Tags:
|
||||
#Robust-control, #H-Infinity-norm, #PI-controllers, #Robust-performance, #Robust-relative-stability, #Unstructured-multiplicative-uncertainty
|
||||
|
||||
>[!Abstract]
|
||||
>
|
||||
|
||||
>[!note] Markdown Notes
|
||||
>This might be an example of sampling unstructured uncertainties
|
||||
|
||||
>[!seealso] Related Papers
|
||||
>
|
||||
|
||||
# Annotations
|
||||
|
||||
>[!fail] Possibly Incorrect
|
||||
> *With respect to the classical robust control literature, the robust stability condition under consideration of multiplicative uncertainty can be formulated as follows: Under the assumption of a nominally stable feedback control system (that is, for G0(s)), the related perturbed feedback control system (containing the plant affected by multiplicative uncertainty) is robustly stable if and only if [7,13, 14]: ‖WM(s)T0(s)‖∞ < 1 (3) Recently, the paper [7] has presented the relativized version of this condition as follows: Under the assumption of a nominally stable feedback control system, the related uncertain feedback control loop is robustly relatively stable, having a margin factor of α if and only if [7]: ‖WM(s)T0(s)‖∞ < 1 α (4) Typically, the margin factor α is assumed to be positive. For the special case of α = 1, both conditions (3) and (4) become identical. More information on the robust stability, robust performance, and robust relative stability conditions, including their graphical interpretations and their versions for the other sorts of models under unstructured uncertainty, can be found in Ref. [7].*
|
||||
>
|
||||
> >[!note] Note
|
||||
> >This is braindead. They invented a factor of safety... that was a whole publication?
|
||||
|
||||
>[!attention] Highlight
|
||||
> *Then, the weight function WM(s), which must fulfill (2), was determined in Ref. [16] as the worst-case uncertainty member (with K = 2.2, T1 = 9, T2 = 0.9) of the plant family (5). This worst-case combination of parameters tallies with the uppermost magnitude characteristics of the normalized perturbations from Figs. 2 and 3 [16], and so the weight function was chosen exactly accordingly:*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *The main purpose of ΔM(s) is (except for acting as a scaling factor on the perturbation magnitude) to account for phase uncertainty [13].*
|
||||
>
|
||||
|
||||
### Imported: 2024-10-22 9:44 am
|
||||
|
||||
|
||||
@ -1,58 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Controller-aware false data injection against programmable logic controllers"
|
||||
year: 2014
|
||||
authors:
|
||||
|
||||
|
||||
- "McLaughlin, Stephen"
|
||||
|
||||
- "Zonouz, Saman"
|
||||
|
||||
|
||||
DOI: "10.1109/SmartGridComm.2014.7007754"
|
||||
ISBN: ""
|
||||
citekey: "mclaughlinControllerawareFalseData2014"
|
||||
itemType: "conferencePaper"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 848-853
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.1109/SmartGridComm.2014.7007754](https://doi.org/10.1109/SmartGridComm.2014.7007754)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#Automata, #Control-systems, #Power-systems, #Process-control, #Servers, #State-estimation, #Vectors
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [IEEE Xplore Full Text PDF](file:///home/danesabo/Zotero/storage/XVIK6466/McLaughlin%20and%20Zonouz%20-%202014%20-%20Controller-aware%20false%20data%20injection%20against%20prog.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Control systems rely on accurate sensor measurements to safely regulate physical processes. In False Data Injection (FDI) attacks, adversaries inject forged sensor measurements into a control system in hopes of misguiding control algorithms into taking dangerous actions. Traditional FDI attacks mostly require adversaries to know the full system topology, i.e., hundreds or thousands of lines and buses, while having unpredictable consequences. In this paper, we present a new class of FDI attacks directly against individual Programmable Logic Controllers (PLCs), which are ubiquitous in power generation and distribution. Our attack allows the adversary to have only partial information about the victim subsystem, and produces a predictable malicious result. Our attack tool analyzes an I/O trace of the compromised PLCs to produce a set of inputs to achieve the desired PLC outputs, i.e., the system behavior. It proceeds in two steps. First, our tool constructs a model of the PLC's internal logic from the I/O traces. Second, it searches for a set of inputs that cause the model to calculate the desired malicious behavior. We evaluate our tool against a set of representative control systems and show that it is a practical threat against insecure sensor configurations.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T14:10:03.042-04:00 %%
|
||||
@ -1,75 +1,82 @@
|
||||
---
|
||||
readstatus: true
|
||||
dateread: 2024-08-13
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Hardware-in-the-Loop Simulations: A Historical Overview of Engineering Challenges"
|
||||
year: 2022
|
||||
authors:
|
||||
- Mihalič, Franc
|
||||
- Truntič, Mitja
|
||||
- Hren, Alenka
|
||||
DOI: 10.3390/electronics11152462
|
||||
ISBN: ""
|
||||
citekey: mihalicHardwareintheLoopSimulationsHistorical2022
|
||||
itemType: journalArticle
|
||||
journal: _Electronics_
|
||||
volume: 11
|
||||
issue: 15
|
||||
pages: 2462
|
||||
---
|
||||
#### DOI
|
||||
[10.3390/electronics11152462](https://doi.org/10.3390/electronics11152462)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
|
||||
- "Mihalič, Franc"
|
||||
|
||||
- "Truntič, Mitja"
|
||||
|
||||
- "Hren, Alenka"
|
||||
|
||||
|
||||
citekey: "mihalicHardwareintheLoopSimulationsHistorical2022"
|
||||
|
||||
journal: "Electronics"
|
||||
|
||||
|
||||
volume: 11
|
||||
|
||||
|
||||
issue: 15
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 2462
|
||||
|
||||
---
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[10.3390/electronics11152462](https://doi.org/10.3390/electronics11152462)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
## Tags:
|
||||
#automotive, #controller-in-the-loop-CIL, #DC-DC-converters, #electric-drives, #grid-applications, #hardware-in-the-loop-HIL, #inverter-systems, #power-hardware-in-the-loop-PHIL, #railway-systems
|
||||
|
||||
**Contribution**::
|
||||
* Lots of good citations to papers about hardware in the loop things. Has citations for a lot of the claims I'm making in [[ARCADE Implementation at the University of Pittsburgh]] about implementation in automotive contexts. Also comments about how expensive these systems are.
|
||||
**Related**::
|
||||
>[!Abstract]
|
||||
>The design of modern industrial products is further improved through the hardware-in-the-loop (HIL) simulation. Realistic simulation is enabled by the closed loop between the hardware under test (HUT) and real-time simulation. Such a system involves a field programmable gate array (FPGA) and digital signal processor (DSP). An HIL model can bypass serious damage to the real object, reduce debugging cost, and, finally, reduce the comprehensive effort during the testing. This paper provides a historical overview of HIL simulations through different engineering challenges, i.e., within automotive, power electronics systems, and different industrial drives. Various platforms, such as National Instruments, dSPACE, Typhoon HIL, or MATLAB Simulink Real-Time toolboxes and Speedgoat hardware systems, offer a powerful tool for efficient and successful investigations in different fields. Therefore, HIL simulation practice must begin already during the university’s education process to prepare the students for professional engagements in the industry, which was also verified experimentally at the end of the paper.
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [Full Text PDF](file:///home/danesabo/Zotero/storage/893YXFRK/Mihalič%20et%20al.%20-%202022%20-%20Hardware-in-the-Loop%20Simulations%20A%20Historical%20Ove.pdf).
|
||||
>[!note] Markdown Notes
|
||||
>None!
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> The design of modern industrial products is further improved through the hardware-in-the-loop (HIL) simulation. Realistic simulation is enabled by the closed loop between the hardware under test (HUT) and real-time simulation. Such a system involves a field programmable gate array (FPGA) and digital signal processor (DSP). An HIL model can bypass serious damage to the real object, reduce debugging cost, and, finally, reduce the comprehensive effort during the testing. This paper provides a historical overview of HIL simulations through different engineering challenges, i.e., within automotive, power electronics systems, and different industrial drives. Various platforms, such as National Instruments, dSPACE, Typhoon HIL, or MATLAB Simulink Real-Time toolboxes and Speedgoat hardware systems, offer a powerful tool for efficient and successful investigations in different fields. Therefore, HIL simulation practice must begin already during the university’s education process to prepare the students for professional engagements in the industry, which was also verified experimentally at the end of the paper.
|
||||
>.
|
||||
>[!seealso] Related Papers
|
||||
>[]()
|
||||
|
||||
# Annotations
|
||||
|
||||
>[!done] Quote
|
||||
> *An HIL model can bypass serious damage to the real object, reduce debugging cost, and, finally, reduce the comprehensive effort during the testing.*
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
>[!attention] Highlight
|
||||
> *At the same time, HIL simulation also includes controller-in-the-loop (CIL) simulations, forming the backbone of the automotive, defense, marine, and space industries. This simulation is infallible in testing a component, such as an electronic control unit (ECU), and is connected to the simulation instead of the real equipment under control.*
|
||||
>
|
||||
|
||||
>[!fail] Possibly Incorrect
|
||||
> *The fact is that the actuators are hard to model, and, when they are available, can be incorporated into the simulation loop to improve the simulation.*
|
||||
>
|
||||
|
||||
>[!done] Quote
|
||||
> *In the last half-century, HIL simulation has played an essential role in the field of flight simulation [3]. At the same time, broad use of this method can also be found in the testing of missile guidance systems [4]. Even before this, highly maneuverable aircraft technology (HiMAT) was developed by NASA [5]. Within this program, the use of advanced concepts was investigated (such as fly-by-wire and reduced static stability). Additional to NASA’s development of an area of high-fidelity HIL simulations, the USAF Phillips Lab has developed a laboratory to integrate component technologies and demonstrate spacecraft subsystem/payload level capabilities [6]. HIL simulation is developing fast from a system model design, synthesis, and simulation criterion. An HIL simulator is often a powerful tool in many applications, such as airplanes, missiles, and uncrewed aerial- or ground-traffic vehicles, where the autopilots play a crucial and vital role [7]. Through the HIL simulator, the embedded system is forced to operate in real time, such as in the real world with real inputs and outputs. For example, the autopilot fools the aircraft system into thinking that it is flying.*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *cost slightly over EUR 100,000 (with 100 inputs and outputs), then the second identical unit cost about EUR 25,000 to build. This was considered a bargain compared to the multi-million dollar unmanned aerial vehicles (UAVs) they were developing—if the HILS prevented the crash of just one UAV, the company would get its money’s worth. There was another, even more, valuable benefit: a HILS allows the software to be developed and tested without waiting for the actual hardware to be built (or, in this case, built and flown*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *In [13], dSpace offers safe testing through the power hardware-in-theloop (Power HIL or PHIL) systems, where a relevant emulation is used for the simulated signals (Figure 3) to validate the ECUs with software-in-the-loop (SIL) in HIL environments. The ECU software is, in a SIL solution, certified in a virtual environment. The ECU software can then be approved with no ECU hardware at all. The requested object model and the software run on a PC using particular tools. The test execution is also possible in the cloud with included scaling as well.*
|
||||
>
|
||||
|
||||
>[!done] Quote
|
||||
> *MATLAB by MathWorks, Inc. [81] is used widely in the dynamic system and controls analysis and simulation areas in the industry and at universities for educational purposes. MATLAB with add-on components called toolboxes is the primary “engine”. Simulink is a MATLAB add-on that provides a graphical user interface for model development and system simulation [9]. The real-time toolboxes and Speedgoat real-time target machines (see Figure 38) can generate real-time code for Simulink models [10], and take you from simulation to RCP and HIL testing in a single click.*
|
||||
>
|
||||
|
||||
### Imported: 2024-10-22 9:46 am
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
### Imported: 2024-08-13 1:47 pm
|
||||
|
||||
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> An HIL model can bypass serious damage to the real object, reduce debugging cost, and, finally, reduce the comprehensive effort during the testing.
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> At the same time, HIL simulation also includes controller-in-the-loop (CIL) simulations, forming the backbone of the automotive, defense, marine, and space industries. This simulation is infallible in testing a component, such as an electronic control unit (ECU), and is connected to the simulation instead of the real equipment under control.
|
||||
|
||||
<mark style="background-color: #ff6666">Quote</mark>
|
||||
> The fact is that the actuators are hard to model, and, when they are available, can be incorporated into the simulation loop to improve the simulation.
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> In the last half-century, HIL simulation has played an essential role in the field of flight simulation [3]. At the same time, broad use of this method can also be found in the testing of missile guidance systems [4]. Even before this, highly maneuverable aircraft technology (HiMAT) was developed by NASA [5]. Within this program, the use of advanced concepts was investigated (such as fly-by-wire and reduced static stability). Additional to NASA’s development of an area of high-fidelity HIL simulations, the USAF Phillips Lab has developed a laboratory to integrate component technologies and demonstrate spacecraft subsystem/payload level capabilities [6]. HIL simulation is developing fast from a system model design, synthesis, and simulation criterion. An HIL simulator is often a powerful tool in many applications, such as airplanes, missiles, and uncrewed aerial- or ground-traffic vehicles, where the autopilots play a crucial and vital role [7]. Through the HIL simulator, the embedded system is forced to operate in real time, such as in the real world with real inputs and outputs. For example, the autopilot fools the aircraft system into thinking that it is flying.
|
||||
|
||||
<mark style="background-color: #e56eee">Quote</mark>
|
||||
> cost slightly over EUR 100,000 (with 100 inputs and outputs), then the second identical unit cost about EUR 25,000 to build. This was considered a bargain compared to the multi-million dollar unmanned aerial vehicles (UAVs) they were developing—if the HILS prevented the crash of just one UAV, the company would get its money’s worth. There was another, even more, valuable benefit: a HILS allows the software to be developed and tested without waiting for the actual hardware to be built (or, in this case, built and flown
|
||||
|
||||
<mark style="background-color: #e56eee">Quote</mark>
|
||||
> In [13], dSpace offers safe testing through the power hardware-in-theloop (Power HIL or PHIL) systems, where a relevant emulation is used for the simulated signals (Figure 3) to validate the ECUs with software-in-the-loop (SIL) in HIL environments. The ECU software is, in a SIL solution, certified in a virtual environment. The ECU software can then be approved with no ECU hardware at all. The requested object model and the software run on a PC using particular tools. The test execution is also possible in the cloud with included scaling as well.
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> MATLAB by MathWorks, Inc. [81] is used widely in the dynamic system and controls analysis and simulation areas in the industry and at universities for educational purposes. MATLAB with add-on components called toolboxes is the primary “engine”. Simulink is a MATLAB add-on that provides a graphical user interface for model development and system simulation [9]. The real-time toolboxes and Speedgoat real-time target machines (see Figure 38) can generate real-time code for Simulink models [10], and take you from simulation to RCP and HIL testing in a single click.
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-13T13:47:22.281-04:00 %%
|
||||
|
||||
@ -1,72 +0,0 @@
|
||||
---
|
||||
status: false
|
||||
dateread:
|
||||
title: "Fuzzy Control Systems: Past, Present and Future"
|
||||
year: 2019
|
||||
authors:
|
||||
|
||||
|
||||
- "Nguyen, Anh-Tu"
|
||||
|
||||
- "Taniguchi, Tadanari"
|
||||
|
||||
- "Eciolaza, Luka"
|
||||
|
||||
- "Campos, Victor"
|
||||
|
||||
- "Palhares, Reinaldo"
|
||||
|
||||
- "Sugeno, Michio"
|
||||
|
||||
|
||||
DOI: "10.1109/MCI.2018.2881644"
|
||||
ISBN: ""
|
||||
citekey: "nguyenFuzzyControlSystems2019"
|
||||
itemType: "journalArticle"
|
||||
|
||||
journal: "_IEEE Computational Intelligence Magazine_"
|
||||
|
||||
|
||||
volume: 14
|
||||
|
||||
|
||||
issue: 1
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
pages: 56-68
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.1109/MCI.2018.2881644](https://doi.org/10.1109/MCI.2018.2881644)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#Analytical-models, #Fuzzy-control, #Fuzzy-logic, #Fuzzy-systems, #Linguistics, #Nonlinear-systems, #Stability-analysis, #Zadeh,-Lotfi
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [IEEE Xplore Full Text PDF](file:///home/danesabo/Zotero/storage/IS27EM5M/Nguyen%20et%20al.%20-%202019%20-%20Fuzzy%20Control%20Systems%20Past,%20Present%20and%20Future.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> More than 40 years after fuzzy logic control appeared as an effective tool to deal with complex processes, the research on fuzzy control systems has constantly evolved. Mamdani fuzzy control was originally introduced as a model-free control approach based on expert?s experience and knowledge. Due to the lack of a systematic framework to study Mamdani fuzzy systems, we have witnessed growing interest in fuzzy model-based approaches with Takagi-Sugeno fuzzy systems and singleton-type fuzzy systems (also called piecewise multiaffine systems) over the past decades. This paper reviews the key features of the three above types of fuzzy systems. Through these features, we point out the historical rationale for each type of fuzzy systems and its current research mainstreams. However, the focus is put on fuzzy model-based approaches developed via Lyapunov stability theorem and linear matrix inequality (LMI) formulations. Finally, our personal viewpoint on the perspectives and challenges of the future fuzzy control research is discussed.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T12:05:44.055-04:00 %%
|
||||
@ -1,48 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: Hardware-In-The-Loop Labs for SCADA Cybersecurity Awareness and Training
|
||||
year: 2021
|
||||
authors:
|
||||
- Puys, Maxime
|
||||
- Thevenon, Pierre-Henri
|
||||
- Mocanu, Stéphane
|
||||
DOI: 10.1145/3465481.3469185
|
||||
ISBN: 978-1-4503-9051-4
|
||||
citekey: puysHardwareInTheLoopLabsSCADA2021
|
||||
itemType: conferencePaper
|
||||
publisher: Association for Computing Machinery
|
||||
location: New York, NY, USA
|
||||
pages: 1–10
|
||||
---
|
||||
#### DOI
|
||||
[10.1145/3465481.3469185](https://doi.org/10.1145/3465481.3469185)
|
||||
#### ISBN
|
||||
[978-1-4503-9051-4](https://www.isbnsearch.org/isbn/978-1-4503-9051-4)
|
||||
|
||||
### Tags:
|
||||
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [Full Text PDF](file:///home/danesabo/Zotero/storage/R5H4972I/Puys%20et%20al.%20-%202021%20-%20Hardware-In-The-Loop%20Labs%20for%20SCADA%20Cybersecurity%20.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> In this paper, we present a SCADA cybersecurity awareness and training program based on a Hands-On training using two twin cyber-ranges named WonderICS and G-ICS. These labs are built using a Hardware-In-the-Loop simulation system of the physical process developed by the two partners. The cyber-ranges allow replication of realistic Advanced Persistent Threat (APT) attacks and demonstration of known vulnerabilities, as they rely on real industrial control devices and softwares. In this work, we present both the demonstration scenarios used for awareness on WonderICS and the training programs developed for graduate students on G-ICS.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T12:05:48.405-04:00 %%
|
||||
@ -1,53 +0,0 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Federal officials investigating after pro-Iran group allegedly hacked water authority in Pennsylvania"
|
||||
year: 2023
|
||||
authors:
|
||||
|
||||
|
||||
- "Sgueglia, Sean Lyngaas, By Kristina"
|
||||
|
||||
|
||||
DOI: ""
|
||||
ISBN: ""
|
||||
citekey: "sguegliaFederalOfficialsInvestigating2023"
|
||||
itemType: "webpage"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[](https://doi.org/)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>.
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> A Pennsylvania water utility is still dealing with the fallout of pro-Iran hackers breaching some of its industrial equipment four days ago, including having to operate one of its water pump stations in manual mode, the utility’s general manager told CNN on Tuesday.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-13T16:37:25.801-04:00 %%
|
||||
@ -0,0 +1,76 @@
|
||||
---
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "Deep Unsupervised Learning using Nonequilibrium Thermodynamics"
|
||||
year: 2015
|
||||
authors:
|
||||
|
||||
|
||||
- "Sohl-Dickstein, Jascha"
|
||||
|
||||
- "Weiss, Eric A."
|
||||
|
||||
- "Maheswaranathan, Niru"
|
||||
|
||||
- "Ganguli, Surya"
|
||||
|
||||
|
||||
citekey: "sohl-dicksteinDeepUnsupervisedLearning2015"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[10.48550/arXiv.1503.03585](https://doi.org/10.48550/arXiv.1503.03585)
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
## Tags:
|
||||
#Computer-Science---Machine-Learning, #Quantitative-Biology---Neurons-and-Cognition, #Condensed-Matter---Disordered-Systems-and-Neural-Networks, #Statistics---Machine-Learning
|
||||
|
||||
>[!Abstract]
|
||||
>A central problem in machine learning involves modeling complex data-sets using highly flexible families of probability distributions in which learning, sampling, inference, and evaluation are still analytically or computationally tractable. Here, we develop an approach that simultaneously achieves both flexibility and tractability. The essential idea, inspired by non-equilibrium statistical physics, is to systematically and slowly destroy structure in a data distribution through an iterative forward diffusion process. We then learn a reverse diffusion process that restores structure in data, yielding a highly flexible and tractable generative model of the data. This approach allows us to rapidly learn, sample from, and evaluate probabilities in deep generative models with thousands of layers or time steps, as well as to compute conditional and posterior probabilities under the learned model. We additionally release an open source reference implementation of the algorithm.
|
||||
|
||||
>[!note] Markdown Notes
|
||||
>None!
|
||||
|
||||
>[!seealso] Related Papers
|
||||
>[]()
|
||||
|
||||
# Annotations
|
||||
|
||||
>[!attention] Highlight
|
||||
> *systematically and slowly destroy structure in a data distribution through an iterative forward diffusion process. We then learn a reverse diffusion process that restores structure in data, yielding a highly flexible and tractable generative model of the data.*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *robabilistic models suffer from a tradeoff between two conflicting objectives: tractability and flexibility*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *Our goal is to define a forward (or inference) diffusion process which converts any complex data distribution into a simple, tractable, distribution, and then learn a finite-time reversal of this diffusion process which defines our generative model distribution (See Figure 1).*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *For both Gaussian and binomial diffusion, for continuous diffusion (limit of small step size β) the reversal of the diffusion process has the identical functional form as the forward process (Feller, 1949).*
|
||||
>
|
||||
|
||||
>[!fail] Possibly Incorrect
|
||||
> *Since q (x(t)|x(t−1)) is a Gaussian (binomial) distribution, and if βt is small, then q (x(t−1)|x(t)) will also be a Gaussian (binomial) distribution.*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *= ∫ dx(1···T )q ( x(1···T )|x(0)) · p ( x(T )) T ∏ t=1 p (x(t−1)|x(t)) q (x(t)|x(t−1)) . (9)*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *Thus, the task of estimating a probability distribution has been reduced to the task of performing regression on the functions which set the mean and covariance of a sequence of Gaussians (or set the state flip probability for a sequence of Bernoulli trials).*
|
||||
>
|
||||
|
||||
### Imported: 2024-10-22 9:46 am
|
||||
|
||||
|
||||
@ -1,87 +0,0 @@
|
||||
---
|
||||
status: false
|
||||
dateread:
|
||||
title: "Deep Unsupervised Learning using Nonequilibrium Thermodynamics"
|
||||
year: 2015
|
||||
authors:
|
||||
|
||||
|
||||
- "Sohl-Dickstein, Jascha"
|
||||
|
||||
- "Weiss, Eric A."
|
||||
|
||||
- "Maheswaranathan, Niru"
|
||||
|
||||
- "Ganguli, Surya"
|
||||
|
||||
|
||||
DOI: "10.48550/arXiv.1503.03585"
|
||||
ISBN: ""
|
||||
citekey: "sohl-dicksteinDeepUnsupervisedLearning2015a"
|
||||
itemType: "preprint"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---
|
||||
#### DOI
|
||||
[10.48550/arXiv.1503.03585](https://doi.org/10.48550/arXiv.1503.03585)
|
||||
#### ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
#Computer-Science---Machine-Learning, #Quantitative-Biology---Neurons-and-Cognition, #Condensed-Matter---Disordered-Systems-and-Neural-Networks, #Statistics---Machine-Learning
|
||||
|
||||
**Contribution**::
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [arXiv Fulltext PDF](file:///home/danesabo/Zotero/storage/BQZ2D4RD/Sohl-Dickstein%20et%20al.%20-%202015%20-%20Deep%20Unsupervised%20Learning%20using%20Nonequilibrium%20Th.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> A central problem in machine learning involves modeling complex data-sets using highly flexible families of probability distributions in which learning, sampling, inference, and evaluation are still analytically or computationally tractable. Here, we develop an approach that simultaneously achieves both flexibility and tractability. The essential idea, inspired by non-equilibrium statistical physics, is to systematically and slowly destroy structure in a data distribution through an iterative forward diffusion process. We then learn a reverse diffusion process that restores structure in data, yielding a highly flexible and tractable generative model of the data. This approach allows us to rapidly learn, sample from, and evaluate probabilities in deep generative models with thousands of layers or time steps, as well as to compute conditional and posterior probabilities under the learned model. We additionally release an open source reference implementation of the algorithm.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>.
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
|
||||
### Imported: 2024-08-08 12:07 pm
|
||||
|
||||
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> systematically and slowly destroy structure in a data distribution through an iterative forward diffusion process. We then learn a reverse diffusion process that restores structure in data, yielding a highly flexible and tractable generative model of the data.
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> robabilistic models suffer from a tradeoff between two conflicting objectives: tractability and flexibility
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> Our goal is to define a forward (or inference) diffusion process which converts any complex data distribution into a simple, tractable, distribution, and then learn a finite-time reversal of this diffusion process which defines our generative model distribution (See Figure 1).
|
||||
|
||||
<mark style="background-color: #e56eee">Quote</mark>
|
||||
> For both Gaussian and binomial diffusion, for continuous diffusion (limit of small step size β) the reversal of the diffusion process has the identical functional form as the forward process (Feller, 1949).
|
||||
|
||||
<mark style="background-color: #ff6666">Quote</mark>
|
||||
> Since q (x(t)|x(t−1)) is a Gaussian (binomial) distribution, and if βt is small, then q (x(t−1)|x(t)) will also be a Gaussian (binomial) distribution.
|
||||
|
||||
<mark style="background-color: #2ea8e5">Quote</mark>
|
||||
> = ∫ dx(1···T )q ( x(1···T )|x(0)) · p ( x(T )) T ∏ t=1 p (x(t−1)|x(t)) q (x(t)|x(t−1)) . (9)
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> Thus, the task of estimating a probability distribution has been reduced to the task of performing regression on the functions which set the mean and covariance of a sequence of Gaussians (or set the state flip probability for a sequence of Bernoulli trials).
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-08T12:07:42.961-04:00 %%
|
||||
@ -1,87 +1,84 @@
|
||||
---
|
||||
readstatus: true
|
||||
dateread: 2024-08-13
|
||||
readstatus: false
|
||||
dateread:
|
||||
title: "SoK: Attacks on Industrial Control Logic and Formal Verification-Based Defenses"
|
||||
year: 2021
|
||||
authors:
|
||||
- Sun, Ruimin
|
||||
- Mera, Alejandro
|
||||
- Lu, Long
|
||||
- Choffnes, David
|
||||
DOI: ""
|
||||
ISBN: ""
|
||||
citekey: sunSoKAttacksIndustrial2021
|
||||
itemType: preprint
|
||||
|
||||
|
||||
- "Sun, Ruimin"
|
||||
|
||||
- "Mera, Alejandro"
|
||||
|
||||
- "Lu, Long"
|
||||
|
||||
- "Choffnes, David"
|
||||
|
||||
|
||||
citekey: "sunSoKAttacksIndustrial2021"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---
|
||||
#### DOI
|
||||
# Indexing Information
|
||||
## DOI
|
||||
[](https://doi.org/)
|
||||
#### ISBN
|
||||
## ISBN
|
||||
[](https://www.isbnsearch.org/isbn/)
|
||||
|
||||
### Tags:
|
||||
## Tags:
|
||||
|
||||
|
||||
**Contribution**::
|
||||
>[!Abstract]
|
||||
>Programmable Logic Controllers (PLCs) play a critical role in the industrial control systems. Vulnerabilities in PLC programs might lead to attacks causing devastating consequences to the critical infrastructure, as shown in Stuxnet and similar attacks. In recent years, we have seen an exponential increase in vulnerabilities reported for PLC control logic. Looking back on past research, we found extensive studies explored control logic modification attacks, as well as formal verification-based security solutions.
|
||||
|
||||
**Related**::
|
||||
|
||||
> [!LINK]
|
||||
>
|
||||
> [Sun et al. - 2021 - SoK Attacks on Industrial Control Logic and Forma.pdf](file:///home/danesabo/Zotero/storage/KSAQEB8Q/Sun%20et%20al.%20-%202021%20-%20SoK%20Attacks%20on%20Industrial%20Control%20Logic%20and%20Forma.pdf)
|
||||
> [Sun et al. - 2021 - SoK Attacks on Industrial Control Logic and Forma.pdf](file:///home/danesabo/Zotero/storage/HYUB6R2T/Sun%20et%20al.%20-%202021%20-%20SoK%20Attacks%20on%20Industrial%20Control%20Logic%20and%20Forma.pdf).
|
||||
|
||||
> [!Abstract]
|
||||
>
|
||||
> Programmable Logic Controllers (PLCs) play a critical role in the industrial control systems. Vulnerabilities in PLC programs might lead to attacks causing devastating consequences to the critical infrastructure, as shown in Stuxnet and similar attacks. In recent years, we have seen an exponential increase in vulnerabilities reported for PLC control logic. Looking back on past research, we found extensive studies explored control logic modification attacks, as well as formal verification-based security solutions.
|
||||
>.
|
||||
>
|
||||
# Notes
|
||||
>
|
||||
>[!note] Markdown Notes
|
||||
>Comment: 18 pages w/ ref, Sok, PLC, ICS, CPS, attack, formal verification
|
||||
|
||||
Comment: 18 pages w/ ref, Sok, PLC, ICS, CPS, attack, formal verification
|
||||
|
||||
Comment: 18 pages w/ ref, Sok, PLC, ICS, CPS, attack, formal verification.
|
||||
Comment: 18 pages w/ ref, Sok, PLC, ICS, CPS, attack, formal verification
|
||||
|
||||
>[!seealso] Related Papers
|
||||
>[]()
|
||||
|
||||
# Annotations
|
||||
|
||||
>[!done] Quote
|
||||
> *Industrial control systems (ICS) are subject to attacks sabotaging the physical processes, as shown in Stuxnet [33], Havex [46], TRITON [31], Black Energy [8], and the German Steel Mill [63]. PLCs are the last line in controlling and defending for these critical ICS systems.*
|
||||
>
|
||||
|
||||
>[!fail] Possibly Incorrect
|
||||
> *PLCs are the last line in controlling and defending for these critical ICS systems.*
|
||||
>
|
||||
|
||||
>[!done] Quote
|
||||
> *.1.1. Programming languages. IEC-61131 [87] defined five types of languages for PLC source code: • Ladder diagram (LD), • Structured text (ST), • Function block diagram (FBD), • Sequential function chart (SFC), • Instruction list (IL). Among them, LD, FBD, and SFC are graph-based languages. IL was deprecated in 2013. PLC programs are developed in engineering stations, which provide standard-compliant or vendor-specific Integrated Development Environments (IDEs) and compilers. Some highend PLCs also support computer-compatible languages (e.g., C, BASIC, and assembly), special high-level languages (e.g., Siemens GRAPH5 [2]), and boolean logic languages [67].*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *Unlike conventional software that follows well-documented formats, such as Executable and Linkable Format (ELF) for Linux and Portable Executable (PE) for Windows, the format of PLC binaries is often proprietary and unknown. Therefore, further exploration requires reverse engineering.*
|
||||
>
|
||||
|
||||
>[!fail] Possibly Incorrect
|
||||
> *showed*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *An extended background in Appendix A provides an example of an ST program controlling the traffic lights in a road intersection, an example of an input manipulation attack, and the process of using formal verification to detect and prevent it.*
|
||||
>
|
||||
|
||||
>[!quote] Other Highlight
|
||||
> *Formal methods have demonstrated uniqueness and practicality to the PLC industry. For example, Beckhoff TwinCat 3 and Nuclear Development Environment 2.0 have integrated safety verification during PLC program implementation [56]. Formal methods have also been used in the PLC programs controlling Ontario Power Generation, and Darlington Nuclear Power Generating Station [76]. Nevertheless, we found existing research to be ad-hoc, and the area is still new to the security community. We believe our systematization can benefit the community with recommendations for future research directions.*
|
||||
>
|
||||
|
||||
>[!attention] Highlight
|
||||
> *We also recommend future studies to develop PLC security benchmarks, including a collection of open-source programs that are vendor-independent and can represent industrial complexities, and a set of security metrics that can support concrete evaluations.*
|
||||
>
|
||||
|
||||
### Imported: 2024-10-22 9:46 am
|
||||
|
||||
|
||||
# Annotations%% begin annotations %%
|
||||
|
||||
|
||||
|
||||
### Imported: 2024-08-08 10:17 am
|
||||
|
||||
|
||||
|
||||
<mark style="background-color: #ff6666">Quote</mark>
|
||||
> showed
|
||||
|
||||
|
||||
### Imported: 2024-08-13 2:19 pm
|
||||
|
||||
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> Industrial control systems (ICS) are subject to attacks sabotaging the physical processes, as shown in Stuxnet [33], Havex [46], TRITON [31], Black Energy [8], and the German Steel Mill [63]. PLCs are the last line in controlling and defending for these critical ICS systems.
|
||||
|
||||
<mark style="background-color: #ff6666">Quote</mark>
|
||||
> PLCs are the last line in controlling and defending for these critical ICS systems.
|
||||
|
||||
<mark style="background-color: #5fb236">Quote</mark>
|
||||
> .1.1. Programming languages. IEC-61131 [87] defined five types of languages for PLC source code: • Ladder diagram (LD), • Structured text (ST), • Function block diagram (FBD), • Sequential function chart (SFC), • Instruction list (IL). Among them, LD, FBD, and SFC are graph-based languages. IL was deprecated in 2013. PLC programs are developed in engineering stations, which provide standard-compliant or vendor-specific Integrated Development Environments (IDEs) and compilers. Some highend PLCs also support computer-compatible languages (e.g., C, BASIC, and assembly), special high-level languages (e.g., Siemens GRAPH5 [2]), and boolean logic languages [67].
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> Unlike conventional software that follows well-documented formats, such as Executable and Linkable Format (ELF) for Linux and Portable Executable (PE) for Windows, the format of PLC binaries is often proprietary and unknown. Therefore, further exploration requires reverse engineering.
|
||||
|
||||
<mark style="background-color: #e56eee">Quote</mark>
|
||||
> An extended background in Appendix A provides an example of an ST program controlling the traffic lights in a road intersection, an example of an input manipulation attack, and the process of using formal verification to detect and prevent it.
|
||||
|
||||
<mark style="background-color: #e56eee">Quote</mark>
|
||||
> Formal methods have demonstrated uniqueness and practicality to the PLC industry. For example, Beckhoff TwinCat 3 and Nuclear Development Environment 2.0 have integrated safety verification during PLC program implementation [56]. Formal methods have also been used in the PLC programs controlling Ontario Power Generation, and Darlington Nuclear Power Generating Station [76]. Nevertheless, we found existing research to be ad-hoc, and the area is still new to the security community. We believe our systematization can benefit the community with recommendations for future research directions.
|
||||
|
||||
<mark style="background-color: #ffd400">Quote</mark>
|
||||
> We also recommend future studies to develop PLC security benchmarks, including a collection of open-source programs that are vendor-independent and can represent industrial complexities, and a set of security metrics that can support concrete evaluations.
|
||||
|
||||
|
||||
%% end annotations %%
|
||||
|
||||
%% Import Date: 2024-08-13T14:19:12.069-04:00 %%
|
||||
|
||||
@ -9,4 +9,8 @@ There's a lot of papers that do 'robust control synthesis and verification' but
|
||||
|
||||
I hate robot people. They use the word robust too softly.
|
||||
|
||||
2.
|
||||
2. [[matusuRegionsRobustRelative2023]]
|
||||
1. This plant has a structured perturbation
|
||||
2. The stuff they do with PI is kind of cool I guess
|
||||
3. No formal methods
|
||||
4. They reinvent the factor of safety. Silly
|
||||
Loading…
x
Reference in New Issue
Block a user