Reproducibility crisis in science, including computational sciences, is a serious, well-known, and well-documented problem, which demands an outstanding effort from the entire research community to be solved. In order to bridge this aforementioned reproducibility gap, Information Systems (IS) journal has launched a novel reproducibility initiative to allow the exact replication of published results in a fast, reliable, and straightforward manner, which consists in inviting authors to publish reproducible papers providing a detailed reproducibility protocol, together with a supplementary collection of software and data. This talk introduces the IS reproducibility initiative, as well as the reproducibility practices encouraged by it, and some examples of reproducible papers.
Suplementary documents: Talk Slides, Reproducibility guidelines

Group signatures allow user data to be collected while preserving the user's privacy but still ensuring it originates from a group member. However, the correlation of data by user is useful for processing data. Therefore, the linkability, i.e. whether signatures can be linked by user, must balance utility and privacy. We first introduce a new variant of group signature scheme that provides a more flexible and privacy-friendly form of linkability. When created, all signatures are fully unlinkable, but can be made linkable via an oblivious centrally trusted entity known as the converter. The conversion takes a batch of group signatures and blindly transforms signatures originating from the same user into a consistent representation. We formally define the requirements for this new type of group signature scheme and provide an efficient instantiation that provably satisfies these requirements. Our original model captures a setting where the entity collecting and processing data is the same. Therefore, when defining security, the data collector is assumed to only submit honest inputs to the converter. The outputs of the converter do not provide any assurance that data originated from a group member. We therefore extend the previous model to remove this assumption and allow authentication to be preserved after data is converted. To provide a provably secure construction in this stronger model we use controlled-malleable NIZKs, which allow proofs to be mauled in a controlled manner. This allows signatures to be blinded, while still ensuring they can be verified during conversions.

What do Apple, the FBI and a Belgian politician have in common? In 2003, in Belgium there was an electronic election and mysteriously one candidate got 4096 extra votes. After counting the total number of voters there was an extra of 4096. An accurate analysis led to the official explanation that a spontaneous creation of a bit in position 13 of the memory of the computer attributed 4096 extra votes to one candidate. One of the most credited answers to this apparently mysterious event is attributed to gamma rays, which can filter through the atmosphere. Indeed, soft-errors such as bitflips are frequent faults especially in outer space, where there's no atmosphere which protects from ionizing radiations such as gamma-rays, which are quite common in outer space. For this reason many space enabled devices mount very expensive and technically advanced memories, to reduce risks of malfunction, breakage or exploit. On the other hand, at ground level our devices aren't equipped with such memories for economic and statistical reasons. Indeed, research in the area shows that gamma rays filter inside the atmosphere, and normally hit our computers every day but mostly they hit unallocated memory and we do not notice their effects. There are cases though, like forensics, where such soft-errors may be helpful. In 2016 the FBI demanded Apple to unlock (decrypt) one of its phones (iPhone 5C) after the San Bernardino's shooting. Apple denied the decryption of the phone alleging that it would put the privacy of millions of users at risk. For this reason the FBI resorted to an Israeli company, which for a single phone charged around 1M USD, successfully reverse engineered the phone and broke into it. This study strives to leverage gamma rays to obtain a row-hammer style effect to cheaply break into a phone without resorting to expensive techniques beyond a radiotherapy session which could be held in a common hospital of western countries. Our preliminary results show as expected that on older memories (+15 years) low radioactive emissions (within 0.4 and 1.4 MeV) produce some side effects, while on modern memory such power is not sufficient. Our hypothesis is to prove that higher emissions, within the radiotherapy range (5-15 MeV) could be enough to generate soft-errors in contemporary COTS electronic devices and consequently allow to unlock/exploit a device by using ionizing radiations. Either by using row-hammer style techniques based on page table spraying or by knowing the memory configuration of a similar unlocked phone and shooting in the right place.

In this talk, I will make an introduction to the paradigm of Answer Set Programming (ASP) and its extension for temporal reasoning. In the first part of the talk, we will see the basic propositional semantics under a logical perspective (using Equilibrium Logic) and explain how this logical encoding relates to the most usual logic programming definition of answer sets. We will then review the most frequent features of the ASP language used in practice, presenting several examples that illustrate the use of variables and some frequent constructs like choice rules, aggregates or minimization. I will also briefly comment about the typical implementation of ASP solvers, separating the process of variable removal (grounding) from the purely propositional solving (which is closer to SAT solvers). In the last part of the talk, we will focus on an extension of Equilibrium Logic and ASP to deal with temporal reasoning, incorporating temporal operators from Linear-time Temporal Logic.

