Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Personenbezug bei dynamischen IP-Adressen – Anmerkung zur Entscheidung des EuGH vom 19.10.2016
Limiting The Impact of Stealthy Attacks on Industrial Control Systems
While attacks on information systems have for most prac-
tical purposes binary outcomes (information was manipulated/eavesdropped, or not), attacks manipulating the sensor or control signals of Industrial Control Systems (ICS) can be tuned by the attacker to cause a continuous spectrum in damages. Attackers that want to remain undetected can attempt to hide their manipulation of the system by following closely the expected behavior of the system, while injecting just enough false information at each time step to achieve their goals.
In this work, we study if physics-based attack detection
can limit the impact of such stealthy attacks. We start with a comprehensive review of related work on attack detection schemes in the security and control systems community. We then show that many of these works use detection schemes that are not limiting the impact of stealthy attacks. We propose a new metric to measure the impact of stealthy attacks and how they relate to our selection on an upper bound on false alarms. We finally show that the impact of such attacks can be mitigated in several cases by the proper combination and configuration of detection schemes. We demonstrate the effectiveness of our algorithms through simulations and experiments using real ICS testbeds and real ICS system
Automated analysis of security protocols with global state
Security APIs, key servers and protocols that need to keep the
status of transactions, require to maintain a global, non-monotonic
state, e.g., in the form of a database or register. However, most
existing automated verification tools do not support the analysis of
such stateful security protocols -- sometimes because of fundamental
reasons, such as the encoding of the protocol as Horn clauses, which
are inherently monotonic. A notable exception is the recent tamarin
prover which allows specifying protocols as multiset rewrite (msr)
rules, a formalism expressive enough to encode state. As multiset
rewriting is a ``low-level'' specification language with no direct
support for concurrent message passing, encoding protocols correctly
is a difficult and error-prone process.
We propose a process calculus which is a variant of the applied pi
calculus with constructs for manipulation of a global state by
processes running in parallel. We show that this language can be
translated to msr rules whilst preserving all security properties
expressible in a dedicated first-order logic for security
properties. The translation has been implemented in a prototype tool
which uses the tamarin prover as a backend. We apply the tool to
several case studies among which a simplified fragment of PKCS\\#11,
the Yubikey security token, and an optimistic contract signing
protocol