Imperial College London

ProfessorMichaelHuth

Faculty of EngineeringDepartment of Computing

Professor of Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8355m.huth Website

 
 
//

Location

 

Huxley 422ACE ExtensionSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

128 results found

Ah-Fat P, Huth M, 2018, Optimal accuracy privacy trade-off for secure computations, IEEE Transactions on Information Theory, ISSN: 0018-9448

The purpose of Secure Multi-Party Computation is to enable protocol participants to compute a public function of their private inputs while keeping 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 Rényi 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.

JOURNAL ARTICLE

Nicolescu R, Huth M, Radanliev P, De Roure Det al., 2018, Mapping the values of IoT, JOURNAL OF INFORMATION TECHNOLOGY, Vol: 33, Pages: 345-360, ISSN: 0268-3962

JOURNAL ARTICLE

Lundbaek L-N, Beutel DJ, Huth M, Jackson S, Kirk L, Steiner Ret al., 2018, Proof of Kernel Work: a democratic low-energy consensus for distributed access-control protocols, ROYAL SOCIETY OPEN SCIENCE, Vol: 5, ISSN: 2054-5703

JOURNAL ARTICLE

Mistry M, D'Iddio AC, Huth M, Misener Ret al., 2018, Satisfiability modulo theories for process systems engineering, COMPUTERS & CHEMICAL ENGINEERING, Vol: 113, Pages: 98-114, ISSN: 0098-1354

JOURNAL ARTICLE

Taylor P, Allpress S, Carr M, Lupu E, Norton J, Smith L, Blackstock J, Boyes H, Hudson-Smith A, Brass I, Chizari H, Cooper R, Coultron P, Craggs B, Davies N, De Roure D, Elsden M, Huth M, Lindley J, Maple C, Mittelstadt B, Nicolescu R, Nurse J, Procter R, Radanliev P, Rashid A, Sgandurra D, Skatova A, Taddeo M, Tanczer L, Vieira-Steiner R, Watson JDM, Wachter S, Wakenshaw S, Carvalho G, Thompson RJ, Westbury PSet al., 2018, Internet of Things: Realising the Potential of a Trusted Smart World, Internet of Things: Realising the Potential of a Trusted Smart World, London, Publisher: Royal Academy of Engineering: London

This report examines the policy challenges for the Internet of Things (IoT), and raises a broad range of issues that need to be considered if policy is to be effective and the potential economic value of IoT is harnessed. It builds on the Blackett review, The Internet of Things: making the most of the second digital revolution, adding detailed knowledge based on research from the PETRAS Cybersecurity of the Internet of Things Research Hub and input from Fellows of the Royal Academy of Engineering. The report targets government policymakers, regulators, standards bodies and national funding bodies, and will also be of interest to suppliers and adopters of IoT products and services.

REPORT

Balduccini M, Griffor E, Huth MRA, Vishik C, Bruns M, Wollman Det al., Ontology-based reasoning about the trustworthiness of cyber-physical systems, Living in the Internet of Things, Publisher: Institution of Engineering and Technology

t has been challenging for the technical and regulatory com-munities to formulate requirements for trustworthiness of thecyber-physical systems (CPS) due to the complexity of theissues associated with their design, deployment, and opera-tions. The US National Institute of Standards and Technology(NIST), through a public working group, has released a CPSFramework that adopts a broad and integrated view of CPS andpositions trustworthiness among other aspects of CPS. This pa-per takes the model created by the CPS Framework and itsfurther developments one step further, by applying ontologi-cal approaches and reasoning techniques in order to achievegreater understanding of CPS. The example analyzed in the pa-per demonstrates the enrichment of the original CPS model ob-tained through ontology and reasoning and its ability to deliveradditional insights to the developers and operators of CPS.

CONFERENCE PAPER

Lundbaek L-N, D'Iddio AC, Huth M, 2017, Centrally Governed Blockchains: Optimizing Security, Cost, and Availability, Editors: Aceto, Bacci, Bacci, Ingolfsdottir, Legay, Mardare, Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 578-599, ISBN: 978-3-319-63120-2

BOOK CHAPTER

