Choreographic programming provides a high-level abstraction for writing distributed computations while ensuring deadlock-freedom by construction. HasChor, a Haskell-based choreographic programming framework, offers a practical implementation of these ideas but faces limitations in handling an arbitrary number of participants and optimizing the communication of branches. In this work, we introduce CloudChor, a set of extensions that enhance HasChor’s expressiveness and efficiency through the use of multiply-located values, allowing choreographies to distribute and collect data across multiple participants in a structured manner. Additionally, we refine HasChor’s branching mechanism through a lightweight static analysis, selectively propagating branching decisions only to relevant participants, reducing communication overhead. To strengthen theoretical guarantees, we establish a formal semantics for HasChor and our extensions, proving deadlock-freedom. Finally, we demonstrate the practicality of our enhancements by implementing a data clean room protocol using CloudChor. Our contributions improve the applicability of choreographic programming to cloud-based secure data collaborations, making it a stronger candidate for real-world deployments.

Differential Privacy (DP) is a cornerstone for ensuring privacy in data analysis by injecting carefully calibrated noise into statistical queries. While numerous DP tools focus on privacy protection, few provide accuracy information, specially for data-dependent computations like averages or quotients of DP-sums. This paper introduces a novel approach to compute confidence intervals, i.e., α-β accuracy, for these computations, leveraging principles from uncertainty propagation. Our method identifies conditions under which analytical error can be predicted, revealing two key invariants: the analytical error improves with large dataset sizes, and addition of values with higher variability require larger dataset sizes for accurate estimation. To simplify adoption, we also propose accuracy tuners to enable rapid determination of minimum dataset sizes and explore trade-offs between privacy budgets and the possibility to perform accuracy estimations. Our theoretical contributions are validated through an empirical evaluation that explores the applicability of fractional uncertainties for computing concrete α-β error across diverse scenarios.

The work of Fuzz has pioneered the use of functional programming languages where types allow reasoning about the sensitivity of programs. Fuzz and subsequent work (e.g., DFuzz and Duet) use advanced technical devices like linear types, modal types, and partial evaluation. These features usually require the design of a new programming language from scratch—a significant task on its own! While these features are part of the classical toolbox of programming languages, they are often unfamiliar to non-experts in this field. Fortunately, recent studies (e.g., Solo ) have shown that linear and complex types in general, are not strictly needed for the task of determining programs’ sensitivity since this can be achieved by annotating base types with static sensitivity information. In this work, we take a different approach. We propose to enrich base types with information about the metric relation between values, and we present the novel idea of applying parametricity to derive direct proofs for the sensitivity of functions. A direct consequence of our result is that calculating and proving the sensitivity of functions is reduced to simply type-checking in a programming language with support for polymorphism and type-level naturals. We formalize our main result in a calculus, prove its soundness, and implement a software library in the programming language Haskell-where we reason about the sensitivity of canonical examples. We show that the simplicity of our approach allows us to exploit the type inference of the host language to support a limited form of sensitivity inference. Furthermore, we extend the language with a privacy monad to showcase how our library can be used in practical scenarios such as the implementation of differentially private programs, where the privacy guarantees depend on the sensitivity of user-defined functions. Our library, called Spar , is implemented in less than 500 lines of code.

Trusted Execution Environments (TEEs) are hardware enforced memory isolation units, emerging as a pivotal security solution for security-critical applications. TEEs, like Intel SGX and ARM TrustZone, allow the isolation of confidential code and data within an untrusted host environment, such as the cloud and IoT. Despite strong security guarantees, TEE adoption has been hindered by an awkward programming model. This model requires manual application partitioning and the use of error-prone, memory-unsafe, and potentially information-leaking low-level C/C++ libraries.

