Iniciativa IMDEA

Inicio > Eventos > - Software Seminars Anteriores

Software Seminar Series (S3) - Invierno 2018

Alejandro Aguirre

Tuesday, April 10, 2018

10:45am Meeting room 202 (Hill View), level 2

Alejandro Aguirre, PhD Student, Instituto IMDEA Software

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus

Abstract:

We extend the simply-typed guarded λ-calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic computations. This provides a framework for programming and reasoning about infinite stochastic processes like Markov chains. We demonstrate the logic sound by interpreting its judgements in the topos of trees and by using probabilistic couplings for the semantics of relational assertions over distributions on discrete types. The program logic is designed to support syntax-directed proofs in the style of relational refinement types, but retains the expressiveness of higher-order logic extended with discrete distributions, and the ability to reason relationally about expressions that have different types or syntactic structure. In addition, our proof system leverages a well-known theorem from the coupling literature to justify better proof rules for relational reasoning about probabilistic expressions. We illustrate these benefits with a broad range of examples that were beyond the scope of previous systems, including shift couplings and lump couplings between random walks.


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


Elena Gutierrez

Tuesday, April 03, 2018

10:45am Meeting room 202 (Hill View), level 2

Elena Gutierrez, PhD Student, Instituto IMDEA Software

Weighted Context-free Grammars: Does Parikh's Theorem still hold?

Abstract:

The celebrated Parikh's Theorem states that every context-free language is equivalent to a regular language when we ignore the ordering of symbols in the words. In this work I study under which conditions we can extend this result to the more general scenario where grammar rules are augmented with a weight and thus, each word in the language carries the weight it "costs" to generate it. An extension of the result to the weighted setting has the potential to enable a richer analysis of certain systems. For instance, one can reason about event-driven programs with asynchronous methods where each event has an associated energy cost and answer questions such as, what is the minimal energy budget to serve a given sequence of events?


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


Pablo Cañones

Tuesday, February 27, 2018

10:45am Lecture hall 1, level B

Pablo Cañones, PhD Student, Instituto IMDEA Software

On the Incomparability of Cache Algorithms in Terms of Security

Abstract:

Modern computer architectures rely on caches to reduce the latency gap between the CPU and main memory. While indispensable for performance, caches pose a serious threat to security because they leak information about memory access patterns of programs via execution time. In this talk, I present a novel approach we have developed for reasoning about the security of cache algorithms with respect to timing leaks. The basis of our approach is the notion of leak competitiveness, which compares the leakage of two cache algorithms on every possible program. Based on this notion, we prove the following two results: First, we show that leak competitiveness is symmetric in the cache algorithms. This implies that no cache algorithm dominates another in terms of leakage via execution time. This is in contrast to performance, where it is well known that such dominance relationships exist. Second, when restricted to caches with finite control, the leak-competitiveness relationship between two cache algorithms is either asymptotically linear or constant. No other shapes are possible.


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


Artem Khyzha

Tuesday, February 20, 2018

10:45am Lecture hall 1, level B

Artem Khyzha, PhD Student, Instituto IMDEA Software

Safe Privatization in Transactional Memory

Abstract:

Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often would like to access the same data both inside and outside transactions, e.g., to improve performance or to support legacy code. In this case, programmers would ideally like the TM to guarantee strong atomicity, where transactions can be viewed as executing atomically also with respect to non-transactional accesses. Since guaranteeing strong atomicity for arbitrary programs is prohibitively expensive, researchers have suggested guaranteeing it only for certain data-race free (DRF) programs, particularly those that follow the privatization idiom: from some point on, threads agree that a given object can be accessed non-transactionally. Supporting privatization safely in a TM is nontrivial, because this often requires correctly inserting transactional fences, which wait until all active transactions complete. In this talk, I will present a notion of DRF that takes into account transactional fences and show that it allows the programmer to safely use the privatization idiom. In particular, I will argue that a program indeed has strongly atomic semantics, when a TM satisfies a certain condition generalizing opacity and the program using it is DRF assuming strong atomicity.


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


Joseph Izraelevitz

Thursday, February 08, 2018

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

Joseph Izraelevitz, Post-doctoral Researcher, Instituto IMDEA Software

Theory and Practice for Programming on Nonvolatile Memory

Abstract:

It is expected that nonvolatile, byte-addressable memory (NVM) will soon be commonplace. However, registers and caches are expected to remain transient. In the event of a power failure, NVM content will be preserved, but data stored in the cache and processor will be lost. Since main memory is customarily seen through the filter of current cache contents, data must be carefully managed in NVM to ensure consistency in the wake of a crash. In this work, we introduce a new memory persistency model, explicit epoch persistency, that builds upon and generalizes prior work. Our model captures both hardware buffering and fully relaxed consistency, and subsumes both existing and proposed instruction set architectures. Using the persistency model, we present an automated transform to convert any linearizable, nonblocking concurrent object into one that is also correct for nonvolatile memory. While this transform is correct, it is not necessarily performant. To reduce this overhead, we developed a new design paradigm that we call periodic persistence. In a periodically persistent data structure, updates are made "in place," but can safely leak back to memory in any order, because only those updates that are known to be valid will be heeded during recovery. To guarantee forward progress, we periodically force a write-back of all dirty data in the cache, ensuring that all "sufficiently old" updates have indeed become persistent, at which point they become semantically visible to the recovery process. Experiments with a prototype implementation suggest that periodic persistence can offer substantially better performance than either file-based or incrementally persistent (per-access write-back) alternatives.


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


Avinash Sudhodanan

Tuesday, January 23, 2018

10:45am Lecture hall 1, level B

Avinash Sudhodanan, Post-doctoral Researcher, Instituto IMDEA Software

Analysis and Detection of Authentication Cross-Site Request Forgeries

Abstract:

Cross-Site Request Forgery (CSRF) attacks are one of the critical threats to web applications. In a CSRF attack, an attacker forces the victim's web browser to send HTTP requests which benefits the attacker (and/or harms the victim) in some way. In this talk I will be focusing on CSRF attacks targeting web sites' authentication and identity management functionalities (also known as Authentication CSRF). The possible impacts of Authentication CSRF attacks include account hijack, personal information theft and cross-site scripting. I will present different variants of Authentication CSRF attacks, detection strategies and the available countermeasures. I will also discuss the findings of the experiments conducted by my former colleagues and myself on the Alexa top 1500 web sites. For instance, out of the 265 web sites we tested, 70% of them were vulnerable (including the web sites of Microsoft, Google, eBay, Instagram etc.). We also responsibly disclosed our findings to the affected vendors and received bounties and/or honorable mentions.


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


Pedro Valero

Tuesday, January 16, 2018

10:45am Lecture hall 1, level B

Pedro Valero, PhD Student, Instituto IMDEA Software

Zearch: Regular Expression Matching on Compressed Text

Abstract:

Facebook, Google, Amazon and many other large companies produce huge amounts of data that they need to store and process. From the need for storing the generated information surges the development of compression algorithms such as brotli and zstd. Similarly, the need for processing the stored data results in the development of regular expression (regex) engines such as Hyperscan or RE2 since regex matching is a key operation for handling text files. To this day very efficient solutions have been found these two problems by considering them independently. However, when facing the need to search with a regular expression in a compressed file, the state of the art approach goes through decompressing it and, in parallel, searching on the original text as it is recovered by the decompresser. ZEARCH challenges this standard practice by searching directly on the compressed file while being competitive with the state of the art technologies, even though the current implementation is purely sequential.


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 2017