This paper introduces a robust optimization framework for cybersecurity decision-making for turn-based security games over probabilistic attack graphs. We address uncertainties in both the attacker’s state and the effectiveness of controls, proposing a novel approach based on repeated leader-multi-follower games; we introduce a game solution for these games as a minimization of the geometric mean across all possible worlds. We show fundamental mathematical properties of this game solution: (a) it is Pareto optimal, (b) it is equivalent to a standard leader-follower game of the sequence of scenarios, and (c) it is robust. Our framework incorporates budget constraints and leverages game-theoretic and robust optimization techniques for efficient solutions. We validate our approach through experiments, where we show our solutions outperform classic robust optimization solutions like minmax regret. We also present a case study showcasing the meaningfulness of our approach in a network attack scenario.

The mathematical modeling of cybersecurity decision-making heavily relies on cybersecurity metrics. However, achieving precision in these metrics is notoriously challenging, and their inaccuracies can significantly influence model outcomes. This paper explores resilience to uncertainties in the effectiveness of security controls. We employ probabilistic attack graphs to model threats and introduce two resilient models: minmax regret and min-product of risks, comparing their performance. Building on previous Stackelberg game models for cybersecurity, our approach leverages totally unimodular matrices and linear programming (LP) duality to provide efficient solutions. While minmax regret is a well-known approach in robust optimization, our extensive simulations indicate that, in this context, the lesser-known min-product of risks offers superior resilience. To demonstrate the practical utility and robustness of our framework, we include a multi-dimensional decision support case study focused on home IoT cybersecurity investments, highlighting specific insights and outcomes. This study illustrates the framework’s effectiveness in real-world settings.

We introduce an efficient solution for Stackelberg games in the context of a class of Security games and bounded rational attackers. These games model a threat scenario where an attacker can launch multi-stage attacks against a defender who can deploy defensive controls subject to some budget constraints. Because the optimal solution in these games may leave some unspent budget, the question of what to do in this situation arises. In this work, we suggest investing it iteratively in the closest sub-optimal solutions until possible. Here we develop the needed theory and framework, starting from defining sub-optimality and solving the corresponding optimisations. By using total unimodularity and precise linear programming (LP) relaxation, we provide an efficient computational solution to these games. The security improvement of the proposed approach is illustrated with an AI threat scenario.

This work introduces a decision support framework, called Cyber Risk Optimiser for Smart homeS (CROSS), which advises both smart home users and smart home service providers on how to select an optimal portfolio of cyber security controls to counteract cyber attacks in a smart home including traditional cyber attacks and adversarial machine learning attacks. CROSS is based on a multi-objective bi-level two-stage optimisation. In stage-one optimisation, the problem is modelled as a multi-leader-follower game that considers both security and economic objectives, where the provider selects a security portfolio to protect both itself and its users, while rational attackers target the weakest path. Stage-two optimisation is a Stackelberg security game that focuses on additional user security controls under the remit of smart home users. While CROSS can potentially be applied to other similar use cases, in this paper, our aim is to address threats against artificial intelligence (AI) applications as the use of AI in smart Internet of Things (IoT) devices introduces new cyber threats to home environments. Specifically, we have implemented and assessed CROSS in a smart heating use case in a prototypical AI-enabled IoT environment that combines characteristics and vulnerabilities currently present on existing commercial off-the-shelf (COTS) devices, demonstrating the selection of optimal decisions.

Through a built-in security analysis feature based on metadata, this article provides a novel framework that starts with a scenario input and produces a collection of visualizations based on Common Attack Pattern Enumeration and Classification (CAPEC) and Common Weakness Enumeration (CWE) Standards. It immediately links enterprise mitigations from MITRE ATT&CK framework to the security flaws it discovered. It’s also integrated with a third-party optimization tool targeted at cutting security costs for businesses, which it can perform in real-time or later using JSON output in the preferred format, depending on the execution mode. All of these stages are conducted without human intervention. Adaptive metadata with a variety of rules for capturing different sorts of known or prospective attack types allows for the production of attack graphs. It can be used as a quick and practical what-if analysis tool to detect potential intrusions for a variety of network configuration setups and assigned access privileges. As a threat modeler, it is suitable for both novice and expert users. Due to the easy input scheme and human-readable outputs, it can also be utilized as an educational tool.