Automatically-synthesized random data generators are an appealing option when using property-based testing. There exists a variety of techniques that extract static information from the codebase to produce random test cases. Unfortunately, such techniques cannot enforce the complex invariants often needed to test properties with sparse preconditions.Coverage-guided, property-based testing (CGPT) tackles this limitation by enhancing synthesized generators with structure-preserving mutations guided by execution traces. Albeit effective, CGPT relies largely on randomness and exhibits poor scheduling, which can prevent bugs from being found.We present MUTAGEN, a CGPT framework that tackles such limitations by generating mutants exhaustively. Our tool incorporates heuristics that help to minimize scalability issues as well as cover the search space in a principled manner. Our evaluation shows that MUTAGEN not only outperforms existing CGPT tools but also finds previously unknown bugs in real-world software.

Smart contracts are self-executing programs running in the blockchain allowing for decentralised storage and execution without a middleman. On-chain execution is expensive, with miners charging fees for distributed execution according to a cost model defined in the protocol. In particular, transactions have a high fixed cost. We present MultiCall, a transaction-batching interpreter for Ethereum that reduces the cost of smart contract executions by gathering multiple users’ transactions into a batch. Our current implementation of MultiCall includes the following features: the ability to emulate Ethereum calls and create transactions, both from MultiCall itself and using an identity unique to the user; the ability to cheaply pay Ether to other MultiCall users; and the ability to authorise emulated transactions on behalf of multiple users in a single transaction using hash-based authorisation rather than more expensive signatures. This improves upon a previous version of MultiCall. Our experiments show that MultiCall provides a saving between 57% and 99% of the fixed transaction cost compared with the standard approach of sending Ethereum transactions directly. Besides, we also show how to prevent an economic attack exploiting the metatransaction feature, describe a generic protocol for hash-based authorisation of metatransactions, and analyse how to minimise its off-chain computational and storage cost.

Embedded domain-specific languages (eDSLs) are typically implemented in a rich host language, such as Haskell, using a combination of deep and shallow embedding techniques. While such a combination enables programmers to exploit the execution mechanism of Haskell to build and specialize eDSL programs, it blurs the distinction between the host language and the eDSL. As a consequence, extension with features such as sums and effects requires a significant amount of ingenuity from the eDSL designer. In this paper, we demonstrate that Normalization by Evaluation (NbE) provides a principled framework for building, extending, and customizing eDSLs. We present a comprehensive treatment of NbE for deeply embedded eDSLs in Haskell that involves a rich set of features such as sums, arrays, exceptions and state, while addressing practical concerns about normalization such as code expansion and the addition of domain-specific features.

Differential privacy offers a formal framework for reasoning about the privacy and accuracy of computations on private data. It also offers a rich set of building blocks for constructing private data analyses. When carefully calibrated, these analyses simultaneously guarantee the privacy of the individuals contributing their data, and the accuracy of the data analysis results, inferring useful properties about the population. The compositional nature of differential privacy has motivated the design and implementation of several programming languages to ease the implementation of differentially private analyses. Even though these programming languages provide support for reasoning about privacy, most of them disregard reasoning about the accuracy of data analyses. To overcome this limitation, we present DPella, a programming framework providing data analysts with support for reasoning about privacy, accuracy, and their trade-offs. The distinguishing feature of DPella is a novel component that statically tracks the accuracy of different data analyses. To provide tight accuracy estimations, this component leverages taint analysis for automatically inferring statistical independence of the different noise quantities added for guaranteeing privacy. We evaluate our approach by implementing several classical queries from the literature and showing how data analysts can calibrate the privacy parameters to meet the accuracy requirements, and vice versa.

