Showing 1–16 of 16 results for author: Huth, M

Leverage Staking with Liquid Staking Derivatives (LSDs): Opportunities and Risks

Authors: Xihan Xiong, Zhipeng Wang, Xi Chen, William Knottenbelt, Michael Huth

Abstract: In the Proof of Stake (PoS) Ethereum ecosystem, users can stake ETH on Lido to receive stETH, a Liquid Staking Derivative (LSD) that represents staked ETH and accrues staking rewards. LSDs improve the liquidity of staked assets by facilitating their use in secondary markets, such as for collateralized borrowing on Aave or asset exchanges on Curve. The composability of Lido, Aave, and Curve enables… ▽ More In the Proof of Stake (PoS) Ethereum ecosystem, users can stake ETH on Lido to receive stETH, a Liquid Staking Derivative (LSD) that represents staked ETH and accrues staking rewards. LSDs improve the liquidity of staked assets by facilitating their use in secondary markets, such as for collateralized borrowing on Aave or asset exchanges on Curve. The composability of Lido, Aave, and Curve enables an emerging strategy known as leverage staking, where users supply stETH as collateral on Aave to borrow ETH and then acquire more stETH. This can be done directly by initially staking ETH on Lido or indirectly by swap** ETH for stETH on Curve. While this iterative process enhances financial returns, it also introduces potential risks. This paper explores the opportunities and risks of leverage staking. We establish a formal framework for leverage staking with stETH and identify 442 such positions on Ethereum over 963 days. These positions represent a total volume of 537,123 ETH (877m USD). Our data reveal that the majority (81.7%) of leverage staking positions achieved an Annual Percentage Rate (APR) higher than that of conventional staking on Lido. Despite the high returns, we also recognize the risks of leverage staking. From the Terra crash incident, we understand that token devaluation can greatly impact the market. Therefore, we conduct stress tests under extreme conditions, particularly during stETH devaluations, to thoroughly evaluate the associated risks. Our simulations indicate that leverage staking can exacerbate the risk of cascading liquidations by introducing additional selling pressures from liquidation and deleveraging activities. Moreover, this strategy poses broader systemic risks as it undermines the stability of ordinary positions by intensifying their liquidations. △ Less

Submitted 23 May, 2024; v1 submitted 28 November, 2023; originally announced January 2024.

Extreme compression of sentence-transformer ranker models: faster inference, longer battery life, and less storage on edge devices

Authors: Amit Chaulwar, Lukas Malik, Maciej Krajewski, Felix Reichel, Leif-Nissen Lundbæk, Michael Huth, Bartlomiej Matejczyk

Abstract: Modern search systems use several large ranker models with transformer architectures. These models require large computational resources and are not suitable for usage on devices with limited computational resources. Knowledge distillation is a popular compression technique that can reduce the resource needs of such models, where a large teacher model transfers knowledge to a small student model.… ▽ More Modern search systems use several large ranker models with transformer architectures. These models require large computational resources and are not suitable for usage on devices with limited computational resources. Knowledge distillation is a popular compression technique that can reduce the resource needs of such models, where a large teacher model transfers knowledge to a small student model. To drastically reduce memory requirements and energy consumption, we propose two extensions for a popular sentence-transformer distillation procedure: generation of an optimal size vocabulary and dimensionality reduction of the embedding dimension of teachers prior to distillation. We evaluate these extensions on two different types of ranker models. This results in extremely compressed student models whose analysis on a test dataset shows the significance and utility of our proposed extensions. △ Less

Submitted 29 June, 2022; originally announced July 2022.

Secure Bayesian Federated Analytics for Privacy-Preserving Trend Detection

Authors: Amit Chaulwar, Michael Huth

