Publications
143 results found
Huth MR, Asokan N, Capkun S, et al., 2013, Proceedings of the Sixth International Conference on Trust & Trustworthy Computing, Publisher: Springer
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
Huth M, Kuo JH-P, 2013, PEALT: A reasoning tool for numerical aggregation of trust evidence, Departmental Technical Report: 13/7, Publisher: Department of Computing, Imperial College London, 13/7
We present a tool that supports the understanding and validation of mechanisms thatnumerically aggregate trust evidence { which may stem from heterogenous sources such asgeographical information, reputation, and threat levels. The tool is based on a policy com-position language Peal [3] and can declare Peal expressions and intended analyses of suchexpressions as input. The analyses include vacuity checking, sensitivity analysis of thresh-olds, and policy re nement. We develop and implement two methods for generating veri -cation conditions for analyses, using the SMT solver Z3 as backend. One method is explicitand space intense, the other one is symbolic and so linear in the analysis expressions. Weexperimentally investigate this space-time tradeo by observing the Z3 code generation andits running time on randomly generated analyses and on a non-random benchmark modelingmajority voting. Our ndings suggest both methods have complementary value and mayscale up su ciently for the analysis of most realistic case studies.
Huth M, Kuo H-P, Piterman N, 2013, Fatal attractors in parity games, Departmental Technical Report: 13/1, Publisher: Department of Computing, Imperial College London, 13/1
We study a new form of attractor in parity games and use it to definesolvers that run in PTIME and are partial in that they do not solve allgames completely. Technically, for color c this new attractor determineswhether player c%2 can reach a set of nodes X of color c whilst avoidingany nodes of color less than c. Such an attractor is fatal if player c%2 canattract all nodes in X back to X in this manner. Our partial solvers detectfixed-points of nodes based on fatal attractors and correctly classify suchnodes as won by player c%2. Experimental results show that our partialsolvers completely solve benchmarks that were constructed to challengeexisting full solvers. Our partial solvers also have encouraging run times.For one partial solver we prove that its runtime is in O(|V |3), that itsoutput game is independent of the order in which attractors are computed,and that it solves all B¨uchi games.
Crampton J, Huth M, Morisset C, 2013, Policy-based access control from numerical evidence, Departmental Technical Report: 13/6, Publisher: Department of Computing, Imperial College London, 13/6
Increasingly, access to resources needs to be regulated or informed by considerations suchas risk, cost, and reputation. We therefore propose a framework for policy languages, basedon semi-rings, that aggregate quantitative evidence to support decision-making in accesscontrol systems. As aggregation operators \addition", \worst case", and \best case" over non-negative reals are both relevant in practice and amenable to analysis, we study an instance,Peal, of our framework in that setting. Peal is a stand-alone policy language but can also beintegrated with existing policy languages.Peal policies can be synthesized into logical formulae that no longer make reference toquantities but capture all policy behavior. Satis ability checking of such formulae can beused to validate and analyze policies in this new evidence-based approach. We discuss anumber of applications, including vacuity, redundancy, change-impact and safety analysis.The synthesis algorithm requires a form of subset enumeration, for which we develop bespokealgorithms and demonstrate experimentally that our algorithms work better than genericstate exploration methods. We also sketch how our approach extends from non-negative realsto other semi-rings and even to rings such as the real numbers.
Huth M, Kuo JHP, Sasse A, et 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.
Huth MR, 2012, Model Checking and Action Abstraction, Verification, Model Checking, and Abstract Interpretation (VMCAI 2008), Publisher: Springer, Pages: 112-126
Huth MR, Kuo JH-P, Piterman N, 2012, Concurrent Small Progress Measures, Publisher: Springer
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)
Huth MR, Kuo JH-P, Piterman N, 2012, The Rabin Index of Parity Games, Haifa Verification Conference, Publisher: Springer, Pages: 259-260
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.
Huth M, Piterman N, Wagner D, 2012, p-Automata: New Foundations for discrete-time probabilistic verification, Performance Evaluation, Vol: 69
Huth MR, Kuo JH-P, Piterman N, 2012, The rabin index of parity games, Departmental Technical Report: 12/1, Publisher: Department of Computing, Imperial College London, 12/1
We study the descriptive complexity of parity games by taking intoaccount the coloring of their game graphs whilst ignoring their owner-ship structure. Di erent colorings of the same graph are identi ed ifthey determine the same winning regions and strategies, for all ownershipstructures of nodes. The Rabin index of a parity game is the minimum ofthe maximal color taken over all equivalent coloring functions. We showthat deciding whether the Rabin index is at least k is in P for k = 1but NP-hard for all xed k 2. We present an EXPTIME algorithmthat computes the Rabin index by simplifying its input coloring function.When replacing simple cycle with cycle detection in that algorithm, itsoutput over-approximates the Rabin index in polynomial time. Experi-mental results show that this approximation yields good values in practice.
Crampton J, Huth M, 2012, On the Modeling and Verification of Security-Aware and Process-Aware Information Systems, 9th International Conference on Business Process Management (BPM 2011), Publisher: SPRINGER-VERLAG BERLIN, Pages: 423-+, ISSN: 1865-1348
- Author Web Link
- Cite
- Citations: 2
Bruns G, Fong PWL, Siahaan ISR, et al., 2012, Relationship-based access control: its expression and enforcement through hybrid logic., Publisher: ACM, Pages: 117-124
Bruns G, Huth M, Avijit K, 2011, Program synthesis in administration of higher-order permissions, Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT, Pages: 41-50
In "administrative" access control, policy controls permissions not just on application actions, but also on actions to modify permissions, on actions to modify permissions on those actions, and so on. One context of work in administrative policy is "administrative RBAC", in which policy controls the permissions of roles, the membership of roles, and other elements of RBAC access-control state. Here we study and extend the UARBAC model for administrative RBAC from the perspective of usability and expressiveness. Using tools from logic and program verification, we formulate UARBAC logically and develop an algorithm that produces "administrative plans" that achieve specified permissions through permitted actions. This work is closely related to work on the safety problem in administrative access control, but aims to aid legitimate users in understanding how to reach a desired access-control state. We then show how this machinery can be used so that ad- ministrative actions at any desired depth, and so plans as well, can be uniformly simulated in the UARBAC model. © 2011 ACM.
Huth MR, Crampton J, 2011, Synthesizing and Verifying Plans for Constrained Workflows: Transferring Tools from Formal Methods, Third International Workshop on Verification and Validation of Planning and Scheduling Systems
Bruns G, Huth M, 2011, Access Control via Belnap Logic: Intuitive, Expressive, and Analyzable Policy Composition, ACM Transactions on Information and System Security, Vol: 14
Access control to IT systems increasingly relies on the ability to compose policies. Hence there is benefit in any framework for policy composition that is intuitive, formal (and so “analyzable” and “implementable”), expressive, independent of specific application domains, and yet able to be extended to create domain-specific instances. Here we develop such a framework based on Belnap logic. An access-control policy is interpreted as a four-valued predicate that maps access requests to either grant, deny, conflict, or unspecified – the four values of the Belnap bilattice. We define an expressive access-control policy language PBel, having composition operators based on the operators of Belnap logic. Natural orderings on policies are obtained by lifting the truth and information orderings of the Belnap bilattice. These orderings lead to a query language in which policy analyses, for example, conflict freedom, can be specified. Policy analysis is supported through a reduction of the validity of policy queries to the validity of propositional formulas on predicates over access requests. We evaluate our approach through firewall policy and RBAC policy examples, and discuss domain-specific and generic extensions of our policy language.
Bruns G, Huth M, 2011, Access control via belnap logic: intuitive, expressive, and analyzable policy composition, Departmental Technical Report: 11/6, Publisher: Department of Computing, Imperial College London, 11/6
Access control to IT systems increasingly relies on the ability to compose policies. Thereis thus bene t in any framework for policy composition that is intuitive, formal (and so \an-alyzable" and \implementable"), expressive, independent of speci c application domains, andyet able to be extended to create domain-speci c instances. Here we develop such a frameworkbased on Belnap logic. An access-control policy is interpreted as a four-valued predicate thatmaps access requests to either grant, deny, conict, or unspeci ed { the four values of the Bel-nap bilattice. We de ne an expressive access-control policy language PBel, having compositionoperators based on the operators of Belnap logic. Natural orderings on policies are obtained bylifting the truth and information orderings of the Belnap bilattice. These orderings lead to aquery language in which policy analyses, e.g. conict freedom, can be speci ed. Policy analysisis supported through a reduction of the validity of policy queries to the validity of propositionalformulas on predicates over access requests. We evaluate our approach through rewall policyand RBAC policy examples, and discuss domain-speci c and generic extensions of our policylanguage.
Huth MR, 2010, Formal Methods and Access Control, Encyclopedia of Cryptography and Security, Editors: van Tilborg, Jajodia, Publisher: Springer
Huth MR, Crampton J, 2010, Towards an Access-Control Framework for Countering Insider Threats, Insider Threats in Cybersecurity - And Beyond, Publisher: Springer, Pages: 173-194
Antonik A, Huth M, Larsen KG, et al., 2010, Modal and Mixed Specifications: Key Decision Problems and their Complexities, Mathematical Structures in Computer Science, Vol: 20, Pages: 75-103
Crampton J, Huth M, 2010, An Authorization Framework Resilient to Policy Evaluation Failures, 15th European Symposium on Research in Computer Security (ESORICS 2010), Publisher: Springer Verlag, Pages: 472-487
Antonik A, Huth M, Larsen KG, et al., 2010, Modal and Mixed Specifications: Key Decision Problems and their Complexities, Mathematical Structures in Computer Science, Vol: 20, Pages: 75-103
Huth M, Piterman N, Wagner D, 2010, p-Automata: New Foundations for Discrete-Time Probabilistic Verification, Seventh International Conference on the Quantitative Evaluation of Systems (QEST), Publisher: IEEE Computer Society Press, Pages: 161-170
Kattenbelt M, Huth M, 2009, Verification and refutation of probabilistic specifications via games, Leibniz International Proceedings in Informatics, LIPIcs, Vol: 4, Pages: 251-262, ISSN: 1868-8969
We develop an abstraction-based framework to check probabilistic specifications of Markov Decision Processes (MDPs) using the stochastic two-player game abstractions (i.e. "games") developed by Kwiatkowska et al. as a foundation. We define an abstraction preorder for these game abstractions which enables us to identify many new game abstractions for each MDP - ranging from compact and imprecise to complex and precise. This added ability to trade precision for efficiency is crucial for scalable software model checking, as precise abstractions are expensive to construct in practice. Furthermore, we develop a four-valued probabilistic computation tree logic (PCTL) semantics for game abstractions. Together, the preorder and PCTL semantics comprise a powerful verification and refutation framework for arbitrary PCTL properties of MDPs. © Mark Kattenbelt and Michael Huth.
Huth M, Piterman N, Wagner D, 2009, p-automata: acceptors for Markov Chains, Departmental Technical Report: 09/14, Publisher: Department of Computing, Imperial College London, 09/14
We present p-automata, which accept an entire Markovchain as input. Acceptance is determined by solving a sequenceof stochastic weak and weak games. The set oflanguages of Markov chains obtained in this way is closedunder Boolean operations. Language emptiness and containmentare equi-solvable, and languages themselves areclosed under bisimulation. A Markov chain (respectively,PCTL formula) determines a p-automaton whose languageis the bisimulation equivalence class of that Markov chain(respectively, the set of models of that formula). We definea simulation game between p-automata, decidable in EXPTIME.Simulation under-approximates language containment,whose decidability status is presently unknown.
Antonik A, Charlton N, Huth M, 2009, Polynomial-Time Under-Approximation of Winning Regions in Parity Games, Electronic Notes in Theoretical Computer Science, Vol: 225, Pages: 115-139, ISSN: 1571-0661
We propose a pattern for designing algorithms that run in polynomial time by construction and under-approximate the winning regions of both players in parity games. This approximation is achieved by the interaction of finitely many aspects governed by a common ranking function, where the choice of aspects and ranking function instantiates the design pattern. Each aspect attempts to improve the under-approximation of winning regions or decrease the rank function by simplifying the structure of the parity game. Our design pattern is incremental as aspects may operate on the residual game of yet undecided nodes. We present several aspects and one higher-order transformation of our algorithms ù based on efficient, static analyses ù and illustrate the benefit of their interaction as well as their relative precision within pattern instantiations. Instantiations of our design pattern can be applied for local model checking and as preprocessors for algorithms whose worst-case running time is exponential. This design pattern and its aspects have already been implemented in [H. Wang. Framework for Under-Approximating Solutions of Parity Games in Polynomial Time. MEng Thesis, Department of Computing, Imperial College London, 78 pages, June 2007].
Crampton J, Huth M, 2009, Detecting and Countering Insider Threats: Can Policy-Based Access Control Help?, 5th International Workshop on Security and Trust Management (STM 2009), Publisher: Elsevier
As insider threats pose very significant security risks to IT systems, we ask what policy-based approaches to access control can do for the detection, mitigation or countering of insider threats and insider attacks. Answering this question is difficult since little public data about insider-threat cases is available, since there is not much consensus about what the insider problem actually is, and since research in access control has by-and-large not dealt with this issue in the past. We explore existing notions of insiderness in order to identify the relevant research issues. We then formulate a set of requirements for next-generation access-control systems whose realization might form part of an overall strategy at addressing the insider problem.\r\n
Huth M, Grumberg O, 2009, Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification, International Journal on Software Tools for Technology Transfer, Vol: 11, Pages: 85-94, ISSN: 1433-2779
Reachability analysis asks whether a system can evolve from legitimate initial states to unsafe states. It is thus a fundamental tool in the validation of computational systems - be they software, hardware or a combination thereof.\r\n\r\nWe recall a standard approach for reachability analysis, which captures the system in a transition system, forms another transition system as an over-approximation, and performs an incremental fixed-point computation on that over-approximation to determine whether unsafe states can be reached. We show this method to be sound for proving the absence of errors, and discuss its limitations for proving the presence of errors, as well as some means of addressing this limitation. \r\n\r\nWe then sketch how program annotations for data integrity constraints and interface specifications - as in Bertrand Meyer's paradigm of Design by Contract - can facilitate the validation of modular programs., e.g. by obtaining more precise verification conditions for software verification supported by automated theorem proving. \r\n\r\nThen we recap how the decision problem of satisfiability for formulae of logics with theories - e.g. bit-vector arithmetic - can be used to construct an over-approximating transition system for a program. Programs with data types comprised of bit-vectors of finite width require bespoke decision procedures for satisfiability. Finite-width data types challenge the reduction of that decision problem to one that off-the-shelf tools can solve effectively, e.g. SAT solvers for propositional logic. In that context, we recall the Tseitin encoding which converts formulae from that logic into conjunctive normal form - the standard format for most SAT solvers - with only linear blow-up in the size of the formula, but linear increase in the number of variables.\r\n\r\nFinally, we discuss the contributions that the three papers in this special section make in the areas that we sketched above.\r\n
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.