The pandemic has demonstrated that healthcare systems are prime targets for attackers. Finding an optimal security control set is a constant challenge for health organizations, where cost is a major consideration. The purpose of this paper is to demonstrate a healthcare cost optimization system as well as a case study based on two IT setup configurations that have been evaluated by medical experts as well as IT experts. These configurations would aid in conveying the complexity of the decision parameters and demonstrating how CySecTool handles this difficulty. In the study, 64 different security controls were linked to 70 vulnerabilities that could occur at any level of a hospital system dealing with both internal and external attacks/risks. The study also includes a novel visualization scheme that allows for the observation of vulnerabilities and also their subcategories based on Microsoft's STRIDE categorization.

A mathematical framework to reason about time resilience in cybersecurity is here introduced. We first consider an attacker who is able to mount several multi-stage attacks on the organization: the defender’s objective is to select an optimal portfolio of security controls, within a given budget, to withstand the highest number of attacks. The mathematical model is a Markov chain with an initial state called the safe state, intermediate states for all possible attacks (each attack state denoting a probabilistic attack graph), and a sink state denoting a successful attack. The overall defence problem is formulated as a bi-level multi-objective optimization, i.e., the defender selects an optimal portfolio of security controls to mitigate an optimal attacker. In order to determine the probability of success of an attack two cases will be considered: (a) the expected probability of success and (b) the highest probability of success. We refer to these two cases as expected-time analysis and worst-case time analysis, respectively. To solve precisely these bi-level optimizations strong duality and Mixed Integer Linear Programming are used. We then extend the framework to investigate resilience in terms of the total duration of the attacks; variations of the previous optimizations are presented to this purpose. Finally numerical evaluations are provided to compare the results obtained from the expected-time analysis and the worst-case time analysis.

We present a new generalising framework for conditional entropies, considering a limit construction over sequences of core-concave entropies, and prove that quasiconcave functions are the set of such limits. This generalising framework subsumes recently proposed frameworks for entropies in quantitative information flow, including entropies whose conditional form reflects the expected leakage and the leakage in the worst-case scenario. Thanks to the properties of the limits it is also shown that several important information theoretical properties can be proven for the generalised entropies satisfying the axioms.

A decision support system for cyber-security is here presented. The system aims to select an optimal portfolio of security controls to counteract multi-stage attacks. The system has several components: a preventive optimisation to select controls for an initial defensive portfolio, a learning mechanism to estimate possible ongoing attacks, and an online optimisation selecting an optimal portfolio to counteract ongoing attacks. The system relies on efficient solutions of bi-level optimisations, in particular, the online optimisation is shown to be a Bayesian Stackelberg game solution. The proposed solution is shown to be more efficient than both classical solutions like Harsanyi transformation and more recent efficient solvers. Moreover, the proposed solution provides significant security improvements on mitigating ongoing attacks compared to previous approaches. The novel techniques here introduced rely on recent advances in Mixed-Integer Conic Programming (MICP), strong duality and totally unimodular matrices.

This work presents an axiomatization for entropy based on an extension of concavity called core-concavity. We show that core-concavity characterizes the largest class of functions for which the data-processing inequality holds, under the assumption that conditional entropy is defined as a generalized average. Also, under the same assumption, we show that data-processing and “conditioning reduces entropy” properties are equivalent. We prove several properties of core-concave functions, including generalization of perfect secrecy and of Fano's inequality. We also show that definitions of conditional entropy based on worst-case can be retrieved as limit cases of generalized averages. A connection between statistical decision making and this axiomatic approach is also presented.

