Information flow testing
Fundamenta Informaticae, Vol. 128, No. 1-2 (2013), s. 81-95
ABSTRACT:
Opacity testing is formalized and studied. We specify opacity testers as well as tested systems by (timed) process algebras. We model various testers according to how sophisticated observations of tested system they can make and which kind of conclusions they can obtain. We use this technique to define several realistic security properties. The properties are studied and compared with other security concepts.
(pdf)
Quantification of positive and negative attacker's information
Fundamenta Informaticae, Vol. 120, No. 3-4 (2012), s. 311-324
ABSTRACT:
Different techniques for expressing an amount of information on
secrete data which can be obtained by a process observation are
presented. They are based on information theory and they express
certainty about
sets of private actions which execution is guaranteed by
a given observation and sets of actions which execution is excluded
by a given observation. Moreover, the case when an intruder has same
preliminary belief on secrete data is discussed. It is shown how the
presented technique could be applied for such case. As regards
working formalism, probabilistic process algebra is used for
description of systems as well as attacker's belief.
(pdf)
Informational analysis of security and integrity
Fundamenta Informaticae, Vol. 120, No. 3-4 (2012), s. 295-309
ABSTRACT:
Formalisms for analysis of systems of various nature specified by
process algebras are proposed. They allow us to formalize security
properties based on an absence of information flow and properties on
system's integrity. Resulting properties are compared and discussed.
We present also quantification of these properties by means of
information theory.
(pdf)
Gained and Excluded Private Actions by Process Observations
Fundamenta Informaticae, Vol. 109, No. 3 (2011), pp. 281-295
ABSTRACT: A general framework for defining security properties is presented.
It allows us to model many traditional security properties as well
as to define new ones. The framework is based on process algebras
contexts and processes relations. By appropriate choice of both of
them we can model also probabilistic and quantified security
properties. (pdf)
Process Algebra Contexts Security Properties
Fundamenta Informaticae, Vol. 102, No. 1 (2010), pp 63-76
ABSTRACT: Formalisms for description how much information on private actions
can be obtained by observing public ones are presented. Two sets of
private actions are considered. The set of actions which execution
is guaranteed according to observations and the set of actions
which execution is excluded according to observations. Since
information flows could be realized also by means of different
covert channels as time, termination and divergence this possibility
is considered as well. Both qualitative and quantitative dimensions
of the flow are considered.
(pdf)
A notion of biological diagnosability inspired by the notion of
opacity in systems security
Fundamenta Informaticae, Vol. 102, No. 1 (2010), pp 19-34
ABSTRACT:
A formal model for diagnostics of biological systems modelled as P systems is
presented. We assume the presence of some biologically motivated
changes (frequently pathological) in the systems behavior and investigate when
these changes could be diagnosed by an external observer by exploiting
some techniques originally developed for reasoning on system security.
(pdf)
Quantifying Security for Timed Process Algebras
Fundamenta Informaticae, Vol. 93, No. 1-3 (2009),
pp 155-169
ABSTRACT:
A quantification of process's security by quantification of an
amount of information flow is defined and studied in the framework
of timed process algebras. The resulting quantified security is
compared with other (qualitative) security notions. Unprecise and
limited observations are defined and discussed.
(pdf)
Security in a Model for Long--running Transactions
Fundamenta Informaticae.
Vol. 85, No. 1-4 (2008), pp 189-203, 2008
ABSTRACT:
Communicating Hierarchical Transaction-based Timed Automata have been
introduced to model systems performing long--running transactions.
Here, for these automata a security concept is introduced, which is based on a notion of opacity and on the assumption that an attacker can not only observe public system activities, but also cause abortion of some of them. Different intruder capabilities as well as different kinds of opacity are defined and the resulting security properties are investigated. Security of long--running transactions is defined by the mentioned notion of opacity and conditions for compositionality are established.
(pdf)
Probabilistic Information Flow Security
Fundamenta Informaticae.
Vol. 85, No. 1-4 (2008), pp 173-187, 2008
ABSTRACT:
A formal model for description of probabilistic timing attacks is
presented and studied. It is based on a probabilistic timed process
algebra, on observations (mappings which make visible only a part of
system behavior) and on an information flow. The resulting security
properties are studied and compared with other security concepts.
(pdf)
Observation Based System Security
Fundamenta Informaticae, 79 (2007), Numbers 3-4, pp. 335-346, 2007
ABSTRACT:
A formal model for description of passive and active timing attacks
is presented, studied and compared with other security concepts. It
is based on a timed process algebra and on a concept of observations
which make only a part of system behaviour visible. From this
partial information which contains also timing of actions an
intruder tries to deduce some private system activities.
(pdf)
Information-Flow Attacks Based on Limited Observations
Proc. of PSI'06, Springer Verlag, LNCS 4378, Berlin, pp
219-230, 2007
ABSTRACT:
Two formal models for description of timing attacks are presented,
studied and compared with other security concepts. The models are
based on a timed process algebra and on a concept of observations
which make visible only a part of a system behaviour.
An intruder tries to deduce some private system activities
from this partial information which contains also timing of actions.
To obtain realistic security characterizations some limitations
on observational power of the intruder are applied.
It is
assumed that the intruder has only limited time window to perform
the attack or time of action occurrences can be measured only with a
given limited precision.
(pdf)
Network Information Flow
Fundamenta Informaticae,
Volume 72, Numbers 1-3, pp 167-180, 2006
ABSTRACT:
A formal model for an analysis of an information flow in
interconnection networks is presented. It is based on timed process
algebra which can express also network properties. The information
flow is based on a concept of deducibility on composition.
Robustness of systems against network timing attacks is defined. A
variety of different security properties which reflect different
security requirements are defined and investigated.
(pdf)
Process Algebras for Network Communication
Fundamenta Informaticae, 45(4), pp 359-378, 2001
ABSTRACT:
Critical issues that arise when process algebras are used
for protocol specifications are discussed. To overcome some
of these problems, a process algebra for protocol
specifications is presented. It is based on Milner's
Calculus of Communicating Systems, which is enriched by time
and network reasoning. Several bisimulation based semantics
for the calculus are defined and their properties are discussed.
(pdf)