Huth MRA, Ah-Fat P, Secure Multi-Party Computation: Information Flow of Outputs and Game Theory, 6th International Conference on Principles of Security and Trust (POST)

Secure multiparty computation enables protocol participantsto compute the output of a public function of their private inputs whilstprotecting the confidentiality of their inputs. But such an output, as afunction of its inputs, inevitably leaks some information about input val-ues regardless of the protocol used to compute it. We introduce founda-tions for quantifying and understanding how such leakage may influenceinput behaviour of deceitful protocol participants as well as that of par-ticipants they target. Our model captures the beliefs and knowledge thatparticipants have about what input values other participants may choose.In this model, measures of information flow that may arise between pro-tocol participants are introduced, formally investigated, and experimen-tally evaluated. These information-theoretic measures not only suggestadvantageous input behaviour to deceitful participants for optimal up-dates of their beliefs about chosen inputs of targeted participants. Theyalso allow targets to quantify the information-flow risk of their inputchoices. We show that this approach supports a game-theoretic formula-tion in which deceitful attackers wish to maximise the information thatthey gain on inputs of targets once the computation output is known,whereas the targets wish to protect the privacy of their inputs.

CONFERENCE PAPER

Huth MRA, Beaumont P, Evans N, Plant Tet al., 2016, Bounded analysis of constrained dynamical systems: a case study in nuclear arms control, INMM Annual Conference 2016, Publisher: Institute of Nuclear Materials Management

We introduce a simple dynamical system that describes key features of a bilateral nuclear armscontrol regime. The evolution of each party's beliefs and declarations under the regime are represented, andthe e ects of inspection processes are captured. Bounded analysis of this model allows us to explore { withina nite horizon { the consequences of changes to the rules of the arms control process and to the strategiesof each party, bounded scope invariants for variables of interest, and dynamics for initial states containingstrict uncertainty. Together these would potentially enable a decision support system to consider casesof interest irrespective of unknowns. We realize such abilities by building a Python package that drawson the capabilities of a Satis ability Modulo Theory (SMT) solver to explore particular scenarios and tooptimize measures of interest { such as the belief of one nation in the statements made by another, orthe timing of an unscheduled inspection such that it has maximum value. We show that these capabilitiescan in principle support the design or assessment of future bilateral arms control instruments by applyingthem to a set of representative and relevant test scenarios with realistic nite horizons.

CONFERENCE PAPER

Huth MRA, Beaumont P, Evans N, Plant Tet al., 2016, Confidence analysis for nuclear arms control: SMT abstractions of Game Theoretic Models, INMM Annual Conference 2016, Publisher: Institute of Nuclear Materials Management