This work explores the problem of designing a channel that leaks the least amount of information while respecting a set of operational constraints. This paper focuses on deterministic channels and deterministic solutions. This setting is relevant because most programs and many channel design problems are naturally modelled by deterministic channels. Moreover, the setting is also relevant when considering an attacker who can observe many outputs of an arbitrary channel while the secret input stays the same: when the number of observations is arbitrarily large, the channel of minimal leakage is deterministic. The deterministic channel design problem has different solutions depending on which leakage measure is chosen. The problem is shown to be NP-hard in general. However, for a particular class of constraints, called k-complete hypergraph constraints, a greedy algorithm is shown to provide the optimal solution for a wide class of leakage measures.

This work introduces a new preorder over channels that is monotonic with Shannon's mutual information for all distributions over the input alphabet. Moreover, this monotonicity also holds when substituting mutual information for quantities relative to Arimoto-Rényi conditional entropies and guessing entropy. Several results connecting this new preorder with others from the literature are proven. This work also discusses an extension of Shannon ordering based on this new preorder, and establishes that channels ordered this way are also ordered with regards to both Shannon and min-capacity.

We introduce a novel generalization of entropy and conditional entropy from which most definitions from the literature can be derived as particular cases. Within this general framework, we investigate the problem of designing countermeasures for information leakage. In particular, we seek metric-invariant solutions, i.e., they are robust against the choice of entropy for quantifying the leakage. The problem can be modeled as an information channel from the system to an adversary, and the countermeasures can be seen as modifying this channel in order to minimize the amount of information that the outputs reveal about the inputs. Our main result is to fully solve the problem under the highly symmetrical design constraint that the number of inputs that can produce the same output is capped. Our proof is constructive and the optimal channels and the minimum leakage are derived in closed form.

In this paper we describe symbolic side-channel analysis techniques for detecting and quantifying information leakage, given in terms of Shannon and min-entropy. Measuring the precise leakage is challenging due to the randomness and noise often present in program executions and side-channel observations. We account for this noise by introducing additional (symbolic) program inputs which are interpreted probabilistically, using symbolic execution with parametrized model counting. We also explore a sampling approach for increased scalability. In contrast to typical Monte Carlo techniques, our approach works by sampling symbolic paths, representing multiple concrete paths, and uses pruning to accelerate computation and guarantee convergence to the optimal results. A key novelty of our approach is to provide bounds on the leakage that are provably under- and over-approximating the exact leakage. We implemented the techniques in the Symbolic PathFinder tool and demonstrate them on Java programs.

We consider a setting where a system has to interact, and hence create distinct outputs (observables), but subject to such operational constraints wants to minimize the leakage that such observables reveal about its secret input. It has been previously demonstrated that under some (highly symmetrical) constraints on the observables, it is possible to design systems that are universally optimal in the sense of leaking minimal information no matter how information is measured.,,In this work we make several contribution to this field. On universal (i.e., measure-invariant) optimality, we show its limitations through a counterexample where symmetry constraints are broken. Nevertheless, we also show two new universal optimality results: the first is in the presence of "graph like" constraints (that may lack symmetry). The second is universal optimality in the case of uncertainty about the prior. Furthermore, we prove that a generic class of leakage optimisation problems are convex problem, from which we derive that KKT conditions are necessary and sufficient for optimality. We demonstrate the practical value of the theory in the form of an application to timing attacks countermeasures.

We present symbolic analysis techniques for detecting vulnerabilities that are due to adaptive side-channel attacks, and synthesizing inputs that exploit the identified vulnerabilities. We start with a symbolic attack model that encodes succinctly all the side-channel attacks that an adversary can make. Using symbolic execution over this model, we generate a set of mathematical constraints, where each constraint characterizes the set of secret values that lead to the same sequence of side-channel measurements. We then compute the optimal attack, i.e, the attack that yields maximum leakage over the secret, by solving an optimization problem over the computed constraints. We use information-theoretic concepts such as channel capacity and Shannon entropy to quantify the leakage over multiple runs in the attack, where the measurements over the side channels form the observations that an adversary can use to try to infer the secret. We also propose greedy heuristics that generate the attack by exploring a portion of the symbolic attack model in each step. We implemented the techniques in Symbolic PathFinder and applied them to Java programs encoding web services, string manipulations and cryptographic functions, demonstrating how to synthesize optimal side-channel attacks.