Language-based information-flow control (IFC) techniques often rely on special purpose, ad-hoc primitives to address different covert channels that originate in the runtime system, beyond the scope of language constructs. Since these piecemeal solutions may not compose securely, there is a need for a unified mechanism to control covert channels. As a first step towards this goal, we argue for the design of a general interface that allows programs to safely interact with the runtime system and the available computing resources. To coordinate the communication between programs and the runtime system, we propose the use of asynchronous exceptions (interrupts), which, to the best of our knowledge, have not been considered before in the context of IFC languages. Since asynchronous exceptions can be raised at any point during execution-often due to the occurrence of an external event-threads must temporarily mask them out when manipulating locks and shared data structures to avoid deadlocks and, therefore, breaking program invariants. Crucially, the naive combination of asynchronous exceptions with existing features of IFC languages (e.g., concurrency and synchronization variables) may open up new possibilities of information leakage. In this paper, we present MACasync, a concurrent, statically enforced IFC language that, as a novelty, features asynchronous exceptions. We show how asynchronous exceptions easily enable (out of the box) useful programming patterns like speculative execution and some degree of resource management. We prove that programs in MACasync satisfy progress-sensitive non-interference and mechanize our formal claims in the Agda proof assistant.

Differential privacy offers a formal framework for reasoning about privacy and accuracy of computations on private data. It also offers a rich set of building blocks for constructing private data analyses. When carefully calibrated, these analyses simultaneously guarantee the privacy of the individuals contributing their data, and the accuracy of the data analyses results, inferring useful properties about the population. The compositional nature of differential privacy has motivated the design and implementation of several programming languages aimed at helping a data analyst in programming differentially private analyses. However, most of the programming languages for differential privacy proposed so far provide support for reasoning about privacy but not for reasoning about the accuracy of data analyses. To overcome this limitation, in this work we present DPella, a programming framework providing data analysts with support for reasoning about privacy, accuracy and their trade-offs. The distinguishing feature of DPella is a novel component which statically tracks the accuracy of different data analyses. In order to make tighter accuracy estimations, this component leverages taint analysis for automatically inferring statistical independence of the different noise quantities added for guaranteeing privacy. We evaluate our approach by implementing several classical queries from the literature and showing how data analysts can figure out the best manner to calibrate privacy to meet the accuracy requirements.

Language-Based Information Flow Control (IFC) provides strong security guarantees for untrusted code, but often suffers from a non-negligible rate of false alarms. Multi-execution based techniques promise to provide security guarantees without raising any false alarms. However, all known multi-execution approaches introduce extraneous performance overheads which are rarely studied. In this work, we lay down the foundations for optimisation techniques aimed at reducing these overheads to a managable level, thus helping to make multi-execution more practical. We characterise our optimisations as data-and control-oriented. Data-oriented optimisations reduce storage overheads- which also helps to remove unnecessary repeated computations. In contrast, computation-oriented optimisations rely on program annotations in order to reduce needless computation. These annotations motivate the need for a new, stronger, theoretical notion of transparency- i.e., a stronger notion for characterising the lack of false alarms. To show the efficacy of our optimisation techniques, we apply them to two case-studies: a secure (faceted) database and a chat server written in a multi-execution based IFC framework. Our case-studies clearly show that our optimisations significantly reduce the storage and computational overhead, sometimes from exponential to polynomial order. All of our formal results are accompanied by mechanised proofs in Agda.

Categorical combinators offer a simpler alternative to typed lambda calculi for static analysis and implementation. Since categorical combinators are accompanied by a rich set of conversion rules which arise from categorical laws, they also offer a plethora of opportunities for program optimization. It is unclear, however, how such rules can be applied in a systematic manner to eliminate intermediate values such as exponentials, the categorical equivalent of higher-order functions, from a program built using combinators. Exponential elimination simplifies static analysis and enables a simple closure-free implementation of categorical combinators--reasons for which it has been sought after.