This talk is scoped for both cryptographers and non-cryptographers. I will start by introducing two of the most active research areas in modern cryptography: secure (multi-party) computation (MPC) and (privacy-preserving) verifiable computation (VC). In MPC protocols, a set of mutually distrusting participants want to jointly compute some function of their choice on their secret data, while keeping their inputs private. In VC, external parties which did not take part in some computation f(x)=y want to make sure that y was indeed computed by applying f to the (potentially hidden) input x. The second part of the talk will describe in more detail Succint Non-Interactive ARguments of Knowledge (SNARKs). SNARKs are an important building block for VC, credential systems, cryptocurrencies and privacy-preserving variants thereof. However, most of current SNARK constructions assume that the statements to be proven can be efficiently represented as either Boolean or arithmetic circuits over finite fields. Furthermore, the field choice is almost always limited by the application of secure bilinear maps in the verification procedure. After explaining the details of field-restricted SNARKs I will present Rinocchio, a designated-verifier SNARKs for statements which are represented as circuits over more general commutative rings, namely those containing big enough exceptional sets. Exceptional sets consist of elements satisfying the property that their pairwise differences are invertible. Along the way, we introduce Quadratic Ring Programs (QRPs) as a characterization of NP where the arithmetic is over a ring. We also study and generalize pre-existent (knowledge-type) assumptions employed in field-restricted SNARKs to the ring context. We propose two applications for Rinocchio: zk-SNARKs for the integers modulo 2^k (e.g. privately applying a Machine Learning model to the Verifier’s data) and VC over encrypted data, for which we can efficiently support more homomorphic encryption schemes and parameters than state-of-the art SNARKs.

Malware analysis systems are one of the best weapons in the arsenal of cybersecurity companies and researchers. An integral part of such systems is a sandbox providing an instru-mented and isolated environment to run unknown artifacts and observe their behavior to identify potentially malicious actions. In order to avoid detection, attackers have developed numerous techniques to make analysis harder. One class of anti-analysis attacks is based on the observation that it is not only the sandbox that monitors the behavior of the runningprogram; the program itself can also monitor its surrounding environment to detect the presence of a sandbox and try to evade it. This is usually achieved by looking for artifacts sug-gesting that the execution environment is a sandbox, such as specific memory patterns, behavioral traits of certain CPUinstructions (known as red pills), or parallel running processes of known Virtual Machine (VM) vendors. To mitigate this threat, sophisticated sandboxes remove or spoof these signals, thus making it harder for a malware sample to detect the emulated environment. In this paper we devise a new evasion strategy based on Proof-of-Work (PoW) algorithms that show an asymptotic behavior, in terms of computational cost, when they run on some class of hardware platform. To this end such algorithms can be used to effectively detect virtualized environments (e.g., malware sandbox analysis). To prove the validity of this intuition, we design and implementScrambleSuit: a tool that is able to automatically implement such detection strategies and embed a test evasion program into an arbitrary malware sample. Evaluation results show that the proposed detection technique can evade the most popular public sandboxes.

Database Management Systems (DBMS) are used ubiquitously for storing and retrieving data. It is critical that they function correctly --- incorrectly computed result sets (e.g., by omitting a row) can cause serious loss or damage. We refer to such defects as logic bugs. Despite their importance, finding logic bugs in production DBMS is a longstanding challenge. Existing techniques such as fuzzing and differential testing are ineffective in finding them. We have proposed a set of novel techniques to effectively detect logic bugs by tackling the two core technical issues: generating test queries and constructing test oracles. We approach from three distinct conceptual angles: (1) generating queries so that a given row is included in their result sets, (2) translating a given query to suppress optimizations and provide reference results, and (3) partitioning a query into multiple queries whose combined result is identical to the original query's result. We designed, realized and evaluated these approaches on a range of widely-used, production-quality DBMS including SQLite, MySQL, PostgreSQL, CockroachDB, and TiDB. To date, we have reported over 400 unique previously unknown bugs in these systems, over 350 of which have been fixed by the developers. Notably, half of our reports were logic bugs, while the remaining errors and crash bugs. Our work has provided solid methodological and technical bases for effectively testing DBMS in practice and already started seeing industrial adoption.

