CSF 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. In capability-safe languages, components can access a resource only if they possess a capability for that resource. As a result, a programmer can prevent an untrusted component from accessing a sensitive resource by ensuring that the component never acquires the corresponding capability. In order to reason about which components may use a sensitive resource it is necessary to reason about how capabilities propagate through a system. This may be difficult, or, in the case of dynamically composed code, impossible to do before running the system.

To counter this situation, we propose extensions to capability-safe languages that restrict the use of capabilities according to declarative policies. We introduce two independently useful semantic security policies to regulate capabilities and describe language-based mechanisms that enforce them. Access control policies restrict which components may use a capability and are enforced using higher-order contracts. Integrity policies restrict which components may influence (directly or indirectly) the use of a capability and are enforced using an information-flow type system. Finally, we describe how programmers can dynamically and soundly combine components that enforce access control or integrity policies with components that enforce different policies or even no policy at all.

ABSTRACT. We present a set of novel techniques for architecture portable software fault isolation (SFI) together with a working, proved-sound prototype in the Coq proof assistant. Unlike traditional SFI, which relies on analysis of assembly-level programs, we analyze and rewrite programs in a compiler intermediate language, the Cminor language of the CompCert C compiler. But like traditional SFI, the compiler remains outside of the trusted computing base. By composing our program transformer with the verified back-end of CompCert, we can obtain binary modules that satisfy the SFI memory safety policy for any of CompCert's supported architectures (currently: PowerPC, ARM, and x86-32). This allows the same SFI analysis to be used across multiple architectures, greatly simplifying the most difficult part of deploying trustworthy SFI systems. Specifically, we prove that any program output by our transformer will be safe with respect to a modified Cminor operational semantics that respects the SFI policy. Further, we arrange that this safety extends to assembly code when our transformer is composed with CompCert. Finally, we argue that our transformer does not modify the observable behavior of safe executions in the Cminor semantics.

ABSTRACT. Digital forensics reports typically document the search process that has led to a conclusion; the primary means to verify the report is to repeat the search process. We believe that, as a result, the Trusted Computing Base for digital forensics is unnecessarily large and opaque.

We advocate the use of forensic certificates as intermediate artifacts between search and verification. Because a forensic certificate has a precise semantics, it can be verified without knowledge of the search process and forensic tools used to create it. In addition, this precision opens up avenues for the analysis of forensic specifications. We present a case study using the specification of a “deleted” file.

We propose a verification architecture that addresses the enormous size of digital forensics data sets. As a proof of concept, we consider a computer intrusion case study, drawn from the Honeynet project. Our Coq formalization yields a verifiable certificate of the correctness of the underlying forensic analysis. The Coq development for this case study is available at http://fpl.cs.depaul.edu/projects/forensics/.