Abstract: Federated analytics has many applications in edge computing, its use can lead to better decision making for service provision, product development, and user experience. We propose a Bayesian approach to trend detection in which the probability of a keyword being trendy, given a dataset, is computed via Bayes' Theorem; the probability of a dataset, given that a keyword is trendy, is computed throug… ▽ More Federated analytics has many applications in edge computing, its use can lead to better decision making for service provision, product development, and user experience. We propose a Bayesian approach to trend detection in which the probability of a keyword being trendy, given a dataset, is computed via Bayes' Theorem; the probability of a dataset, given that a keyword is trendy, is computed through secure aggregation of such conditional probabilities over local datasets of users. We propose a protocol, named SAFE, for Bayesian federated analytics that offers sufficient privacy for production grade use cases and reduces the computational burden of users and an aggregator. We illustrate this approach with a trend detection experiment and discuss how this approach could be extended further to make it production-ready. △ Less

Submitted 28 July, 2021; originally announced July 2021.

Comments: 10 pages, 1 figure

Two and Three-Party Digital Goods Auctions: Scalable Privacy Analysis

Authors: Patrick Ah-Fat, Michael Huth

Abstract: A digital goods auction is a type of auction where potential buyers bid the maximal price that they are willing to pay for a certain item, which a seller can produce at a negligible cost and in unlimited quantity. To maximise her benefits, the aim for the seller is to find the optimal sales price, which every buyer whose bid is not lower will pay. For fairness and privacy purposes, buyers may be c… ▽ More A digital goods auction is a type of auction where potential buyers bid the maximal price that they are willing to pay for a certain item, which a seller can produce at a negligible cost and in unlimited quantity. To maximise her benefits, the aim for the seller is to find the optimal sales price, which every buyer whose bid is not lower will pay. For fairness and privacy purposes, buyers may be concerned about protecting the confidentiality of their bids. Secure Multi-Party Computation is a domain of Cryptography that would allow the seller to compute the optimal sales price while guaranteeing that the bids remain secret. Paradoxically, as a function of the buyers' bids, the sales price inevitably reveals some private information. Generic frameworks and entropy-based techniques based on Quantitative Information Flow have been developed in order to quantify and restrict those leakages. Due to their combinatorial nature, these techniques do not scale to large input spaces. In this work, we aim at scaling those privacy analyses to large input spaces in the particular case of digital goods auctions. We derive closed-form formulas for the posterior min-entropy of private inputs in two and three-party auctions, which enables us to effectively quantify the information leaks for arbitrarily large input spaces. We also provide supportive experimental evidence that enables us to formulate a conjecture that would allow us to extend our results to any number of parties. △ Less

Submitted 20 September, 2020; originally announced September 2020.

Owner-centric sharing of physical resources, data, and data-driven insights in digital ecosystems

Authors: Kwok Cheung, Michael Huth, Laurence Kirk, Leif-Nissen Lundbæk, Rodolphe Marques, Jan Petsche

Abstract: We are living in an age in which digitization will connect more and more physical assets with IT systems and where IoT endpoints will generate a wealth of valuable data. Companies, individual users, and organizations alike therefore have the need to control their own physical or non-physical assets and data sources. At the same time, they recognize the need for, and opportunity to, share access to… ▽ More We are living in an age in which digitization will connect more and more physical assets with IT systems and where IoT endpoints will generate a wealth of valuable data. Companies, individual users, and organizations alike therefore have the need to control their own physical or non-physical assets and data sources. At the same time, they recognize the need for, and opportunity to, share access to such data and digitized physical assets. This paper sets out our technology vision for such sharing ecosystems, reports initial work in that direction, identifies challenges for realizing this vision, and seeks feedback and collaboration from the academic access-control community in that R\&D space. △ Less

Submitted 4 June, 2019; originally announced June 2019.

Journal ref: ACM SACMAT 2019: 73-81

Scalable Information-Flow Analysis of Secure Three-Party Affine Computations

Authors: Patrick Ah-Fat, Michael Huth