We show that fine-grained and coarse-grained dynamic information-flow control (IFC) systems are equally expressive. To this end, we mechanize two mostly standard languages, one with a fine-grained dynamic IFC system and the other with a coarse-grained dynamic IFC system, and prove a semantics-preserving translation from each language to the other. In addition, we derive the standard security property of non-interference of each language from that of the other, via our verified translation. This result addresses a longstanding open problem in IFC: whether coarse-grained dynamic IFC techniques are less expressive than fine-grained dynamic IFC techniques (they are not!). The translations also stand to have important implications on the usability of IFC approaches. The coarse- to fine-grained direction can be used to remove the label annotation burden that fine-grained systems impose on developers, while the fine- to coarse-grained translation shows that coarse-grained systems---which are easier to design and implement---can track information as precisely as fine-grained systems and provides an algorithm for automatically retrofitting legacy applications to run on existing coarse-grained systems.

To enforce non-interference, both Secure Multi-Execution (SME) and Multiple Facets (MF) rely on the introduction of multi-executions. The attractiveness of these techniques is that they are precise: secure programs running under SME or MF do not change their behavior. Although MF was intended as an optimization for SME, it does provide a weaker security guarantee for termination leaks. This paper presents Faceted Secure Multi Execution (FSME), a novel synthesis of MF and SME that combines the stronger security guarantees of SME with the optimizations of MF. The development of FSME required a unification of the ideas underlying MF and SME into a new multi-execution framework (Multef), which can be parameterized to provide MF, SME, or our new approach FSME, thus enabling an apples-to-apples comparison and benchmarking of all three approaches. Unlike the original work on MF and SME, Multef supports arbitrary (and possibly infinite) lattices necessary for decentralized labeling models---a feature needed in order to make possible the writing of applications where each principal can impose confidentiality and integrity requirements on data. We provide some micro-benchmarks for evaluating Multef and write a file hosting service, called ProtectedBox, whose functionality can be securely extended via third-party plugins.

We present Clio, an information flow control (IFC) system that transparently incorporates cryptography to enforce confidentiality and integrity policies on untrusted storage. Clio insulates developers from explicitly manipulating keys and cryptographic primitives by leveraging the policy language of the IFC system to automatically use the appropriate keys and correct cryptographic operations. We prove that Clio is secure with a novel proof technique that is based on a proof style from cryptography together with standard programming languages results. We present a prototype Clio implementation and a case study that demonstrates Clio's practicality.

Many state-of-the-art information-flow control (IFC) tools are implemented as Haskell libraries. A distinctive feature of this language is lazy evaluation. In his influencal paper on why functional programming matters, John Hughes proclaims:,,Lazy evaluation is perhaps the most powerful tool for modularization in the functional programmer's repertoire.,,Unfortunately, lazy evaluation makes IFC libraries vulnerable to leaks via the internal timing covert channel. The problem arises due to sharing, the distinguishing feature of lazy evaluation, which ensures that results of evaluated terms are stored for subsequent re-utilization. In this sense, the evaluation of a term in a high context represents a side-effect that eludes the security mechanisms of the libraries. A naïve approach to prevent that consists in forcing the evaluation of terms before entering a high context. However, this is not always possible in lazy languages, where terms often denote infinite data structures. Instead, we propose a new language primitive, lazyDup, which duplicates terms lazily. By using lazyDup to duplicate terms manipulated in high contexts, we make the security library MAC robust against internal timing leaks via lazy evaluation. We show that well-typed programs satisfy progress-sensitive non-interference in our lazy calculus with non-strict references. Our security guarantees are supported by mechanized proofs in the Agda proof assistant.

Many modern web-platforms are no longer written by a single entity, such as a company or individual, but consist of a trusted core that can be extended by untrusted third-party authors. Examples of this approach include Facebook, Yammer, and Salesforce. Unfortunately, users running third-party “app s” have little control over what the apps can do with their private data. Today’s platforms offer only ad hoc constraints on app behavior, leaving users an unfortunate trade-off between convenience and privacy. A principled approach to code confinement could allow the integration of untrusted code while enforcing flexible, end-to-end policies on data access. This paper presents a new framework, Hails, for building web platforms, that adds mandatory access control and a declarative policy language to the familiar MVC architecture. We demonstrate the flexibility of Hails by building several platforms, including GitStar, a code-hosting website that enforces robust privacy policies on user data even while allowing untrusted apps to deliver extended features to users.

