Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series (S3)

Software Seminar Series (S3)

Pedro Valero

Tuesday, February 26, 2019

10:45am Lecture hall 1, level B

Pedro Valero, PhD Student, Instituto IMDEA Software

Complete Abstractions for Checking Language Inclusion

Abstract:

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


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Marco Guarnieri

Tuesday, February 19, 2019

10:45am Lecture hall 1, level B

Marco Guarnieri, Post-doctoral Researcher, Instituto IMDEA Software

Spectector: Principled detection of speculative information flows

Abstract:

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.


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Platon Kotzias

Tuesday, February 12, 2019

10:45am Lecture hall 1, level B

Platon Kotzias, PhD Student, Instituto IMDEA Software

Mind Your Own Business: A Longitudinal Study of Threats and Vulnerabilities in Enterprises

Abstract:

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.


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Miguel Ambrona

Thursday, February 07, 2019

10:45am Lecture hall 1, level B

Miguel Ambrona, PhD Student, Instituto IMDEA Software

Zero-Knowledge Proofs

Abstract:

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.


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Pepe Vila

Tuesday, January 29, 2019

10:45am Lecture hall 1, level B

Pepe Vila, PhD Student, Instituto IMDEA Software

CSS Injection Attacks: or how to leak content with <style>

Abstract:

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.


Time and place:
10:45am Lecture hall 1, level B
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Software Seminar Series (S3) - Otoño 2018