-
VeriBlock: A Blockchain-Based Verifiable Trust Management Architecture with Provable Interactions
Authors:
Shantanu Pal,
Ambrose Hill,
Tahiry Rabehaja,
Michael Hitchens
Abstract:
There has been considerable advancement in the use of blockchain for trust management in large-scale dynamic systems. In such systems, blockchain is mainly used to store the trust score or trust-related information of interactions among the various entities. However, present trust management architectures using blockchain lack verifiable interactions among the entities on which the trust score is…
▽ More
There has been considerable advancement in the use of blockchain for trust management in large-scale dynamic systems. In such systems, blockchain is mainly used to store the trust score or trust-related information of interactions among the various entities. However, present trust management architectures using blockchain lack verifiable interactions among the entities on which the trust score is calculated. In this paper, we propose a blockchain-based trust management framework that allows independent trust providers to implement different trust metrics on a common set of trust evidence and provide individual trust value. We employ geo-location as proof of interaction. Some of the existing proposals rely upon geo-location data, but they do not support trust calculation by multiple trust providers. Instead, they can only support a centralised system. Our proposed architecture does not depend upon a single centralised third-party entity to ensure trusted interactions. Our architecture is supported by provable interactions that can easily be verified using blockchain. Therefore, it allows a high degree of confidence in trust management by ensuring the actual interactions between the entities. We provide a detailed design and development of the architecture using real-world use case examples. The proof of prototype was implemented on the Ethereum blockchain platform. Experimental results demonstrate that the employment of independent trust providers adequately provides a high degree of trust scores and that the proposed architecture can be used in a real-world environment.
△ Less
Submitted 12 June, 2022;
originally announced June 2022.
-
Controlling Resource Allocation using Blockchain-Based Delegation
Authors:
Shantanu Pal,
Ambrose Hill,
Tahiry Rabehaja,
Michael Hitchens
Abstract:
Allocation of resources and their control over multiple organisations is challenging. This is especially true for a large-scale and dynamic system like the Internet of Things (IoT). One of the core issues in such a system is the provision of secure access control. In particular, transfer of access rights from one entity to another in a secure, flexible and fine-grained manner. In this paper, we pr…
▽ More
Allocation of resources and their control over multiple organisations is challenging. This is especially true for a large-scale and dynamic system like the Internet of Things (IoT). One of the core issues in such a system is the provision of secure access control. In particular, transfer of access rights from one entity to another in a secure, flexible and fine-grained manner. In this paper, we present a multi-organisational delegation framework using blockchain. Our framework takes advantage of blockchain smart contracts to define the interactions and resource allocation between the consortium of organisations. We show the feasibility of our solution in a real-world scenario using the allocation of transportation credits in a multi-level organisational setting as a use-case. We provide proof of implementation of the proposed framework using the Hyperledger Fabric blockchain platform. Our results indicate that the proposed framework is efficient and can be used for city-wide transport, potentially even scale country-wide with a shared blockchain with complex access control rules. It also bestows better transparency to the delegation of access rights and control over the employees' transportation access for the organisations.
△ Less
Submitted 3 October, 2021;
originally announced October 2021.
-
A Blockchain-Based Trust Management Framework with Verifiable Interactions
Authors:
Shantanu Pal,
Ambrose Hill,
Tahiry Rabehaja,
Michael Hitchens
Abstract:
There has been tremendous interest in the development of formal trust models and metrics through the use of analytics (e.g., Belief Theory and Bayesian models), logics (e.g., Epistemic and Subjective Logic) and other mathematical models. The choice of trust metric will depend on context, circumstance and user requirements and there is no single best metric for use in all circumstances. Where diffe…
▽ More
There has been tremendous interest in the development of formal trust models and metrics through the use of analytics (e.g., Belief Theory and Bayesian models), logics (e.g., Epistemic and Subjective Logic) and other mathematical models. The choice of trust metric will depend on context, circumstance and user requirements and there is no single best metric for use in all circumstances. Where different users require different trust metrics to be employed the trust score calculations should still be based on all available trust evidence. Trust is normally computed using past experiences but, in practice (especially in centralised systems), the validity and accuracy of these experiences are taken for granted. In this paper, we provide a formal framework and practical blockchain-based implementation that allows independent trust providers to implement different trust metrics in a distributed manner while still allowing all trust providers to base their calculations on a common set of trust evidence. Further, our design allows experiences to be provably linked to interactions without the need for a central authority. This leads to the notion of evidence-based trust with provable interactions. Leveraging blockchain allows the trust providers to offer their services in a competitive manner, charging fees while users are provided with payments for recording experiences. Performance details of the blockchain implementation are provided.
△ Less
Submitted 9 June, 2021;
originally announced June 2021.
-
Abstract Hidden Markov Models: a monadic account of quantitative information flow
Authors:
Annabelle McIver,
Carroll Morgan,
Tahiry Rabehaja
Abstract:
Hidden Markov Models, HMM's, are mathematical models of Markov processes with state that is hidden, but from which information can leak. They are typically represented as 3-way joint-probability distributions.
We use HMM's as denotations of probabilistic hidden-state sequential programs: for that, we recast them as `abstract' HMM's, computations in the Giry monad $\mathbb{D}$, and we equip them…
▽ More
Hidden Markov Models, HMM's, are mathematical models of Markov processes with state that is hidden, but from which information can leak. They are typically represented as 3-way joint-probability distributions.
We use HMM's as denotations of probabilistic hidden-state sequential programs: for that, we recast them as `abstract' HMM's, computations in the Giry monad $\mathbb{D}$, and we equip them with a partial order of increasing security. However to encode the monadic type with hiding over some state $\mathcal{X}$ we use $\mathbb{D}\mathcal{X}\to \mathbb{D}^2\mathcal{X}$ rather than the conventional $\mathcal{X}{\to}\mathbb{D}\mathcal{X}$ that suffices for Markov models whose state is not hidden. We illustrate the $\mathbb{D}\mathcal{X}\to \mathbb{D}^2\mathcal{X}$ construction with a small Haskell prototype.
We then present uncertainty measures as a generalisation of the extant diversity of probabilistic entropies, with characteristic analytic properties for them, and show how the new entropies interact with the order of increasing security. Furthermore, we give a `backwards' uncertainty-transformer semantics for HMM's that is dual to the `forwards' abstract HMM's - it is an analogue of the duality between forwards, relational semantics and backwards, predicate-transformer semantics for imperative programs with demonic choice.
Finally, we argue that, from this new denotational-semantic viewpoint, one can see that the Dalenius desideratum for statistical databases is actually an issue in compositionality. We propose a means for taking it into account.
△ Less
Submitted 28 March, 2019; v1 submitted 4 August, 2017;
originally announced August 2017.
-
Compositional security and collateral leakage
Authors:
N. Bordenabe,
A. McIver,
C Morgan,
T. Rabehaja
Abstract:
In quantitative information flow we say that program $Q$ is "at least as secure as" $P$ just when the amount of secret information flowing from $Q$ is never more than flows from $P$, with of course a suitable quantification of "flow". This secure-refinement order $\sqsubseteq$ is compositional just when $P{\sqsubseteq}Q$ implies ${\cal C}(P){\sqsubseteq}{\cal C}(Q)$ for any context ${\cal C}$, aga…
▽ More
In quantitative information flow we say that program $Q$ is "at least as secure as" $P$ just when the amount of secret information flowing from $Q$ is never more than flows from $P$, with of course a suitable quantification of "flow". This secure-refinement order $\sqsubseteq$ is compositional just when $P{\sqsubseteq}Q$ implies ${\cal C}(P){\sqsubseteq}{\cal C}(Q)$ for any context ${\cal C}$, again with a suitable definition of "context".
Remarkable however is that leaks caused by executing $P,Q$ might not be limited to their declared variables: they might impact correlated secrets in variables declared and initialised in some broader context to which $P,Q$ do not refer even implicitly. We call such leaks collateral because their effect is felt in domains of which (the programmers of) $P, Q$ might be wholly unaware: our inspiration is the "Dalenius" phenomenon for statistical databases.
We show that a proper treatment of these collateral leaks is necessary for a compositional program semantics for read/write "open" programs. By adapting a recent Hidden-Markov denotational model for non-interference security, so that it becomes "collateral aware", we give techniques and examples (e.g.\ public-key encryption) to show how collateral leakage can be calculated and then bounded in its severity.
△ Less
Submitted 18 April, 2016;
originally announced April 2016.
-
Probabilistic Rely-guarantee Calculus
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach which combines and adapts probabilistic Kleene algebras with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rule…
▽ More
Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach which combines and adapts probabilistic Kleene algebras with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rules built on top of that semantics. In particular, we show how to obtain bounds on probabilities by deriving rely-guarantee rules within the true-concurrent denotational semantics. The use of these rules is illustrated by a detailed verification of a simple probabilistic concurrent program: a faulty Eratosthenes sieve.
△ Less
Submitted 2 June, 2015; v1 submitted 1 September, 2014;
originally announced September 2014.
-
An Event Structure Model for Probabilistic Concurrent Kleene Algebra
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen's work on probabilistic concurrency and Varacca's probabilistic prime event structures. The event structures are compared with a true-concurrent version of Segala's probabilistic simulation. Finally, the algebraic properties of the…
▽ More
We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen's work on probabilistic concurrency and Varacca's probabilistic prime event structures. The event structures are compared with a true-concurrent version of Segala's probabilistic simulation. Finally, the algebraic properties of the model are summarised to the extent that they can be used to derive techniques such as probabilistic rely/guarantee inference rules.
△ Less
Submitted 8 October, 2013;
originally announced October 2013.
-
Probabilistic Concurrent Kleene Algebra
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
We provide an extension of concurrent Kleene algebras to account for probabilistic properties. The algebra yields a unified framework containing nondeterminism, concurrency and probability and is sound with respect to the set of probabilistic automata modulo probabilistic simulation. We use the resulting algebra to generalise the algebraic formulation of a variant of Jones' rely/guarantee calculus…
▽ More
We provide an extension of concurrent Kleene algebras to account for probabilistic properties. The algebra yields a unified framework containing nondeterminism, concurrency and probability and is sound with respect to the set of probabilistic automata modulo probabilistic simulation. We use the resulting algebra to generalise the algebraic formulation of a variant of Jones' rely/guarantee calculus.
△ Less
Submitted 11 June, 2013;
originally announced June 2013.
-
Weak Concurrent Kleene Algebra with Application to Algebraic Verification
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
We propose a generalisation of concurrent Kleene algebra \cite{Hoa09} that can take account of probabilistic effects in the presence of concurrency. The algebra is proved sound with respect to a model of automata modulo a variant of rooted $η$-simulation equivalence. Applicability is demonstrated by algebraic treatments of two examples: algebraic may testing and Rabin's solution to the choice coor…
▽ More
We propose a generalisation of concurrent Kleene algebra \cite{Hoa09} that can take account of probabilistic effects in the presence of concurrency. The algebra is proved sound with respect to a model of automata modulo a variant of rooted $η$-simulation equivalence. Applicability is demonstrated by algebraic treatments of two examples: algebraic may testing and Rabin's solution to the choice coordination problem.
△ Less
Submitted 30 January, 2013;
originally announced January 2013.