Abstract: Elaborate protocols in Secure Multi-party Computation enable several participants to compute a public function of their own private inputs while ensuring that no undesired information leaks about the private inputs, and without resorting to any trusted third party. However, the public output of the computation inevitably leaks some information about the private inputs. Recent works have introduced… ▽ More Elaborate protocols in Secure Multi-party Computation enable several participants to compute a public function of their own private inputs while ensuring that no undesired information leaks about the private inputs, and without resorting to any trusted third party. However, the public output of the computation inevitably leaks some information about the private inputs. Recent works have introduced a framework and proposed some techniques for quantifying such information flow. Yet, owing to their complexity, those methods do not scale to practical situations that may involve large input spaces. The main contribution of the work reported here is to formally investigate the information flow captured by the min-entropy in the particular case of secure three-party computations of affine functions in order to make its quantification scalable to realistic scenarios. To this end, we mathematically derive an explicit formula for this entropy under uniform prior beliefs about the inputs. We show that this closed-form expression can be computed in time constant in the inputs sizes and logarithmic in the coefficients of the affine function. Finally, we formulate some theoretical bounds for this privacy leak in the presence of non-uniform prior beliefs. △ Less

Submitted 3 January, 2019; originally announced January 2019.

Future developments in cyber risk assessment for the internet of things

Authors: Petar Radanliev, David Charles De Roure, Razvan Nicolescu, Michael Huth, Rafael Mantilla Montalvo, Stacy Cannady, Peter Burnap

Abstract: This article is focused on the economic impact assessment of Internet of Things (IoT) and its associated cyber risks vectors and vertices - a reinterpretation of IoT verticals. We adapt to IoT both the Cyber Value at Risk model, a well-established model for measuring the maximum possible loss over a given time period, and the MicroMort model, a widely used model for predicting uncertainty through… ▽ More This article is focused on the economic impact assessment of Internet of Things (IoT) and its associated cyber risks vectors and vertices - a reinterpretation of IoT verticals. We adapt to IoT both the Cyber Value at Risk model, a well-established model for measuring the maximum possible loss over a given time period, and the MicroMort model, a widely used model for predicting uncertainty through units of mortality risk. The resulting new IoT MicroMort for calculating IoT risk is tested and validated with real data from the BullGuard's IoT Scanner - over 310,000 scans - and the Garner report on IoT connected devices. Two calculations are developed, the current state of IoT cyber risk and the future forecasts of IoT cyber risk. Our work therefore advances the efforts of integrating cyber risk impact assessments and offer a better understanding of economic impact assessment for IoT cyber risk. △ Less

Submitted 13 September, 2018; originally announced September 2018.

Comments: http://doi.org/10.1016/J.COMPIND.2018.08.002

Ontology-Based Reasoning about the Trustworthiness of Cyber-Physical Systems

Authors: Marcello Balduccini, Edward Griffor, Michael Huth, Claire Vishik, Martin Burns, David Wollman

Abstract: It has been challenging for the technical and regulatory communities to formulate requirements for trustworthiness of the cyber-physical systems (CPS) due to the complexity of the issues associated with their design, deployment, and operations. The US National Institute of Standards and Technology (NIST), through a public working group, has released a CPS Framework that adopts a broad and integrat… ▽ More It has been challenging for the technical and regulatory communities to formulate requirements for trustworthiness of the cyber-physical systems (CPS) due to the complexity of the issues associated with their design, deployment, and operations. The US National Institute of Standards and Technology (NIST), through a public working group, has released a CPS Framework that adopts a broad and integrated view of CPS and positions trustworthiness among other aspects of CPS. This paper takes the model created by the CPS Framework and its further developments one step further, by applying ontological approaches and reasoning techniques in order to achieve greater understanding of CPS. The example analyzed in the paper demonstrates the enrichment of the original CPS model obtained through ontology and reasoning and its ability to deliver additional insights to the developers and operators of CPS. △ Less

Submitted 20 March, 2018; originally announced March 2018.