The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert’s control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical infrastructure, the POSIX shell is maligned and misunderstood. Its power and its subtlety are a dangerous combination.

We define a formal, mechanized, executable small-step semantics for the POSIX shell, which we call Smoosh. We compared Smoosh against seven other shells that aim for some measure of POSIX compliance (bash, dash, zsh, OSH, mksh, ksh93, and yash). Using three test suites—the POSIX test suite, the Modernish test suite and shell diagnosis, and a test suite of our own device—we found Smoosh’s semantics to be the most conformant to the POSIX standard. Modernish judges Smoosh to have the fewest bugs (just one, from using dash’s parser) and no quirks. To show that our semantics is useful beyond yielding a conformant, executable shell, we also implemented a symbolic stepper to illuminate the subtle behavior of the shell.

Smoosh will serve as a foundation for formal study of the POSIX shell, supporting research on and development of new shells, new tooling for shells, and new shell designs.

This talk will refine and extend my POPL 2020 talk with technical detail on the POSIX shell itself, on Smoosh's implementation, and on future directions.

This is joint work with Austin J. Blatt, now an engineer at Puppet Labs.

Modern graph query engines are gaining momentum, driven by exponentially growing, interconnected data volumes that populate scientific and industrial repositories, as part of the Linked Open Data and the Semantic Web. While successful commercial implementations exist, no standard graph query language has emerged and, despite the mature tools developed in the formal methods community and the security-sensitive applications currently involving graph-shaped data, no principled framework for the reliable evaluation of such queries has been proposed. In this talk, I will explain how we can address these issues, by employing the Coq proof assistant to develop a mechanically-certified engine for evaluating graph queries and for incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD), a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as a native operator. To this end, we mechanize an RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq program extraction mechanism, we test an OCaml version of the verified engine on a set of preliminary benchmarks, confirming the feasibility of obtaining a unified, machine-verified, formal framework for graph query processing.

In response to incidents of unintended disclosure and misuse of user data by online services, modern data protection regulations require service providers to restrict their collection, processing, sharing and storage of sensitive user data. However, ensuring compliance with such regulation in today's complex and rapidly evolving systems is technically challenging. In my research, I have developed practical systems to prevent unintended disclosures and misuse of data in the face of two broad classes of threats: software bugs and misconfiguration, and side channels. In this talk, I will describe Pacer, a compliance system designed to prevent indirect inference of sensitive data via side channels in shared network links in the Cloud. Pacer shapes the outbound traffic of a Cloud tenant to make it independent of the tenant's secrets. At the same time, Pacer does allow variations in the traffic shape based only on public (non-secret) aspects of the tenants' workloads, thus enabling efficient sharing of network resources and incurring moderate overhead. Implementing Pacer requires modest changes to the Cloud hypervisor and the guest OS, and minimal changes to the guest application.

Software correctness is becoming an increasingly important concern as our society grows more and more reliant on computer systems. Even the simplest of software errors can have devastating financial or security consequences. How can we find errors in real-world applications? How can we guarantee that such errors don't exist? To even begin to answer these questions we need a specification: a description of what it means for a piece of code to be correct, stated either explicitly (e.g. my private data are never leaked to third parties) or implicitly (e.g. this code will not terminate with an uncaught exception). In this talk, I will discuss efficient ways to debug and reason about software and specifications, focusing on two techniques and their interplay: property-based testing and mechanized formal verification. Testing can quickly uncover errors in complex software, but it cannot guarantee their absence. Formal verification provides strong correctness guarantees, but is still very expensive in time and effort. Together, they are a match made in heaven.

Fully-autonomous cyber-physical systems (CPS) such as autonomous vehicles, drones, and robots today are not engineered as rigorously as aircraft, and thus are not as reliable. In fact, these CPS will likely experience more failures in the future, since they will have a cumulative operation time several orders of magnitude more than that of airplanes. Thus, it is essential that we bring the reliability of today’s commercial aircraft systems (“ultra-reliability”) to the next generation of fully-autonomous CPS. One of the main challenges that needs to be addressed in this regard is ensuring high reliability with minimal cost in the presence of environmental disturbance sources such as electro-magnetic interference and thermal effects. To this end, I will present the first provably safe reliability analysis of Ethernet-based distributed real-time systems in the presence of environmentally-induced Byzantine errors. The analysis helps quantify and systematically evaluate the reliability tradeoffs involved when using different replication schemes. In this talk, I will discuss the key features of our analysis, including how we tackle reliability anomalies and how we quantify a CPS application's inherent robustness to occasional failures, and my plans for future research.