Abstract We describe a language-based, dynamic information flow control (IFC) system called LIO. Our system presents a new design point for IFC, influenced by the challenge of implementing IFC as a Haskell library, as opposed to the more typical approach of modifying the language runtime system. In particular, we take a coarse-grained, floating-label approach, previously used by IFC Operating Systems, and associate a single, mutable label—the current label —with all the data in a computation's context. This label is always raised to reflect the reading of sensitive information and it is used to restrict the underlying computation's effects. To preserve the flexibility of fine-grained systems, LIO also provides programmers with a means for associating an explicit label with a piece of data. Interestingly, these labeled values can be used to encapsulate the results of sensitive computations which would otherwise lead to the creeping of the current label. Unlike other language-based systems, LIO also bounds the current label with a current clearance , providing a form of discretionary access control that LIO programs can use to deal with covert channels. Moreover, LIO provides programmers with mutable references and exceptions. The latter, exceptions, are used in LIO to encode and recover from monitor failures, all while preserving data confidentiality and integrity—this addresses a longstanding concern that dynamic IFC is inherently prone to information leakage due to monitor failure.

Environmental noise (e.g. heat, ionized particles, etc.) causes transient faults in hardware, which lead to corruption of stored values. Mission-critical devices require such faults to be mitigated by fault-tolerance -- a combination of techniques that aim at preserving the functional behaviour of a system despite the disruptive effects of transient faults. Fault-tolerance typically has a high deployment cost -- special hardware might be required to implement it -- and provides weak statistical guarantees. It is also based on the assumption that faults are rare. In this paper, we consider scenarios where security, rather than functional correctness, is the main asset to be protected. Our main contribution is a theory for expressing confidentiality of data in the presence of transient faults. We show that the natural probabilistic definition of security in the presence of faults can be captured by a possibilistic definition. Furthermore, the possibilistic definition is implied by a known bisimulation-based property, called Strong Security. We illustrate the utility of these results for a simple RISC architecture for which only the code memory and program counter are assumed fault-tolerant. We present a type-directed compilation scheme that produces RISC code from a higher-level language for which Strong Security holds -- i.e. well-typed programs compile to RISC code which is secure despite transient faults. In contrast with fault-tolerance solutions, our technique assumes relatively little special hardware, gives formal guarantees, and works in the presence of an active attacker who aggressively targets parts of a system and induces faults precisely.

Information-Flow Control (IFC) is a well-established approach for allowing untrusted code to manipulate sensitive data without disclosing it. IFC is typically enforced via type systems and static analyses or via dynamic execution monitors. The LIO Haskell library, originating in operating systems research, implements a purely dynamic monitor of the sensitivity level of a computation, particularly suitable when data sensitivity levels are only known at runtime. In this paper, we show how to give programmers the flexibility of deferring IFC checks to runtime (as in LIO), while also providing static guarantees---and the absence of runtime checks---for parts of their programs that can be statically verified (unlike LIO). We present the design and implementation of our approach, HLIO (Hybrid LIO), as an embedding in Haskell that uses a novel technique for deferring IFC checks based on singleton types and constraint polymorphism. We formalize HLIO, prove non-interference, and show how interesting IFC examples can be programmed. Although our motivation is IFC, our technique for deferring constraints goes well beyond and offers a methodology for programmer-controlled hybrid type checking in Haskell.