Comments: IET PETRAS 2018 conference

Optimal Accuracy-Privacy Trade-Off for Secure Multi-Party Computations

Authors: Patrick Ah-Fat, Michael Huth

Abstract: The purpose of Secure Multi-Party Computation is to enable protocol participants to compute a public function of their private inputs while kee** their inputs secret, without resorting to any trusted third party. However, opening the public output of such computations inevitably reveals some information about the private inputs. We propose a measure generalising both Renyi entropy and g-entropy… ▽ More The purpose of Secure Multi-Party Computation is to enable protocol participants to compute a public function of their private inputs while kee** their inputs secret, without resorting to any trusted third party. However, opening the public output of such computations inevitably reveals some information about the private inputs. We propose a measure generalising both Renyi entropy and g-entropy so as to quantify this information leakage. In order to control and restrain such information flows, we introduce the notion of function substitution which replaces the computation of a function that reveals sensitive information with that of an approximate function. We exhibit theoretical bounds for the privacy gains that this approach provides and experimentally show that this enhances the confidentiality of the inputs while controlling the distortion of computed output values. Finally, we investigate the inherent compromise between accuracy of computation and privacy of inputs and we demonstrate how to realise such optimal trade-offs. △ Less

Submitted 1 March, 2018; originally announced March 2018.

Constrained Bayesian Networks: Theory, Optimization, and Applications

Authors: Paul Beaumont, Michael Huth

Abstract: We develop the theory and practice of an approach to modelling and probabilistic inference in causal networks that is suitable when application-specific or analysis-specific constraints should inform such inference or when little or no data for the learning of causal network structure or probability values at nodes are available. Constrained Bayesian Networks generalize a Bayesian Network such tha… ▽ More We develop the theory and practice of an approach to modelling and probabilistic inference in causal networks that is suitable when application-specific or analysis-specific constraints should inform such inference or when little or no data for the learning of causal network structure or probability values at nodes are available. Constrained Bayesian Networks generalize a Bayesian Network such that probabilities can be symbolic, arithmetic expressions and where the meaning of the network is constrained by finitely many formulas from the theory of the reals. A formal semantics for constrained Bayesian Networks over first-order logic of the reals is given, which enables non-linear and non-convex optimisation algorithms that rely on decision procedures for this logic, and supports the composition of several constrained Bayesian Networks. A non-trivial case study in arms control, where few or no data are available to assess the effectiveness of an arms inspection process, evaluates our approach. An open-access prototype implementation of these foundations and their algorithms uses the SMT solver Z3 as decision procedure, leverages an open-source package for Bayesian inference to symbolic computation, and is evaluated experimentally. △ Less

Submitted 15 May, 2017; originally announced May 2017.

Comments: 43 pages, 18 figures

Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving

Authors: Andrea Callia D'Iddio, Michael Huth

Abstract: Optimization of Mixed-Integer Non-Linear Programming (MINLP) supports important decisions in applications such as Chemical Process Engineering. But current solvers have limited ability for deductive reasoning or the use of domain-specific theories, and the management of integrality constraints does not yet exploit automated reasoning tools such as SMT solvers. This seems to limit both scalability… ▽ More Optimization of Mixed-Integer Non-Linear Programming (MINLP) supports important decisions in applications such as Chemical Process Engineering. But current solvers have limited ability for deductive reasoning or the use of domain-specific theories, and the management of integrality constraints does not yet exploit automated reasoning tools such as SMT solvers. This seems to limit both scalability and reach of such tools in practice. We therefore present a tool, ManyOpt, for MINLP optimization that enables experimentation with reduction techniques which transform a MINLP problem to feasibility checking realized by an SMT solver. ManyOpt is similar to the SAT solver ManySAT in that it runs a specified number of such reduction techniques in parallel to get the strongest result on a given MINLP problem. The tool is implemented in layers, which we may see as features and where reduction techniques are feature vectors. Some of these features are inspired by known MINLP techniques whereas others are novel and specific to SMT. Our experimental results on standard benchmarks demonstrate the benefits of this approach. The tool supports a variety of SMT solvers and is easily extensible with new features, courtesy of its layered structure. For example, logical formulas for deductive reasoning are easily added to constrain further the optimization of a MINLP problem of interest. △ Less