Traditionally, the server-side code of websites was written in languages such as PHP or Java for which security issues are well-studied and well-understood. Recently, though, full-stack JavaScript web applications emerged, which have both their client-side and server-side code written in this language. The benefits of such an approach are obvious, e.g., easy knowledge transfer across tiers and uniform usage of tools. However, JavaScript was designed as a scripting language with a thin API and it was expected to run in a tightly-controlled environment, e.g., a sandbox. Taking JavaScript outside of the browser and using it as a general purpose programming language represents a paradigm shift for the web community and, thus, the npm ecosystem emerged to support this change. Npm is supposedly the largest software repository in the world with more than a million reusable packages. Nevertheless, the lack of code isolation and code vetting, the various ways to abuse the JavaScript language, and the plethora of reported vulnerabilities and malware incidents make npm a dangerous ecosystem with unique challenges for the security community. In this talk, we start by analyzing the attack surface of npm, showing that transitive dependencies and the large number of human agents in the ecosystem represent an important risk. We then continue with showing that vulnerabilities in npm packages affect real-world websites and that a motivated attacker can craft exploits against production websites by analyzing third-party, open-source code. Finally, we present a technique for boosting the recall of existing security analyses on JavaScript code that heavily relies on third-party libraries. More precisely, our approach extracts taint specifications for npm packages by using dynamic analysis and by leveraging test suites available in clients of the target package.

Blockchain technologies have rapidly acquired popularity and promise to become one of the pillars of the digital society. They, however, are not immune from open challenges in terms of security, privacy and scalability. First, the complexity of blockchain applications makes their security analysis prohibitive, which may lead to coin losses by honest users. Second, the fundamental requirement of including every single transaction in the blockchain for transparency is at odds with the privacy of transactions and users. Last, but not least, storing all data in the blockchain creates severe scalability issues: currently, blockchain technologies typically support a dozen transactions per second, which is far from the throughput of other payment systems available today. In this talk, I will present my research on security, privacy and scalability in blockchain technologies. In particular, I will focus our findings on the security and privacy issues with currently deployed scalability solutions such as the Lightning Network that affected to all its users in practice. Moreover, I will overview the cryptographic protocols that we have designed to mitigate the aforementioned issues. They have been implemented and tested for the Lightning Network and other currently deployed solutions. I will finish this talk with an overview of some of the open problems with current blockchain technologies.

High-performance multicores providing strong consistency guarantees speculatively reorder memory operations. If a memory reordering is seen by other cores, speculative operations are squashed and re-executed. This talk presents the concept of non-speculative and invisible reordering of memory operations, the foundation on which the ECHO project (an ERC Consolidator Grant) is based on. The talk offers a background about memory-level speculation in current multicores. Then, it shows that, for the case of the load-load reordering, is not necessary to squash and re-execute reordered loads to guarantee the load-load order. It also presents a case for store-store ordering, which allows for the first time cost-effective store coalescing with strong consistency. Finally, it discusses solutions for secure speculative execution.

Program synthesis is often called the "holy grail" of computer science, as it enables users to refrain from error-prone software development process and focus on only analyzing the intended behavior of the system. Thus, program synthesis exhibits its power in automatic generation of intricate and complex parts of a system as well as in repetitive programming tasks, and bringing the power of programming to the average computer user who may not possess sophisticated programming skills. A particular area where program synthesis can play a central role is in distributed systems due to their inherent complex nature. This talk will present our recent results and breakthroughs in synthesizing parameterized distributed self-stabilizing algorithms.