We consider the use of game theory in an arms control inspection planning scenario. Speci callywe develop a case study that games the number of inspections available against an ideal treaty length.Normal game theoretic techniques struggle to justify pay-o values to use for certain events, limiting theusefulness of such techniques. In order to improve the value of using game theory for decision making, weintroduce a methodology for under-specifying the game theoretic models through a mixture of regressiontechniques and Satis ability Modulo Theory (SMT) constraint solving programs. Our approach allows auser to under-specify pay-o s in games, and to check, in a manner akin to robust optimisation, for howsuch under-speci cations a ect the `solution' of a game. We analyse the Nash equilibria and the mixedstrategy sets that would lead to such equilibria - and explore how to maximise expected pay-o s and useof individual pure strategies for all possible values of an under-speci cation. Through this approach, wegain an insight into how - irrespective of uncertainty - we can still compute with game theoretic models,and present the types and kinds of analysis we can run that bene t from this uncertainty.

CONFERENCE PAPER

Huth MRA, Beaumont, Day E, Evans N, Haworth S, Plant T, Roberts Cet al., 2016, An in-depth case study: modelling an information barrier with Bayesian Belief Networks, INMM Annual Conference, Publisher: Institute of Nuclear Materials Management

We present in detail a quantitative Bayesian Belief Network (BBN) model of the use of aninformation barrier system during a nuclear arms control inspection, and an analysis of this model usingthe capabilities of a Satis ability Modulo Theory (SMT) solver. Arms control veri cation processes do notin practice allow the parties involved to gather complete information about each other, and therefore anymodel we use must be able to cope with the limited information, subjective assessment and uncertaintyin this domain. We have previously extended BBNs to allow this kind of uncertainty in parameter values(such as probabilities) to be re ected; theseconstrainedBBNs (cBBNs) o er the potential for more robustmodelling, which in that study we demonstrated with a simple information barrier model. We now presenta much more detailed model of a similar veri cation process, based on the technical capabilities anddeployment concept of the UK-Norway Initiative (UKNI) Information Barrier system, demonstrating thescalability of our previously-presented approach. We discuss facets of the model itself in detail, beforeanalysing pertinent questions of interest to give examples of the power of this approach.

CONFERENCE PAPER

Huth M, Kuo JH-P, Piterman N, 2016, Static Analysis of Parity Games: Alternating Reachability Under Parity, Editors: Probst, Hankin, Hansen, Publisher: SPRINGER INT PUBLISHING AG, Pages: 159-177, ISBN: 978-3-319-27809-4

BOOK CHAPTER

Ah-Fat P, Huth M, 2016, Partial Solvers for Parity Games: Effective Polynomial-Time Composition, ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, Pages: 1-15, ISSN: 2075-2180

JOURNAL ARTICLE

Huth MRA, Huth, Piterman, Kuo Jet al., 2015, Static Analysis of Parity Games: Alternating Reachability Under Parity, Semantics, Logics, and Calculi Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, Publisher: Springer, Pages: 159-177, ISSN: 0302-9743

It is well understood that solving parity games is equivalent,up to polynomial time, to model checking of the modal mu-calculus. Itis a long-standing open problem whether solving parity games (or modelchecking modal mu-calculus formulas) can be done in polynomial time.A recent approach to studying this problem has been the design of partialsolvers, algorithms that run in polynomial time and that may only solveparts of a parity game. Although it was shown that such partial solverscan completely solve many practical benchmarks, the design of such partialsolvers was somewhat ad hoc, limiting a deeper understanding ofthe potential of that approach. We here mean to provide such robustfoundations for deeper analysis through a new form of game, alternatingreachability under parity. We prove the determinacy of these games anduse this determinacy to define, for each player, a monotone fixed pointover an ordered domain of height linear in the size of the parity gamesuch that all nodes in its greatest fixed point are won by said player inthe parity game. We show, through theoretical and experimental work,that such greatest fixed points and their computation leads to partialsolvers that run in polynomial time. These partial solvers are based onestablished principles of static analysis and are more effective than partialsolvers studied in extant work.

CONFERENCE PAPER

Huth M, Kuo JH-P, Piterman N, 2015, The Rabin index of parity games: Its complexity and approximation, INFORMATION AND COMPUTATION, Vol: 245, Pages: 36-53, ISSN: 0890-5401

JOURNAL ARTICLE

Beaumont P, Evans N, Huth M, Plant Tet al., 2015, Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks, 20th European Symposium on Research in Computer Security (ESORICS), Publisher: SPRINGER INT PUBLISHING AG, Pages: 521-540, ISSN: 0302-9743

CONFERENCE PAPER

Huth MR, Kuo JH-P, 2014, PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), Publisher: Springer, Pages: 109-123, ISSN: 0302-9743

CONFERENCE PAPER

Crampton J, Huth M, Kuo JH-P, 2014, Authorized workflow schemas: deciding realizability through LTL(F) model checking, INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, Vol: 16, Pages: 31-48, ISSN: 1433-2779

JOURNAL ARTICLE

Huth M, Kuo JHP, 2014, On designing usable policy languages for declarative trust aggregation, Pages: 45-56, ISSN: 0302-9743

We argue that there will be an increasing future need for the design and implementation of declarative languages that can aggregate trust evidence and therefore inform the decision making of IT systems at run-time. We first present requirements for such languages. Then we discuss an instance of such a language, Peal+, which extends an early prototype Peal that was researched by others in collaboration with us. Next, we formulate the intuitive semantics of Peal+, present a simple use case of it, and evaluate to what extent Peal+ meets our formulated requirements. In this evaluation, particular attention is given to the usability aspects of declarative languages that mean to aggregate trust evidence. © 2014 Springer International Publishing.

CONFERENCE PAPER

Huth MR, Kuo JH-P, Piterman N, 2013, The Rabin index of parity games, Electronic Proceedings inTheoretical Computer Science, Vol: 119, Pages: 35-49

JOURNAL ARTICLE

Huth M, Kuo JHP, 2013, Towards verifiable trust management for software execution (extended abstract), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7904 LNCS, Pages: 275-276, ISSN: 0302-9743

In the near future, computing devices will be present in most artefacts, will considerably outnumber the number of people on this planet, and will host software the executes in a potentially hostile and only partially known environment. This suggests the need for bringing trust management into running software itself, so that executing software be guard-railed by policies that reflect risk postures deemed to be appropriate for software and its deployment context. We sketch here an implementation of a prototype that realizes, in part, such a vision. © 2013 Springer-Verlag.

JOURNAL ARTICLE

Huth M, Kuo JHP, Sasse A, Kirlappos Iet al., 2013, Towards usable generation and enforcement of trust evidence from programmers' intent, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 8030 LNCS, Pages: 246-255, ISSN: 0302-9743

Programmers develop code with a sense of purpose and with expectations on how units of code should interact with other units of code. But this intent of programmers is typically implicit and undocumented, goes beyond considerations of functional correctness, and may depend on trust assumptions that programmers make. At present, neither programming languages nor development environments offer a means of articulating such intent in a manner that could be used for controlling whether software executions meet such intentions and their associated expectations. We here study how extant research on trust can inform approaches to articulating programmers' intent so that it may help with creating trust evidence for more trustworthy interaction of software units. © 2013 Springer-Verlag Berlin Heidelberg.

JOURNAL ARTICLE

Huth MR, Asokan N, Capkun S, Flechais I, Coles-Kemp Let al., 2013, Proceedings of the Sixth International Conference on Trust & Trustworthy Computing, Publisher: Springer

CONFERENCE PAPER

Huth MR, Kuo JH-P, Piterman N, 2013, Fatal Attractors in Parity Games, Foundations of Software Science and Computation Structures (FoSSaCS 2013), Publisher: Springer, Pages: 34-49

CONFERENCE PAPER

Huth MR, 2012, Model Checking and Action Abstraction, Verification, Model Checking, and Abstract Interpretation (VMCAI 2008), Publisher: Springer, Pages: 112-126

CONFERENCE PAPER

Huth MR, Kuo JH-P, Piterman N, 2012, Concurrent Small Progress Measures, Publisher: Springer

CONFERENCE PAPER

Huth MR, Kuo JH-P, Piterman N, 2012, The Rabin Index of Parity Games, Haifa Verification Conference, Publisher: Springer, Pages: 259-260

CONFERENCE PAPER

Huth MR, Crampton J, Kuo JH-P, 2012, Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning, Third Workshop on Practical Aspects of Automated Reasoning (PAAR-2012)

CONFERENCE PAPER

Crampton J, Huth M, 2012, A framework for the modular specification and orchestration of authorization policies, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7127 LNCS, Pages: 155-170, ISSN: 0302-9743

Many frameworks for defining authorization policies fail to make a clear distinction between policy and state. We believe this distinction to be a fundamental requirement for the construction of scalable, distributed authorization services. In this paper, we introduce a formal framework for the definition of authorization policies, which we use to construct the policy authoring language APOL. This framework makes the required distinction between policy and state, and APOL permits the specification of complex policy orchestration patterns even in the presence of policy gaps and conflicts. A novel aspect of the language is the use of a switch operator for policy orchestration, which can encode the commonly used rule- and policy-combining algorithms of existing authorization languages. We define denotational and operational semantics for APOL and then extend our framework with statically typed methods for policy orchestration, develop tools for policy analysis, and show how that analysis can improve the precision of static typing rules. © 2012 Springer-Verlag.

JOURNAL ARTICLE

Huth M, Piterman N, Wagner D, 2012, p-Automata: New Foundations for discrete-time probabilistic verification, Performance Evaluation, Vol: 69

JOURNAL ARTICLE

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00333344&limit=30&person=true