Wyniki wyszukiwania - BazTech

Ograniczanie wyników

3 Fundamenta Informaticae

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: non-interference

Sortuj według:

Ogranicz wyniki do:

Persistent Stochastic Non-Interference

Hillston Jane, Marin Andrea, Piazza Carla, Rossi Sabina

Fundamenta Informaticae

2021

Vol. 181, nr 1

1--35

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). We propose a quantitative extension of the Non-Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI : one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.

A Causal View on Non-Interference

Baldan P., Carraro A.

Fundamenta Informaticae

2015

Vol. 140, nr 1

1--38

The concept of non-interference has been introduced to characterise the absence of undesired information flows in a computing system. Although it is often explained referring to an informal notion of causality - the activity involving the part of the system with higher level of confidentiality should not cause any observable effect at lower levels - it is almost invariably formalised in terms of interleaving semantics. Here we focus on Petri nets and on the BNDC (Bisimilarity-based Non-Deducibility on Composition) property, a formalisation of non-interference widely studied in the literature. We show that BNDC admits natural characterisations based on the unfolding semantics - a classical true concurrent semantics for Petri nets - in terms of causalities and conflicts between high and low level activities. This leads to algorithms for checking BNDC on various classes of Petri nets, based on the construction of suitable complete prefixes of the unfolding. We also developed a prototype tool UBIC (Unfolding-Based Interference Checker), working on safe Petri nets, which provides promising results in terms of efficiency.

Gained and Excluded Private Actions by Process Observations

Gruska D.P.

Fundamenta Informaticae

2011

Vol. 109, nr 3

281-295

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.