Perfect secrecy describes cases where an adversary cannot learn anything about the secret beyond its prior distribution. A classical result by Shannon shows that a necessary condition for perfect secrecy is that the adversary should not be able to eliminate any of the possible secrets. In this paper we answer the following fundamental question: What is the lowest leakage of information that can be achieved when some of the secrets have to be eliminated? We address this question by deriving the minimum leakage in closed-form, and explicitly providing "universally optimal" randomized strategies, in the sense that they guarantee the minimum leakage irrespective of the measure of entropy used to quantify the leakage. We then introduce a generalization of Rényi family of asymmetric measures of leakage which generalizes the g-leakage and show that a slight modification of our strategies are optimal with respect to an important class of such measures. Subsequently, we show that our schemes constitute the Nash Equilibria of closely related two-person zero sum games. This game perspective provides implicit solutions for a wider set of structural constraints and asymmetric entropies. Finally we demonstrate how this work can also be seen as designing a universally optimal channel given a specified prior.

Side-channel attacks recover confidential information from non-functional characteristics of computations, such as time or memory consumption. We describe a program analysis that uses symbolic execution to quantify the information that is leaked to an attacker who makes multiple side-channel measurements. The analysis also synthesizes the concrete public inputs (the "attack") that lead to maximum leakage, via a novel reduction to Max-SMT solving over the constraints collected with symbolic execution. Furthermore model counting and information-theoretic metrics are used to compute an attacker's remaining uncertainty about a secret after a certain number of side-channel measurements are made. We have implemented the analysis in the Symbolic PathFinder tool and applied it in the context of password checking and cryptographic functions, showing how to obtain tight bounds on information leakage under a small number of attack steps.

When investing in cyber security resources, information security managers have to follow effective decision-making strategies. We refer to this as the cyber security investment challenge.In this paper, we consider three possible decision support methodologies for security managers to tackle this challenge. We consider methods based on game theory, combinatorial optimisation , and a hybrid of the two. Our modelling starts by building a framework where we can investigate the effectiveness of a cyber security control regarding the protection of different assets seen as targets in presence of commodity threats. As game theory captures the interaction between the endogenous organisation's and attackers' decisions, we consider a 2-person control game between the security manager who has to choose among different implementation levels of a cyber security control, and a commodity attacker who chooses among different targets to attack. The pure game theoretical methodology consists of a large game including all controls and all threats. In the hybrid methodology the game solutions of individual control-games along with their direct costs (e.g. financial) are combined with a Knapsack algorithm to derive an optimal investment strategy. The combinatorial optimisation technique consists of a multi-objective multiple choice Knapsack based strategy. To compare these approaches we built a decision support tool and a case study regarding current government guidelines. The endeavour of this work is to highlight the weaknesses and strengths of different investment methodologies for cyber security, the benefit of their interaction, and the impact that indirect costs have on cyber security investment. Going a step further in validating our work, we have shown that our decision support tool provides the same advice with the one advocated by the UK government with regard to the requirements for basic technical protection from cyber attacks in SMEs .

Satisfiability Modulo Theories (SMT) is a decision problem for logical formulas over one or more first-order theories. In this paper, we study the problem of finding all solutions of an SMT problem with respect to a set of Boolean variables, henceforth All-SMT. First, we show how an All-SMT solver can benefit various domains of application: Bounded Model Checking, Automated Test Generation, Reliability analysis, and Quantitative Information Flow. Secondly, we then propose algorithms to design an All-SMT solver on top of an existing SMT solver, and implement it into a prototype tool, called aZ3. Thirdly, we create a set of benchmarks for All-SMT in the theory of linear integer arithmetic QF_LIA and the theory of bit vectors with arrays and uninterpreted functions QF_AUFBV. We compare aZ3 against Math SAT, the only existing All-SMT solver, on our benchmarks. Experimental results show that aZ3 is more precise than Math SAT.

