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.

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.

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/

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.