Fuzzing has become a very interesting technique for finding bugs in computer programs. Since a few years back there is always at least one fuzzing paper in each big conference in systems security. In the industry is also a significant component of the software development cycle. In big companies like Google or Facebook fuzzing is used extensively across their products, like Chrome or Hack. In this talk I present the problem of fuzzing targets with complex inputs like compilers and interpreters. I also present the work in progress of an approach for fuzzing interpreters of object oriented scripting languages like JavaScript. In this approach a fuzzer leverages on what is called Object Oriented Genetic Programming for targeting a specific part of the interpreter; the standard library. This libraries are usually implemented in native code for performance and, because of that, are interesting targets for fuzzing. Along with the architecture of the fuzzer I also present the preliminary results of comparing my fuzzer with other fuzzers in the state of the art and the roadmap of the next steps.

Starting from one of the most celebrated undecidable problem in CS, the Halting Problem, and using reductions as a bridge to show that one problem is at least as difficult to solve as other hard problem, I will gradually achieve the goal of this presentation: proving the undecidability of a collection of problems on the theory of context-free languages.

We all love eating pizza, but we don't love so much using a fork and a knife for that. The problem is that the moment we pick up a slice of pizza with our hand, it tends to flop over and dangles from our fingers. Luckily, we have a solution: we just need to fold the slice along the bisection (making the shape of an U), that way the slice of pizza won't bend down. Behind this apparently simple trick lies a remarkable mathematical result about the curvature of surfaces. This result was published in 1827 by Carl Friedrich Gauss and says that curvature is an intrinsic property of a surface, independent of its isometric embedding in Euclidean space. A consequence of this is that a 2-dimensional living being on a surface can measure the curvature of his land by just measuring angles and distances. Gauss found this result so outstanding that he named it by "Theorema Egregium" (latin for "remarkable theorem"). In this talk we'll explain the historial context and the importance of this theorem, as well as show some surprising applications as, for example, its relation with our way of eating pizza. Disclaimer: pizza won't be served during the talk.

We study the language inclusion problem L1 ⊆ L2 where L1 is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L1, obtained by successively overapproximating the Kleene iterates of its least fixpoint characterization, is included in L2. We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e. its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e. it guarantees termination of least fixpoint computations). Such overapproximating abstraction function on languages can be defined using quasiorder relations on words where the abstraction gives the language of all words ``greater than or equal to'' a given input word for that quasiorder. We put forward a range of quasiorders that allow us to systematically design decision procedures for different language inclusion problems such as context-free languages into regular languages and regular languages into trace sets of one-counter nets. We also provide quasiorders for which the induced inclusion checking procedure corresponds to well-known state-of-the-art algorithms like the so-called antichain algorithms. Finally, we provide an equivalent greatest fixpoint language inclusion check which relies on quotients of languages and, to the best of our knowledge, was not previously known

Since the advent of Spectre, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. We present a novel, principled approach for reasoning about software defenses against Spectre-style attacks. Our approach builds on speculative non-interference, the first semantic notion of security against speculative execution attacks. We develop Spectector, an algorithm based on symbolic execution for automatically proving speculative non-interference, or detecting violations. We implement Spectector in a tool, and we use it to detect subtle leaks – and optimizations opportunities – in the way major compilers place Spectre countermeasures.

Enterprises own a significant fraction of the hosts connected to the Internet and possess valuable assets, such as financial data and intellectual property, which may be targeted by attackers. They suffer attacks that exploit unpatched hosts and install malware, resulting in breaches that may cost millions in damages. Despite the scale of this phenomenon, the threat and vulnerability landscape of enterprises remains under-studied. The security posture of enterprises remains unclear, and it's unknown whether enterprises are indeed more secure than consumer hosts. To address these questions, we perform the largest and longest enterprise security study up to date. Our data covers nearly 3 years and is collected from 28K enterprises, belonging to 67 industries, which own 82M hosts and 73M public-facing servers. Our measurements comprise of two parts: an analysis of the threat landscape and an analysis of the enterprise vulnerability patching behavior. The threat landscape analysis first classifies low reputation files observed in enterprise hosts into families. Then, it measures, among others, that 91%--97% of the enterprises, 13%--41% of the enterprise hosts, encountered at least one malware or PUP file over the length of our study; that enterprises encounter malware much more often than PUP; and that some industries like banks and consumer finances are doing notoriously better, achieving significantly lower malware and PUP encounter rates than the most-affected industries. The vulnerability analysis examines the patching of 12 client-side and 112 server-side applications in enterprise hosts and servers. It measures, among others, that it takes over 6 months on average to patch 90% of the population across all vulnerabilities in the 12 client-side applications; that enterprise computers are faster to patch vulnerabilities compared to consumer hosts; and that the patching of server applications is much worse than the patching of client-side applications.

Are you tired of having to reveal the solution to your sudoku in order to convince others that you have solved it? Are you sick of not being believed when you know a secret? Are you embarrassed about your id card picture and having to expose it every time you need to prove your identity? For the third: Sorry... For the former two: Here they come! Zero-Knowledge proof systems! A ZK proof system allows a party (the prover) to convince another party (the verifier) about the validity of certain statement, without revealing any other additional information, e.g., why the statement is valid. ZK proofs play an essential role in many applications such as: authentication systems, cryptographic protocols or blockchains. In this talk, I will present several examples of ZK proofs and I will consider the following two questions: - How can we be sure that no additional information is leaked from a proof? - What does it mean "to know something"? The audience will get an intuition about how the above questions have been formally addressed in cryptography.

In this talk we'll discuss the impact of CSS (or stylesheet) injection attacks on web security. For that, we'll first present some historical notes about CSS injections and related research. Then we'll show and explain two working demos that leak HTML attributes and text nodes using only CSS (no JavaScript) from a vulnerable web page. Finally, we'll show a recursion trick that allows these attacks to work w/o need of iframes or redirections, enabling them in isolated environments like Electron apps.