Several mathematical ideas have been investigated for quantitative information flow. Information theory, probability, guessability are the main ideas in most proposals. They aim to quantifyhow much informationis leaked,how likely is to guessthe secret andhow long does it taketo guess the secret respectively. In this work, we investigate the relationship between these ideas in the context of the quantitative analysis of deterministic systems. We propose the lattice of information as a valuable foundation for these approaches; not only it provides an elegant algebraic framework for the ideas, but also to investigate their relationship. In particular, we will use this lattice to prove some results establishing order relation correspondences between the different quantitative approaches. The implications of these results w.r.t. recent work in the community is also investigated. While this work concentrates on the foundational importance of the lattice of information its practical relevance has been recently proven, notably with the quantitative analysis of Linux kernel vulnerabilities. Overall, we believe these works set the case for establishing the lattice of information as one of the main reference structure for quantitative information flow.

We present a novel method for Quantitative Information Flow analysis. We show how the problem of computing information leakage can be viewed as an extension of the Satisfiability Modulo Theories (SMT) problem. This view enables us to develop a framework for QIF analysis based on the framework DPLL(T) used in SMT solvers. We then show that the methodology of Symbolic Execution (SE) also fits our framework. Based on these ideas, we build two QIF analysis tools: the first one employs CBMC, a bounded model checker for ANSI C, and the second one is built on top of Symbolic PathFinder, a Symbolic Executor for Java. We use these tools to quantify leaks in industrial code such as C programs from the Linux kernel, a Java tax program from the European project HATS, and anonymity protocols.

In recent years, quantitative security techniques have been providing effective measures of the security of a system against an attacker. Such techniques usually assume that the system produces a finite amount of observations based on a finite amount of secret bits and terminates, and the attack is based on these observations. By modeling systems with Markov chains, we are able to measure the effectiveness of attacks on non-terminating systems. Such systems do not necessarily produce a finite amount of output and are not necessarily based on a finite amount of secret bits. We provide characterizations and algorithms to define meaningful measures of security for non-terminating systems, and to compute them when possible. We also study the bounded versions of the problems, and show examples of non-terminating programs and how their effectiveness in protecting their secret can be measured.

We report on our work-in-progress into the use of reliability analysis to quantify information leaks. In recent work we have proposed a software reliability analysis technique that uses symbolic execution and model counting to quantify the probability of reaching designated program states, e.g. assert violations, under uncertainty conditions in the environment. The technique has many applications beyond reliability analysis, ranging from program understanding and debugging to analysis of cyber-physical systems. In this paper we report on a novel application of the technique, namely Quantitative Information Flow analysis (QIF). The goal of QIF is to measure information leakage of a program by using information-theoretic metrics such as Shannon entropy or Renyi entropy. We exploit the model counting engine of the reliability analyzer over symbolic program paths, to compute an upper bound of the maximum leakage over all possible distributions of the confidential data.

This work, of a foundational nature, establishes a connection between secure computation and the 2nd principle of thermodynamics. In particular we show that any deterministic computation, where the final state of the system is observable, must dissipate at least W K_B T ln(2). Here W is the information theoretic notion of remaining uncertainty as defined in Quantitative Information Flow, K_B the Boltzmann constant and T the system temperature. By contrast, for probabilistic computations thermodynamic work can be extracted from secure systems: in this case, again using information theoretic results, we provide bounds on the amount of work that can be extracted. Further we show that in deterministic systems the dissipated energy is an upper bound on Smith's remaining vulnerability, by doing so we provide the first thermodynamic interpretation of guess ability. Crucially, unlike much literature on the physics of computation, our focus is not a universal model but a software field of great practical relevance, namely security. We see this work as a genuine scientific advance with the potential to enhance the understanding of both confidentiality and dissipative systems in physics.

