IMDEA initiative

Home > Events > Software Seminar Series (S3)

Software Seminar Series (S3)

Isabel García

Tuesday, June 19, 2018

10:45am Meeting room 302 (Mountain View), level 3

Isabel García, PhD Student, IMDEA Software Institute

Towards Better User Guidance in Abstract Interpretation

Abstract:

Approximations during program analysis are a necessary evil, as they ensure essential properties, such as analysis soundness and termination, but they also imply that the analysis is not guaranteed to always produce useful results. In such cases it is necessary to have some means for users to provide information to guide analysis and thus to improve precision, such as the trust assertions of CiaoPP or the "known facts" of Astrée. This allows dealing with, e.g., predicates for which the analysis is not complete or when the source is only partially available. We present techniques for supporting within an abstract interpretation framework with a rich set of trust assertions (conditional, dealing with call/success pairs and multivariance). We extend the language of program-point assertions to deal with multi-variance. Our techniques can also deal with the cases where run-time checks for assertions are present in the program and those in which no run-time checks are generated. Finally, we show how the approach can be applied to both improving precision and accelerating.


Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Alejandro Aguirre

Tuesday, June 12, 2018

10:45am Lecture hall 1, level B

Alejandro Aguirre, PhD Student, IMDEA Software Institute

Almost Sure Productivity

Abstract:

A program that computes on an infinite data structure, such as an infinite list or tree cannot be expected to terminate. But for it to behave properly, not only it must run forever, it also must compute arbitrarily precise approximations of the result in finite time. This property is known as productivity, and is the dual of termination. Productivity is well-known and has been studied in a deterministic setting. However, extending it to a probabilistic setting poses some formal challenges. In this talk I will introduce a probabilistic extension of productivity , which we name Almost Sure Productivity (ASP). I will first look further into this duality between termination and productivity, which is essentially the duality between algebras and coalgebras, and present the theoretical background that will allow us to formalize the concept of ASP. Then I will define a core language for probabilistic computations on infinite lists and trees, and provide two methods for checking whether a program is ASP: an efficient but incomplete syntactic criterion, and a decision procedure based on model-checking probabilistic pushdown automata.


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

Tuesday, June 05, 2018

10:45am Lecture hall 1, level B

Miguel Ambrona, PhD Student, IMDEA Software Institute

Primality tests: How can we know that a number is prime?

Abstract:

Prime numbers are essential in cryptography. Many cryptographic primitives (RSA encryption, ElGamal, digital signatures...) rely on finding and using large prime numbers (in the range of 256-2048 bits long). But, why are prime numbers important for cryptography? And, how can we check whether such large numbers are prime? In this talk, I will present different techniques to assure primality, such as probabilistic algorithms (that assure with very high probability that the number is prime) and the celebrated AKS algorithm (which is the first known deterministic algorithm for primality checking running in polynomial time). These algorithms are efficient enough to be used in actual cryptographic applications. Additionally, I will talk about the largest prime numbers known by humanity and how we know they are prime (note that the mentioned algorithms cannot be used to assure primality of these staggering numbers and dedicated algorithms must be employed).


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, May 22, 2018

12:00pm Meeting room 302 (Mountain View), level 3

Pepe Vila, PhD Student, IMDEA Software Institute

Theory and Practice of Finding Eviction Sets

Abstract:

Many micro-architectural attacks rely on the capability of an attacker to efficiently find small eviction sets: groups of virtual addresses that map to the same cache set. This capability has become a decisive primitive for cache sidechannel, rowhammer, and speculative execution attacks. Despite their importance, algorithms for finding small eviction sets have not been systematically studied in the literature. In this talk, we perform such a systematic study. We begin by formalizing the problem and analyzing the probability that a set of random virtual addresses is evicting. We then present novel algorithms, based on ideas from threshold group testing, that reduce random eviction sets to their minimal core in linear time, improving over the quadratic state-of-the-art. We complement the theoretical analysis of our algorithms with a rigorous empirical evaluation in which we identify and isolate factors that affect their reliability in practice, such as adaptive replacement strategies and TLB thrashing. Our results indicate that our algorithms enable finding small eviction sets much faster than before, and under conditions where this was previously deemed impractical.


Time and place:
12:00pm Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Software Seminar Series (S3) - Winter 2018