Recent years have seen a tremendous growth in the interest in secure multiparty computation (MPC) and its applications. While much progress has been made concerning its efficiency, many current, efficient protocols are vulnerable to Denial of Service attacks, where a cheating party may prevent the honest parties from learning the output of the computation, whilst remaining anonymous. The security model of identifiable abort aims to prevent these attacks, by allowing honest parties to agree upon the identity of a cheating party, who can then be excluded in the future. Several existing MPC protocols offer security with identifiable abort against a dishonest majority of corrupted parties. However, all of these protocols have a round complexity that scales linearly with the depth of the circuit, so are unsuitable for use in high latency networks. In this work, we present the first efficient MPC protocols with identifiable abort in the dishonest majority setting, which run in a constant number of rounds and make only black-box use of cryptographic primitives. Our main construction is built from highly efficient primitives in a careful way to achieve identifiability at a low cost. In particular, we avoid the use of public-key operations outside of a setup phase, incurring a relatively low overhead on top of the fastest currently known constant-round MPC protocols based on garbled circuits. In addition, we show how to upgrade our protocol to achieve public verifiability using a public bulletin board, allowing any external party to verify correctness of the computation and identify a cheating party.

In secret sharing a dealer holds a secret and wants to distribute it among several parties in such a way that the individuals do not learn the secret. However, if several of the parties unite their shares they are able to reconstruct the secret. Secret sharing has several applications such as distributed storage and secure multiparty computation. For different applications it is desired to have different properties for the secret sharing scheme used. Such properties can be linearity, low share size compared to the secret size, low reconstruction, and high privacy. In this talk, I will present some bounds connecting some of these properties. These bounds give some restrictions on what we can achieve for secret sharing schemes. The talk is based on results from the paper "Improved Bounds on the Threshold Gap in Ramp Secret Sharing" by Ignacio Cascudo, Jaron Skovsted Gundersen and Diego Ruano, published in IEEE Transactions on Information Theory.

Software is a fundamental pillar of modern scientific research, across all fields and disciplines. However, there is a general lack of adequate means to archive, reference and cite software. In this talk, we will survey the main issues that make this task difficult, ranging from the specificity of the persistent identifiers needed for reproducibility to the complexity of determining software authorship and authority, especially for long running projects, which are needed for proper software attribution and credit. We report on recent contributions to the ongoing efforts to develop proper processes, guidelines and recommendations for software reference and software citation, building upon the internal experience of Inria and the emerging Software Heritage infrastructure.

The Elliptic Curve Digital Signature Algorithm (ECDSA) is a widely adopted digital signature standard; in particular it is employed to validate bitcoin transactions. In this context, the theft of a secret signing key results in an immediate financial loss, thereby creating a single point of failure. An interesting solution to reduce the risk of key theft is that of sharing the secret signing key among various devices, such that a signature can only be produced if these devices collaborate to jointly produce a signature, thereby distributing the signature protocol. In this talk I will focus on the two party case, which allows for instance to share a secret key between a mobile phone and a laptop. Unfortunately, efficient distributed variants of ECDSA are notoriously hard to achieve and prior to our work, solutions required expensive zero knowledge proofs to deal with malicious adversaries (MacKenzie et al. (Crypto’01)), relied on non standard interactive assumptions (Lindell (Crypto’17)) or induced a high communication cost (Doerner et al. (IEEE S&P’18)). I will explain how, in a recent article from Crypto’19 we overcome all of the above drawbacks, and — using class groups of imaginary quadratic fields — provide a provably secure two party ECDSA protocol, relying only on standard assumptions, which is the most efficient to date in terms of bandwidth consumption while remaining competitive in terms of timings. I will further justify that — by resorting to two recently introduced computational assumptions on class groups — we can dramatically improve the efficiency of the zero knowledge proofs needed by our protocol (and thereby that of the overall protocol).

Caches have become the prime method for unintended information extraction across logical isolation boundaries. They are widely available on all major CPU platforms and, as a side-channel, caches provide great resolution, making them the most convenient channel for Spectre and Meltdown. As a consequence, several methods to stop cache attacks by detecting them have been proposed. Detection is strongly aided by the fact that observing cache activity of co-resident processes is not possible without altering the cache state and thereby forcing evictions on the observed processes. In this work, we show that this widely held assumption is incorrect. Through clever usage of the cache replacement policy, it is possible to track cache accesses of a victim's process without forcing evictions on the victim' s data. Hence, online detection mechanisms that rely on these evictions can be circumvented as they would not detect the introduced RELOAD+REFRESH attack. The attack requires a profound understanding of the cache replacement policy. We present a methodology to recover the replacement policy and apply it to the last five generations of Intel processors. We further show empirically that the performance of RELOAD+REFRESH on cryptographic implementations is comparable to that of other widely used cache attacks, while detection methods that rely on L3 cache events are successfully thwarted.