Leakage of confidential information represents a serious security risk. Despite a number of novel, theoretical advances, it has been unclear if and how quantitative approaches to measuring leakage of confidential information could be applied to substantial, real-world programs. This is mostly due to the high complexity of computing precise leakage quantities. In this paper, we introduce a technique which makes it possible to decide if a program conforms to a quantitative policy which scales to large state-spaces with the help of bounded model checking.

Pasquale Malacaria; Program Analysis Probably Counts: Discussant Contribution for the Computer Journal Lecture by Chris Hankin, The Computer Journal, Volume 53,

There is a clear intuitive connection between the notion of leakage of information in a program and concepts from Information Theory. We explore this connection by interpreting Information Theory as a security risk assessment of programs. Information Theory will then be used to introduce techniques to reason on looping constructs, which are the kind of programs that previous quantitative models failed to satisfactory address. The semantics here introduced allows to describe both the amount and rate of leakage; if either is small enough, then a program might be deemed “secure”. Using the semantics we provide an investigation and classification of bounded and unbounded covert channels.

There is a natural intuitive match between anonymity and information theory. In particular, the maximal anonymity loss in anonymity protocols can be matched to the information theoretical notion of channel capacity.

There is a clear intuitive connection between the notion of leakage of information in a program and concepts from information theory. This intuition has not been satisfactorily pinned down, until now. In particular, previous information-theoretic models of programs are imprecise, due to their overly conservative treatment of looping constructs. In this paper we provide the first precise information-theoretic semantics of looping constructs. Our semantics describes both the amount and rate of leakage; if either is small enough, then a program might be deemed "secure". Using the semantics we provide an investigation and classification of bounded and unbounded covert channels.

We propose an approach to quantify interference in a simple imperative language that includes a looping construct. In this paper we focus on a particular case of this definition of interference: leakage of information from private variables to public ones via a Trojan Horse attack. We quantify leakage in terms of Shannon’s information theory and we motivate our definition by proving a result relating this definition of leakage and the classical notion of programming language interference. The major contribution of the paper is a quantitative static analysis based on this definition for such a language. The analysis uses some non-trivial information theory results like Fano’s inequality and the [Formula: see text] inequality to provide reasonable bounds for conditional statements. While-loops are handled by integrating a qualitative flow-sensitive dependency analysis into the quantitative analysis.

This paper uses Shannon's information theory to give a quantitative definition of information flow in systems that transform inputs to outputs. For deterministic systems, the definition is shown to specialize to a simpler form when the information source and the known inputs jointly determine all inputs uniquely. For this special case, the definition is related to the classical security condition of non-interference and an equivalence is established between non-interference and independence of random variables. Quantitative information flow for deterministic systems is then presented in relational form. With this presentation, it is shown how relational parametricity can be used to derive upper and lower bounds on information flows through families of functions defined in the second-order lambda calculus.

We present a unifying framework for using game semantics as a basis for program analysis. Also, we present a case study of the techniques. The unifying framework presents games-based program analysis as an abstract interpretation of an appropriate games category in the category of non-deterministic games. The case study concerns an application to security.

J.-Y. Girard (Proc. ASL Meeting, 1988) proposed an interpretation of second order lambda -calculus in a C algebra and showed that the interpretation of a term is a nilpotent operator. By extending to untyped lambda -calculus the functional analysis interpretation for typed lambda -terms, V. Danos (Proc. 3rd Italian Conf. on Theor. Comput. Sci., 1989) showed that all and only strongly normalizable terms are interpreted by nilpotent operators; in particular all and only nonstrongly normalizable terms are interpreted by infinite sums of operators. It is shown that interpretation of lambda -terms always makes sense, by showing that lambda -terms are interpreted by weakly nilpotent operators in the sense of Girard. This result is obtained as a corollary of an aperiodicity property of execution of lambda -terms, which seems to be related to some basic property of environment machines.>