For several decades, researchers from different communities have independently focused on protecting confidentiality of data. Two distinct technologies have emerged for such purposes: Mandatory Access Control (MAC) and Information-Flow Control (IFC)—the former belonging to operating systems (OS) research, while the latter to the programming languages community. These approaches restrict how data gets propagated within a system in order to avoid information leaks. In this scenario, Haskell plays a unique privileged role: it is able to protect confidentiality via libraries. This pearl presents a monadic API which statically protects confidentiality even in the presence of advanced features like exceptions, concurrency, and mutable data structures. Additionally, we present a mechanism to safely extend the library with new primitives, where library designers only need to indicate the read and write effects of new operations.

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 often used to boost the permissiveness of the IFC monitor, by rejecting fewer programs, and to reduce the burden of explicit label annotations. However, when added naively, in a purely dynamic setting, mutable labels can expose a high bandwidth covert channel. In this work, we present an extension for LIO-a language-based 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 in a safe manner. To eliminate the burden of determining when a reference should be upgraded, we additionally provide a mechanism for automatic upgrades. Our approach naturally extends to a concurrent setting, not previously considered by dynamic 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, a surprising result on its own.

LIO is a decentralized information flow control (DIFC) system, implemented in Haskell. In this demo proposal, we give an overview of the LIO library and show how LIO can be used to build secure systems. In particular, we show how to specify high-level security policies in the context of web applications, and describe how LIO automatically enforces these policies even in the presence of untrusted code.

In the past years, researchers have been focusing on applying information flow security to web applications. These mechanisms should raise a minimum of false alarms in order to be applicable to millions of existing web pages. A promising technique to achieve this is secure multi-execution (SME). If a program is already secure, its secure multi- execution produces the same output events; otherwise, this correspondence is intentionally broken in order to preserve security. Thus, there is no way to know if unexpected results are due to bugs or due to semantics changes produced by SME. Moreover, SME provides no guarantees on the relative ordering of output events from different security levels. We argue that these shortcomings limit the applicability of SME. In this article, we propose a scheduler for secure multi- execution which makes it possible to preserve the order of output events. Using this scheduler, we introduce a novel com- bination between monitoring and SME, called multi-execution monitor, which raises alarms only for actions breaking the non-interference notion of ID-security for reactive systems. Additionally, we show that the monitor guarantees trans- parency even for CP-similarity, a progress-sensitive notion of observation.

When termination of a program is observable by an adversary, confidential information may be leaked by terminating accordingly. While this termination covert channel has limited bandwidth for sequential programs, it is a more dangerous source of information leakage in concurrent settings. We address concurrent termination and timing channels by presenting a dynamic information-flow control system that mitigates and eliminates these channels while allowing termination and timing to depend on secret values. Intuitively, we leverage concurrency by placing such potentially sensitive actions in separate threads. While termination and timing of these threads may expose secret values, our system requires any thread observing these properties to raise its information-flow label accordingly, preventing leaks to lower-labeled contexts. We implement this approach in a Haskell library and demonstrate its applicability by building a web server that uses information-flow control to restrict untrusted web applications.

We describe a new, dynamic, floating-label approach to language-based information flow control, and present an implementation in Haskell. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality, while ensuring that the current label exceeds the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance that provides a form of discretionary access control. In addition, programs may encapsulate and pass around the results of computations with different labels. We give precise semantics and prove confidentiality and integrity properties of the system.

This paper seeks to answer fundamental questions about trade-offs between static and dynamic security analysis. It has been previously shown that flow-sensitive static information-flow analysis is a natural generalization of flow-insensitive static analysis, which allows accepting more secure programs. It has been also shown that sound purely dynamic information-flow enforcement is more permissive than static analysis in the flow-insensitive case. We argue that the step from flow-insensitive to flow-sensitive is fundamentally limited for purely dynamic information-flow controls. We prove impossibility of a sound purely dynamic information-flow monitor that accepts programs certified by a classical flow-sensitive static analysis. A side implication is impossibility of permissive dynamic instrumented security semantics for information flow, which guides us to uncover an unsound semantics from the literature. We present a general framework for hybrid mechanisms that is parameterized in the static part and in the reaction method of the enforcement (stop, suppress, or rewrite) and give security guarantees with respect to termination-insensitive noninterference for a simple language with output.