ABSTRACT. A number of systems have been developed for dynamic information flow control (IFC). In such systems, the security policy is expressed by labeling input and output channels; it is enforced by tracking and checking labels on data. Some systems have been proved to enforce some form of noninterference (NI), formalized as a property of two runs of the program. In practice, NI is too strong and it is desirable to enforce some relaxation of NI that allows downgrading under constraints that have been classified as `what', `where', `who', or `when' policies. To encompass a broad range of policies, relational logic has been proposed as a means to specify and statically enforce policy. This paper shows how relational logic policies can be dynamically checked. To do so, we provide a new account of monitoring, in which the monitor state is viewed as an abstract interpretation of certain pairs of program runs.

ABSTRACT. Flow-sensitive analysis for information-flow control (IFC) allows data structures to have mutable security labels, i.e., labels that can change over the course of the computation. This feature is beneficial for several reasons: it often boosts permissiveness, reduces the burden of explicit annotations, and enables reuse of single-threaded data structures. However, in a purely dynamic setting, mutable labels can expose a covert channel capable of leaking secrets at a high rate. We present an extension for LIO---a language-level floating-label system--that safely handles flow-sensitive references. The key insight to safely manipulating the label of a reference is to not only consider the label on the data stored in the reference, i.e, the reference label, but also the label on the reference label itself. Taking this into consideration, we provide an upgrade primitive that can be used to change the label of a reference, when deemed safe. To eliminate the burden of determining when it is safe to upgrade a reference, we additionally provide a mechanism for the automatic upgrades. Our approach naturally extends to a concurrent setting, not previously considered by flow-sensitive systems. For both our sequential and concurrent calculi we prove non-interference by embedding the flow-sensitive system into the flow-insensitive LIO calculus; the embedding itself is a surprising result.

ABSTRACT. Research on information flow security for concurrent programs usually assumes sequential consistency although modern multi-core processors often support weaker consistency guarantees. In this article, we clarify the impact that relaxations of sequential consistency have on information flow security. We consider four memory models and prove for each of them that information flow security under this model does not imply information flow security in any of the other models. These results suggest that research on security needs to pay more attention to the consistency guarantees provided by contemporary hardware. The other main technical contribution of this article is a program transformation that soundly enforces information flow security under different memory models. This program transformation is significantly less restrictive than a transformation that first establishes sequential consistency and then applies a traditional information flow analysis for concurrent programs.

ABSTRACT. The perception of risk has been established as an important part of the study of human aspects of security research. Similarly, risk awareness is often considered a central precursor for the adoption of security mechanisms and how people use them and interact with them. However, the state of risk awareness in users during their everyday use of the modern Internet has not been studied in detail. While it is well known that users have a limited "budget" for security behavior and that trying to coerce them into considering additional risks does not work well, it remains unclear which risks are on users' minds and therefore already accounted for in terms of their budget. Hence, assessing which risks and which consequences users currently perceive when using information technology is an important and currently overlooked foundation to shape usability aspects of IT security mechanisms. In this paper, we present a survey of risk and consequence awareness in users, analyze how this may influence the current lack of adoption for improved security measures, and make recommendations how this situation can be alleviated.

ABSTRACT. This paper addresses security and safety choices that involve a decision on the timing of an action, either on a short- or a long-term scale. Examples of such decisions include when to make backups, when to patch, when to update passwords, or when to check the correctness of personal financial account information. We effectively combine survey measures with economic experiments to better understand how performance in timing-related security situations is shaped by individuals' cognitive predispositions. Our work is aimed to explore timing-relevant cognitive biases and to eventually develop strategies to help decision-makers with behavioral intervention strategies. Two behavioral experiments are presented in which the timing of online security actions is the critical decision-making factor. We distinguish between visual feedback and estimation (Experiment 1) and purely temporal estimation (Experiment 2). Using psychometric scales, we investigate the role of individual difference variables, specifically risk propensity and need for cognition. The analysis is based on the data from over 450 participants and a careful statistical methodology. Risk propensity is not a hindrance in timing tasks. Participants of average risk propensity generally benefit from a reflective disposition (high need for cognition), particularly when visual feedback is given. Overall, participants benefit from need for cognition; in the more difficult, temporal-estimation task, this requires task experience.

ABSTRACT. Attribute-based encryption (ABE) has attracted considerable attention in the research community in recent years. It has a number of applications such as broadcast encryption and the cryptographic enforcement of access control policies. Existing instantiations of ABE make use of access structures encoded either as trees of Shamir threshold secret-sharing schemes or monotone span programs. In both cases, the appropriate computations for these schemes need to be interleaved with the standard operations for cryptographic pairings. Moreover, the resulting schemes are not particularly appropriate for access control policies. In this paper, therefore, we start by examining the representation of access control policies and investigate alternative secret-sharing schemes that could be used to enforce them. We develop new ABE schemes based on the Benaloh-Leichter scheme, which employs only elementary arithmetic operations, and then extend this to arbitrary linear secret sharing schemes. We then compare the complexity of existing schemes with our scheme based on Benaloh-Leichter.

ABSTRACT. Block cipher modes of operation provide a mechanism for encrypting arbitrary length messages based on block ciphers having some fixed (small) block size. Existing techniques for proving modes secure under standard security definitions require analyzing the global behavior of the mode. We propose a new approach which requires only \emph{local} analysis of a single block. As part of our approach, we model modes of operations as graphs, and specify a set of type-inference rules over the edges of the graph. This allows us to reduce the question of security (against chosen-plaintext attacks) for some mode to the question of whether the graph has a consistent type assignment, which in turn can be reduced to a question of boolean satisfiability. We couple this security-analysis tool with a synthesizer that automatically generates viable modes using an SMT solver.

ABSTRACT. Many algorithms admit very efficient batch versions that compute simultaneously the output of the algorithms on a set of inputs. Batch algorithms are widely used in cryptography, especially in the setting of pairing-based computations, where they deliver significant speed-ups.

AutoBatch is an automated tool that computes highly optimized batch verification algorithms for pairing-based signature schemes. Thanks to finely tuned heuristics, AutoBatch is able to rediscover efficient batch verifiers for several signature schemes of interest, and in some cases to output batch verifiers that outperform the best known verifiers from the literature. However, \AutoBatch only provides weak guarantees (in the form of a LaTeX proof) of the correctness of the batch algorithms it outputs. In this paper, we verify the correctness and security of these algorithms using the EasyCrypt framework. To achieve this goal, we define a domain-specific language to describe verification algorithms based on pairings and provide a very efficient algorithm for checking (approximate) observational equivalence between expressions of this language. By translating the output of AutoBatch to this language and applying our verification procedure, we obtain machine-checked correctness proofs of the batch verifiers. Moreover, we formalize notions of security for batch verifiers and we provide a generic proof in EasyCrypt that batch verifiers satisfy a security property called screening, provided they are correct and the original signature is unforgeable against chosen-message attacks. We apply our techniques to several well-known pairing-based signature schemes from the literature, and to Groth-Sahai proofs in the SXDH setting.

ABSTRACT. A signature scheme is malleable if, on input a message m and a signature s, it is possible to efficiently compute a signature s' on a related message m' = T(m), for a transformation T that is allowed with respect to this signature scheme. In this paper, we first provide new definitions for malleable signatures that allow us to capture a broader range of transformations than was previously possible. We then give a generic construction based on malleable zero-knowledge proofs that allows us to construct malleable signatures for a wide range of transformation classes, with security properties that are stronger than those that have been achieved previously. Finally, we construct delegatable anonymous credentials from signatures that are malleable with respect to an appropriate class of transformations (that we show our malleable signature supports). The resulting instantiation satisfies a stronger security notion than previous schemes while also scaling linearly with the number of delegations.

ABSTRACT. The Secure Web Bulletin Board (WBB) is a key component of verifiable election systems. However, there is very little in the literature on their specification, design and implementation, and there are no formally analysed designs. The WBB is used in the context of election verification to publish evidence of voting and tallying that voters and officials can check, and where challenges can be launched in the event of malfeasance. In practice, the election authority has responsibility for implementing the web bulletin board correctly and reliably, and will wish to ensure that it behaves correctly even in the presence of failures and attacks. To ensure robustness, an implementation will typically use a number of peers to be able to provide a correct service even when some peers go down or behave dishonestly. In this paper we propose a new protocol to implement such a Web Bulletin Board, motivated by the needs of the vVote verifiable voting system. Using a distributed algorithm increases the complexity of the protocol and requires careful reasoning in order to establish correctness. Here we use the Event-B modelling and refinement approach to establish correctness of the peered design against an idealised specification of the bulletin board behaviour. In particular we have shown that for n peers, a threshold of t > 2n/3 peers behaving correctly is sufficient to ensure correct behaviour of the bulletin board distributed design. The algorithm also behaves correctly even if honest or dishonest peers temporarily drop out of the protocol and then return. The verification approach also establishes that the protocols used within the bulletin board do not interfere with each other. This is the first time a peered secure web bulletin board suite of protocols has been formally verified.

ABSTRACT. Secure multiparty computation systems are commonly built form a small set of primitive components. Composability of security notions has a central role in the analysis of such systems, since it allows us to deduce security properties of complex protocols from the properties of its components. We show that the standard notions of universally composable security are overly restrictive in this context and can lead to protocols with sub-optimal performance. As a remedy, we introduce a weaker notion of privacy that it is satisfied by simpler protocols and is preserved by composition. After that we fix a passive security model and show how to convert a private protocol into a universally composable protocol. As a result, we obtain modular security proofs without performance penalties.

ABSTRACT. Many protocols use the Diffie-Hellman method for key agreement, in combination with certified long-term values or digital signatures for authentication. These protocols aim at security goals such as key secrecy, forward secrecy, resistance to key compromise attacks, and various flavors of authentication. However, analysis of these protocols has been challenging, both in the computational model and in the symbolic model. An obstacle in the symbolic model is the undecidability of unification in many theories such as rings.

In this paper, we develop an algebraic version of the symbolic approach, in which we work directly within finite fields. These are natural structures for the protocols. The adversary, in giving a counterexample to a protocol goal in a finite field, may rely on any identity in that field. He defeats the protocol if there are counterexamples in infinitely many finite fields.

We prove that, even for this strong adversary, security goals for a wide class of protocols are decidable.

ABSTRACT. Automated analysis of protocols involving Diffie-Hellman key exchange is challenging, in part because of the undecidability of the unification problem in relevant theories. In this paper, we justify the use of a more restricted theory that includes multiplication of exponents but not addition, providing unitary and efficient unification.

To justify this theory, we link it to a computational model of non-uniform circuit complexity through several incremental steps. First, we give a model closely analogous to the computational model, in which derivability is modeled by closure under simple algebraic transformations. This model retains many of the complex features of the computational model, including defining success based on asymptotic probability for a non-uniform family of strategies. We describe an intermediate model based on formal polynomial manipulations, in which success is exact and there is no longer a parametrized notion of the strategy. Despite the many differences in form, we are able to prove an equivalence between the asymptotic and intermediate models by showing that a sufficiently successful asymptotic strategy implies the existence of a perfect strategy. Finally, we describe a symbolic model in which addition of exponents is not modeled, and prove that (for expressible problems), the symbolic model is equivalent to the intermediate model.

ABSTRACT. Despite Alice’s best efforts, her long-term secret keys may be revealed to an adversary. Possible reasons include weakly generated keys, compromised key storage, subpoena, and coercion. However, Alice may still be able afterwards to communicate securely with other parties. Whether this is possible depends on the protocol used. We call the associated property resilience against Actor Key Compromise (AKC). We formalise this property in a symbolic model and identify conditions under which it can and cannot be achieved. In case studies that include TLS and SSH, we find that many protocols are not resilient against AKC. We implement a concrete AKC attack on the mutually authenticated TLS protocol.

ABSTRACT. In formal verification, cryptographic messages are often represented by algebraic terms. This abstracts not only from the intricate details of the real cryptography, but also from the details of the non-cryptographic aspects: the actual formatting and structuring of messages.

We introduce a new algebraic model to include these details and define a small, simple language to precisely describe message formats. We support fixed-length fields, variable-length fields with offsets, tags, and encodings into smaller alphabets like Base64, thereby covering both classical formats as in TLS and modern XML-based formats.

We define two reasonable properties for formats. First, they should be un-ambiguous: for a given format, any string can be parsed in at most one way. Second, they should be pairwise disjoint: a string can be parsed as at most one of the formats. We show how to easily establish these properties for many practical formats.

An abstract model is obtained by replacing the formats with free function symbols. This abstract model is compatible with all existing verification tools. We prove that the abstraction is sound for un-ambiguous, disjoint formats: there is an attack in the concrete message model if (and actually only if) there is one in the abstract message model.

ABSTRACT. To achieve end-to-end security in a system built from parts, it is important to ensure that the composition of secure components is itself secure. This work investigates the compositionality of two popular conditions of possibilistic noninterference. The first condition, progress-insensitive noninterference (PINI), is the security property enforced by practical tools like JSFlow, Paragon, LIO, Jif, FlowCaml, and SPARK Examiner. We show that this condition is not preserved under fair parallel composition: composing a PINI system fairly with another PINI system can yield an insecure system. We explore constraints that allow recovering compositionality for PINI. Further, we develop a theory of compositional reasoning and enforcement for progress-sensitive noninterference (PSNI). Our work is performed within a general framework for nondeterministic interactive systems.

ABSTRACT. We propose a novel mechanism for enforcing information flow policies with support for declassification on event-driven programs. Declassification policies consist of two functions. First, a projection function specifies for each confidential event what information in the event can be declassified directly. This generalizes the traditional security labelling of inputs. Second, a stateful release function specifies the aggregate information about all confidential events seen so far that can be declassified. We provide evidence that such declassification policies are useful in the context of JavaScript web applications. An enforcement mechanism for our policies is presented and its soundness and precision is proven. Finally, we give evidence of practicality by implementing and evaluating the mechanism in a browser.

ABSTRACT. Protecting sensitive information from improper disclosure is a fundamental security goal. It is complicated, and difficult to achieve, often because of unavoidable or even unpredictable operating conditions that lead to breaches in planned security defences. An attractive approach is to frame the goal as a quantitative problem, and then to design methods that allow system vulnerabilities to be measured in terms of the amount of information that they leak. A consequence of this view is that the precise operating conditions and any assumptions about prior knowledge can play a crucial role in assessing the severity of any measured vunerability.

We develop this theme by concentrating on robustness of vulnerability measurements: we wish to allow general leakage bounds to be placed on a program, whatever its operating conditions and whatever the prior knowledge might be. In particular we propose a theory of channel capacity, generalizing Shannon capacity from information theory, that can apply both to additive- and to multiplicative forms of a recently-proposed measure known as g-leakage. Further, we explore the computational aspects of calculating these capacities: we show that one of these scenarios can be solved efficiently by expressing it as a Kantorovich distance, and that another is NP-complete. We also show capacity bounds for a scenario related to Dalenius's Desideratum.

ABSTRACT. This risk of catastrophe from an attack is a consequence of a network's structure formed by the connected individuals, businesses and computer systems. Understanding the likelihood of extreme events, or, more generally, the probability distribution of the number of compromised nodes is an essential requirement to provide risk-mitigation or cyber-insurance. However, previous network security research has not considered the higher moments of this distribution, while previous cyber-insurance research has not considered the effect of topologies on the supply side.

We provide a mathematical basis for bridging this gap: we study the complexity of computing these loss-number distributions, both generally and for special cases of common real-world networks. In the case of scale-free networks, we demonstrate that expected loss alone cannot determine the riskiness of a network, and that this riskiness cannot be naively estimated from smaller samples, which highlights the lack/importance of topological data in security incident reporting.

ABSTRACT. Attack trees are widely used to represent threat scenarios in a succinct and intuitive manner, suitable for conveying security information to non-experts. The manual construction of such objects relies on the creativity and experience of specialists, and therefore it is error-prone and impracticable for large systems. Nonetheless, the automated generation of attack trees has only been explored in connection to computer networks and levering rich models, whose analysis typically leads to an exponential blow-up of the state space. We propose a static analysis approach where attack trees are automatically inferred from a process algebraic specification in a syntax-directed fashion, encompassing a great many application domains and avoiding incurring systematically an exponential explosion. Moreover, we show how the standard propositional denotation of an attack tree can be used to phrase interesting quantitative problems, that can be solved through an encoding into Satisfiability Modulo Theories. The flexibility and effectiveness of the approach is demonstrated on the study of a national-scale authentication system, whose attack tree is computed thanks to a Java implementation of the framework.

ABSTRACT. The management and specification of access control that enforce a given policy is a non-trivial, complex, and time consuming task. In this paper we aim at simplifying this task both at specification and verification levels. For that, we propose a formal model of Netfilter, a firewall system integrated in the Linux kernel. We define an abstraction of the concepts of chains, rules, and packets existent in Netfilter configurations, and give a semantics that mimics packet filtering and address translation. We then introduce a simple but powerful language that permits to specify firewall configurations which are unaffected by the relative ordering of rules and that does not depend on the underlying Netfilter chains. We give a semantics for this language and show that it can be translated into our Netfilter abstraction. We present Mignis, a publicly available tool that translates abstract firewall specifications into real Netfilter configurations. Mignis is currently used to configure the whole firewall of the DAIS Department of Ca’ Foscari University.

ABSTRACT. Enforcing protection at the browser side has recently become a popular approach for securing web authentication. Though interesting, existing attempts in the literature only address specific classes of attacks, and thus fall short of providing robust foundations to reason on web authentication security. In this paper we provide such foundations, by introducing a novel notion of web session integrity, which allows us to capture many existing attacks and spot some new ones. We then propose FF+, a security-enhanced model of a web browser that provides a full-fledged and provably sound enforcement of web session integrity. We leverage our theory to develop SessInt, a prototype extension for Google Chrome implementing the security mechanisms formalized in FF+. SessInt provides a level of security very close to FF+, while keeping an eye at usability and user experience.

ABSTRACT. The anonymous communication protocol Tor constitutes the most widely deployed technology for providing anonymity for user communication over the Internet. Several frameworks have been proposed that show strong anonymity guarantees; none of these, however, are capable of modeling the class of traffic-related timing attacks against Tor, such as traffic correlation and website fingerprinting.

In this work, we present GATA: the first framework that allows for establishing strong anonymity guarantees in the presence of time-sensitive adversaries that mount traffic-related timing attacks. GATA incorporates a comprehensive notion of time in an asynchronous communication model with sequential activation, while offering strong compositionality properties for security proofs. We apply GATA to evaluate a novel countermeasure for Tor against website fingerprinting attacks. Our analysis relies on a formalization of the onion routing protocol that underlies Tor and proves rigorous anonymity guarantees in the presence of traffic-related timing attacks.

ABSTRACT. \emph{Differential privacy} is becoming a gold standard for privacy research; it offers a guaranteed bound on loss of privacy due to release of query results, even under worst-case assumptions. The theory of differential privacy is an active research area, and there are now differentially private algorithms for a wide range of interesting problems.

However, the question of when differential privacy works \emph{in practice} has received relatively little attention. In particular, there is still no rigorous method for choosing the key parameter ϵ, which controls the crucial tradeoff between the strength of the privacy guarantee and the accuracy of the published results.

In this paper, we examine the role that these parameters play in concrete applications of differential privacy, identifying the key challenges that must be addressed when choosing specific values. This choice requires balancing the interests of two different parties: the data {\em analyst} and the prospective {\em participant}, who must decide whether to allow their data to be included in the analysis. We propose a simple model that expresses this balance as formulas over a handful of parameters. We illustrate the model with several scenarios, including a medical study and a study of movie ratings data. We also explore a surprising insight: in some circumstances, a differentially private study can be \emph{more accurate} than a non-private study for the same cost, under our model. Finally, we discuss a number of simplifying assumptions in our model and outline a research agenda for possible refinements.

ABSTRACT. \emph{Differential privacy} is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the program's distribution on outputs. More technically, differential privacy is a quantitative 2-safety property that bounds the distance between the output distributions of a probabilistic program on adjacent inputs. Like many 2-safety properties, differential privacy lies outside the scope of traditional verification techniques. Existing approaches to enforce privacy are based on intricate, non-conventional type systems, or customized relational logics. These approaches are difficult to implement and often cumbersome to use.

We present an alternative approach that verifies differential privacy by standard, non-relational reasoning on non-probabilistic programs. Our approach is based on transforming a probabilistic program into a non-probabilistic program which simulates two executions of the original program. We prove that if the target program is correct with respect to a Hoare specification, then the original probabilistic program is differentially private. We provide a variety of examples from the differential privacy literature to demonstrate the utility of our approach. Finally, we compare our approach with existing verification techniques for privacy.

ABSTRACT. Privacy is a core human need, but society sometimes has the requirement to do targeted, proportionate investigations in order to provide security. To reconcile individual privacy and societal security, we explore whether we can have surveillance in a form that is verifiably accountable to citizens. This means that citizens get verifiable proofs of the quantity and nature of the surveillance that actually takes place. In our scheme, governments are held accountable for the extent to which they exercise their surveillance power, and political parties can pledge in election campaigns their intention about reducing (or increasing) this figure.

We propose a general idea of {\em accountable escrow} and motivate this idea as an approach to reconciling and balancing the requirements of individual privacy and societal security. We design a balanced crypto system for asynchronous communication (e.g., email). We propose a novel method for escrowing the decryption capability in public-key cryptography. A government can decrypt it in order to conduct targetted surveillance, but doing so necessarily puts records in a public log against which the government is held accountable.