Submitted 4 February, 2017; originally announced February 2017.

Comments: 17 pages, 3 figures, link to open research data and code available

Optimizing Governed Blockchains for Financial Process Authentications

Authors: Leif-Nissen Lundbaek, Andrea Callia D'Iddio, Michael Huth

Abstract: We propose the formal study of governed blockchains that are owned and controlled by organizations and that neither create cryptocurrencies nor provide any incentives to solvers of cryptographic puzzles. We view such approaches as frameworks in which system parts, such as the cryptographic puzzle, may be instantiated with different technology. Owners of such a blockchain procure puzzle solvers as… ▽ More We propose the formal study of governed blockchains that are owned and controlled by organizations and that neither create cryptocurrencies nor provide any incentives to solvers of cryptographic puzzles. We view such approaches as frameworks in which system parts, such as the cryptographic puzzle, may be instantiated with different technology. Owners of such a blockchain procure puzzle solvers as resources they control, and use a mathematical model to compute optimal parameters for the cryptographic puzzle mechanism or other parts of the blockchain. We illustrate this approach with a use case in which blockchains record hashes of financial process transactions to increase their trustworthiness and that of their audits. For Proof of Work as cryptographic puzzle, we develop a detailed mathematical model to derive MINLP optimization problems for computing optimal Proof of Work configuration parameters that trade off potentially conflicting aspects such as availability, resiliency, security, and cost in this governed setting. We demonstrate the utility of such a mining calculus by solving some instances of this problem. This experimental validation is strengthened by statistical experiments that confirm the validity of random variables used in formulating our mathematical model. We hope that our work may facilitate the creation of domain-specific blockchains for a wide range of applications such as trustworthy information in Internet of Things systems and bespoke improvements of legacy financial services. △ Less

Submitted 16 May, 2017; v1 submitted 1 December, 2016; originally announced December 2016.

Comments: 25 pages, 4 tables, minor corrections and edits throughout second version, updated relation work in second version, statistical evaluation of random variable for disputes added in second version

Partial Solvers for Parity Games: Effective Polynomial-Time Composition

Authors: Patrick Ah-Fat, Michael Huth

Abstract: Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be by studying interactions of partial solvers based on generic composition patterns that preserve polynomial-time computabilit… ▽ More Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be by studying interactions of partial solvers based on generic composition patterns that preserve polynomial-time computability. We show that use of such composition patterns discovers new partial solvers - including those that merge node sets that have the same but unknown winner - by studying games that composed partial solvers can neither solve nor simplify. We experimentally validate that this data-driven approach to refinement leads to polynomial-time partial solvers that can solve all standard benchmarks of structured games. For one of these polynomial-time partial solvers not even a sole random game from a few billion random games of varying configuration was found that it won't solve completely. △ Less

Submitted 13 September, 2016; originally announced September 2016.

Comments: In Proceedings GandALF 2016, arXiv:1609.03648

Journal ref: EPTCS 226, 2016, pp. 1-15

Fatal Attractors in Parity Games: Building Blocks for Partial Solvers

Authors: Michael Huth, Jim Huan-Pu Kuo, Nir Piterman