End-to-End security of mobile code requires that the code neither intentionally nor accidentally propagates sensitive information to an adversary. Although mobile code is commonly multithreaded low-level code, there lack enforcement mechanisms that ensure information security for such programs. The modularity is three-fold: we give modular extensions of sequential semantics, sequential security typing, and sequential security-type preserving compilation that allow us enforcing security for multithreaded programs. Thanks to the modularity, there are no more restrictions on multithreaded source programs than on sequential ones, and yet we guarantee that their compilations are provably secure for a wide class of schedulers.

Timeout mechanisms are a useful feature for web applications. However, these mechanisms need to be used with care because, if used as-is, they are vulnerable to timing attacks. This paper focuses on internal timing attacks, a particularly dangerous class of timing attacks, where the attacker needs no access to a clock. In the context of client-side web application security, we present JavaScript-based exploits against the timeout mechanism of the DOM (document object model), supported by the modern browsers. Our experimental findings reveal rather liberal choices for the timeout semantics by different browsers and motivate the need for a general security solution. We propose a foundation for such a solution in the form of a runtime monitor. We illustrate for a simple language that, while being more permissive than a typical static analysis, the monitor enforces termination-insensitive noninterference.

Protecting confidentiality of data has become increasingly important for computing systems. Information-flow techniques have been developed over the years to achieve that purpose, leading to special-purpose languages that guarantee information-flow security in programs. However, rather than producing a new language from scratch, information-flow security can also be provided as a library. This has been done previously in Haskell using the arrow framework. In this paper, we show that arrows are not necessary to design such libraries and that a less general notion, namely monads, is sufficient to achieve the same goals. We present a monadic library to provide information-flow security for Haskell programs. The library introduces mechanisms to protect confidentiality of data for pure computations, that we then easily, and modularly, extend to include dealing with side-effects. We also present combinators to dynamically enforce different declassification policies when release of information is required in a controlled manner. It is possible to enforce policies related to what, by whom, and when information is released or a combination of them. The well-known concept of monads together with the light-weight characteristic of our approach makes the library suitable to build applications where confidentiality of data is an issue.

Li and Zdancewic have recently proposed an approach to provide information-flow security via a library rather than producing a new language from the scratch. They have shown how to implement such a library in Haskell by using arrow combinators. However, their approach only works with computations that have no side-effects. In fact, they leave as an open question how their library, and the mechanisms in it, need to be modified to consider these kind of effects. Another absent feature in the library is support for multithreaded programs. Information-flow in multi-threaded programs still remains as a challenge, and no support for that has been implemented yet. It is not surprising, then, that the two main stream compilers that provide information-flow security, Jif and FlowCaml, lack support for multithreading. Following ideas taken from literature, this paper presents an extension to Li and Zdancewic's library that provides information-flow security in presence of reference manipulation and multithreaded programs. Moreover, an online-shopping case study has been implemented to evaluate the proposed techniques. The case study reveals that exploiting concurrency to leak secrets is feasible and dangerous in practice and how our extension helps avoiding that. To the best of our knowledge, this is the first implemented tool to guarantee information-flow security in concurrent programs and the first implementation of a case study that involves concurrency and information-flow policies.

The problem of information flow in multithreaded programs remains an important open challenge. Existing approaches to specifying and enforcing information flow security often suffer from over-restrictiveness, relying on non-standard semantics, lack of compositionality, inability to handle dynamic threads, scheduler dependence, and efficiency overhead for code that results from security-enforcing transformations. This paper suggests a remedy for some of these shortcomings by developing a novel treatment of the interaction between threads and the scheduler. As a result, we present a permissive noninterference-like security specification and a compositional security type system that provably enforces this specification. The type system guarantees security for a wide class of schedulers and provides a flexible and efficiency-friendly treatment of dynamic threads