I'm a postdoctoral researcher in the Verification Lab at UCSB, where I work with Tevfik Bultan and a fantastic group of grad students.
We also participate in the DARPA Space/Time Analysis for Cybersecurity program, teamed up with researchers from CMU SV and Vanderbilt.
I enjoy sailing, rock climbing, photography, playing piano, attending Arts & Lectures concerts, and sending vintage postcards.
I'm originally from Buenos Aires, Argentina.
By the way, actual gauchos don't really look like the UCSB Gaucho.
My main background is in formal methods, automated verification, and testing. In the last few years I've been working on security, with an emphasis on side-channel analysis.
I like a healthy mix of theoretical research and hands-on engineering.
My tools and techniques often involve:
For further details take a look at my publications and research projects.
Profit Side-channel leak detection for networked applications
Profit quantifies side-channel leakage in encrypted network streams. It profiles the application, records the traffic, and searches for features (size of a certain packet, time elapsed between certain events, etcetera) that leak information about a user-specified secret variable. It automatically generates a ranking of leaky features sorted by the amount of information that they leak about the secret variable.
Profit uses multiple-sequence-alignment algorithms from genomics to align captured packet traces. Recurrent patterns in the traces, once aligned, are leveraged as delimiters to identify phases of application behavior, revealing subsequences of packets that may be potentially meaningful and adding them as features. We are now extending Profit with mutation-based input generation and feedback-driven input space search optimization.
Attack synthesis Adaptive side-channel attack synthesis in noisy environments
Our prototype uses symbolic execution to find profiling witnesses and profiles the target system through the network in order to automatically build a noise model. Then, during the online attack synthesis phase, it uses weighted model counting and numeric optimization to automatically synthesize attack inputs that maximize the expected information gain.
Cashew Cache mechanism for model-counting constraint solvers
Cashew acts as a wrapper around a model-counting SMT solver. It normalizes constraints as they come in, caches query results, and avoids unnecessary solver calls. Its constraint equivalence scheme is based on the cardinality of solution sets. In model-counting contexts, this allows for much more aggressive normalization than requiring the exact solution sets to match. We built Cashew as an extension of the Green framework.
ABC Automata-based model counter for string constraints
ABC is a string constraint solver and model counter. It provides solutions to systems of string constraints as deterministic finite automata. Given a concrete bound k on the length of strings, it can compute the number of satisfying solutions for strings of up to k characters. It can also return a symbolic representation of the number of strings of length up to k that satisfy the constraints, i.e., a model-counting function.
BLISS Symbolic execution with improved lazy initialization
Lazy initialization (LI) allows symbolic execution to effectively deal with heap-allocated data structures. BLISS refines the search for valid structures during symbolic execution, further reducing the number of spurious and redundant structures. It exploits TACO bounds based on structure invariants and auxiliary solver queries that prune large parts of the search space. We implemented BLISS as an extension of Symbolic PathFinder.
Ranger Distributed analysis of Alloy models by range partitioning
Given the task of verifying a property over an Alloy model, Ranger splits the underlying constraint satisfaction problem into subproblems of lesser complexity by using ranges of candidate solutions, which partition the space of all candidate solutions. It defines a total ordering among candidate solutions, divides this space of candidates into ranges, and launches independent searches within these ranges' endpoints.
TACO Analysis of Java code involving heap-allocated structures
TACO speeds up automated SAT-based verification of JML-annotated Java code. It is particularly well-suited for code involving complex linked structures. Using class invariants and symmetry breaking, TACO automatically computes tight relational bounds for each field of a class. Once computed, they can speed up verification of class methods by several orders of magnitude. Computation of bounds is performed in parallel.
MUCHO-TACO Distributed TACO analysis by tight bound refinement
TACO's tight relational bounds include leeway for structural freedom, allowing each class field to point to many possible objects. We exploit this as a problem-splitting mechanism. MUCHO-TACO refines tight bounds by removing some degrees of freedom at a time, yielding multiple subproblems that can be analyzed in parallel.
DynAlloy An extension of Alloy with actions
DynAlloy is an extension to the Alloy specification language to describe dynamic properties of systems using actions. The DynAlloy tool translates DynAlloy models and properties to Alloy, thus offering the same push-button automated analysis capability as the Alloy Analyzer.
Department of Computer Science
University of California Santa Barbara
Santa Barbara, CA 93106
Office: 2162 Harold Frank Hall
Email: rosner /at/ cs.ucsb.edu
Phone: (805) 724-9174