Abstract: Attractors in parity games are a technical device for solving "alternating" reachability of given node sets. A well known solver of parity games - Zielonka's algorithm - uses such attractor computations recursively. We here propose new forms of attractors that are monotone in that they are aware of specific static patterns of colors encountered in reaching a given node set in alternating fashion.… ▽ More Attractors in parity games are a technical device for solving "alternating" reachability of given node sets. A well known solver of parity games - Zielonka's algorithm - uses such attractor computations recursively. We here propose new forms of attractors that are monotone in that they are aware of specific static patterns of colors encountered in reaching a given node set in alternating fashion. Then we demonstrate how these new forms of attractors can be embedded within greatest fixed-point computations to design solvers of parity games that run in polynomial time but are partial in that they may not decide the winning status of all nodes in the input game. Experimental results show that our partial solvers completely solve benchmarks that were constructed to challenge existing full solvers. Our partial solvers also have encouraging run times in practice. For one partial solver we prove that its run-time is at most cubic in the number of nodes in the parity game, that its output game is independent of the order in which monotone attractors are computed, and that it solves all Buechi games and weak games. We then define and study a transformation that converts partial solvers into more precise partial solvers, and we prove that this transformation is sound under very reasonable conditions on the input partial solvers. Noting that one of our partial solvers meets these conditions, we apply its transformation on 1.6 million randomly generated games and so experimentally validate that the transformation can be very effective in increasing the precision of partial solvers. △ Less

Submitted 19 May, 2014; v1 submitted 2 May, 2014; originally announced May 2014.

The Rabin index of parity games

Authors: Michael Huth, Jim Huan-Pu Kuo, Nir Piterman

Abstract: We study the descriptive complexity of parity games by taking into account the coloring of their game graphs whilst ignoring their ownership structure. Colored game graphs are identified if they determine the same winning regions and strategies, for all ownership structures of nodes. The Rabin index of a parity game is the minimum of the maximal color taken over all equivalent coloring functions.… ▽ More We study the descriptive complexity of parity games by taking into account the coloring of their game graphs whilst ignoring their ownership structure. Colored game graphs are identified if they determine the same winning regions and strategies, for all ownership structures of nodes. The Rabin index of a parity game is the minimum of the maximal color taken over all equivalent coloring functions. We show that deciding whether the Rabin index is at least k is in PTIME for k=1 but NP-hard for all fixed k > 1. We present an EXPTIME algorithm that computes the Rabin index by simplifying its input coloring function. When replacing simple cycle with cycle detection in that algorithm, its output over-approximates the Rabin index in polynomial time. Experimental results show that this approximation yields good values in practice. △ Less

Submitted 16 July, 2013; originally announced July 2013.

Comments: In Proceedings GandALF 2013, arXiv:1307.4162

Journal ref: EPTCS 119, 2013, pp. 35-49

Labelled transition systems as a Stone space

Authors: Michael Huth

Abstract: A fully abstract and universal domain model for modal transition systems and refinement is shown to be a maximal-points space model for the bisimulation quotient of labelled transition systems over a finite set of events. In this domain model we prove that this quotient is a Stone space whose compact, zero-dimensional, and ultra-metrizable Hausdorff topology measures the degree of bisimilarity s… ▽ More A fully abstract and universal domain model for modal transition systems and refinement is shown to be a maximal-points space model for the bisimulation quotient of labelled transition systems over a finite set of events. In this domain model we prove that this quotient is a Stone space whose compact, zero-dimensional, and ultra-metrizable Hausdorff topology measures the degree of bisimilarity such that image-finite labelled transition systems are dense. Using this compactness we show that the set of labelled transition systems that refine a modal transition system, its ''set of implementations'', is compact and derive a compactness theorem for Hennessy-Milner logic on such implementation sets. These results extend to systems that also have partially specified state propositions, unify existing denotational, operational, and metric semantics on partial processes, render robust consistency measures for modal transition systems, and yield an abstract interpretation of compact sets of labelled transition systems as Scott-closed sets of modal transition systems. △ Less

Submitted 8 March, 2006; v1 submitted 15 December, 2004; originally announced December 2004.

Comments: Changes since v2: Metadata update

ACM Class: F.3.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 1, Issue 1 (January 26, 2005) lmcs:2271