IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series (S3)

Software Seminar Series (S3)

Isabel García

Tuesday, March 03, 2020

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

Isabel García, PhD Student, IMDEA Software Institute

Modular verification of C programs

Abstract:

To obtain scalability, software model checkers often employ modular analysis techniques that analyze each of the procedures in a program separately. In this context, summaries are used to abstract the behavior of procedures, as relations of their input/output parameters, to analyze any procedure call without inlining or analyzing its body. One key challenge when producing summaries of memory-manipulating programs is to solve the frame problem: determining which memory locations are not changed by a procedure. In SMT-based model checking, the program heap is usually modeled by logical (unbounded) arrays. A pointer analysis is typically used as a pre-analysis to divide the heap into multiple disjoint regions, such that each region is encoded into an array. In general, a summary contains two arrays (input and output) per memory region, describing all possible values before and after the call to the procedure. A naive SMT encoding requires quantifiers to express which elements of the output array are equal to the input array. Although some SMT solvers can handle formulas with quantifiers, the problem is in general undecidable and, therefore, we want to avoid them if possible. In this talk we will show how to leverage a pointer analysis to produce an SMT encoding that enforces the SMT solver to search only for quantifier-free summaries. First, we use the explicit heap representation that the pointer analysis produces to distinguish between finite and potentially infinite memory regions accessed by a procedure. Second, we introduce a new SMT encoding that replaces array variables with scalars if the procedure only uses a finite amount of memory. This is a joint work with Jorge Navas and Arie Gurfinkel.


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


Avinash Sudhodanan

Tuesday, February 18, 2020

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

Avinash Sudhodanan, Post-doctoral Researcher, IMDEA Software Institute

Cross-Origin State Inference (COSI) Attacks: Leaking Web Site States through XS-Leaks

Abstract:

This talk will be a rehearsal of my Network and Distributed System Security Symposium (NDSS) 2020 paper presentation. I will be presenting our work on Cross-Origin State Inference (COSI) attacks. In a COSI attack, an attacker convinces a victim into visiting an attack web page, which leverages the cross-origin interaction features of the victim's web browser to infer the victim's state at a target web site. Multiple instances of COSI attacks have been found in the past under different names such as login detection or access detection attacks. But, those attacks only consider two states (e.g., logged in or not) and focus on a specific browser leak method (or XS-Leak). This work shows that mounting more complex COSI attacks such as deanonymizing the owner of an account, determining if the victim owns sensitive content, and determining the victim's account type often requires considering more than two states. Furthermore, robust attacks require supporting a variety of browsers since the victim's browser cannot be predicted apriori. To address these issues, we present a novel approach to identify and build complex COSI attacks that differentiate more than two states and support multiple browsers by combining multiple attack vectors, possibly using different XS-Leaks. To enable our approach, we introduce the concept of a COSI attack class. We propose two novel techniques to generalize existing COSI attack instances into COSI attack classes and to discover new COSI attack classes. We systematically apply our techniques to existing attacks, identifying 40 COSI attack classes. As part of this process, we discover a novel XS-Leak based on window.postMessage. We implement our approach into Basta-COSI, a tool to find COSI attacks in a target web site. We apply Basta-COSI to test four stand-alone web applications and 58 popular web sites, finding COSI attacks against each of them.


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


Pedro Valero

Tuesday, February 4, 2020

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

Pedro Valero, PhD Student, IMDEA Software Institute

Lossless Compression of Textual Data

Abstract:

This talk is a combination of what I have learned about grammar-based compression while developing our tool -zearch- for searching on compressed text [1] and what I have learned about LZ77-based compression during my internship at Facebook. We will begin with an introduction to these two paradigms of compression of textual data: Grammar-based and LZ77-based, followed by an explanation of one algorithm from each family: REcursive PAIRing (Grammar) [2] and zstd (LZ77) [3]. After that, we will compare these two classes of algorithms and discuss some of the advantages of each of them with respect to the other. Finally, we will talk about dictionary-enhanced compression as a mechanism for efficiently compressing large amounts of small but similar files. This technique has proven so efficient that has been deployed at large scale within Facebook creating the so called "Managed Compression". [1] https://ieeexplore.ieee.org/document/8712660 [2] https://ieeexplore.ieee.org/abstract/document/755679 [3] https://facebook.github.io/zstd/


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


Pepe Vila

Tuesday, January 28, 2020

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

Pepe Vila, PhD Student, IMDEA Software Institute

CacheQuery: Learning Replacement Policies from Hardware Caches

Abstract:

We show how to infer deterministic cache replacement policies using off-the-shelf automata learning and program synthesis techniques. For this, we construct and chain two abstractions that expose the cache replacement policy of any set in the cache hierarchy as a membership oracle to the learning algorithm, based on timing measurements on a silicon CPU. Our experiments demonstrate an advantage in scope and scalability over prior art and uncover 2 previously undocumented cache replacement policies.


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


Software Seminar Series (S3) - Fall 2019