Nico Rosner

University of California Santa Barbara
Computer Science Department

GPG key           Download CV

About me

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.

Research interests

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:

  • Constraint solving
  • Symbolic execution
  • Model counting
  • Fuzzing and mutation
  • Information theory
  • Distributed systems

For further details take a look at my publications and research projects.

Publications

DBLP     Google Scholar

  • Nicolás Rosner, Ismet Burak Kadron, Lucas Bang, Tevfik Bultan. Profit: Detecting and Quantifying Side Channels in Networked Applications. Network and Distributed System Security Symposium (NDSS 2019).   PDF
  • Ivan Bocić, Tefvik Bultan, Nicolás Rosner. Inductive Verification of Data Model Invariants in Web Applications Using First-Order Logic. Automated Software Engineering (ASE Journal 2018).   DOI   PDF
  • Lucas Bang, Nicolás Rosner, Tevfik Bultan. Online Synthesis of Adaptive Side-Channel Attacks Based On Noisy Observations. IEEE European Symposium on Security and Privacy (Euro S&P 2018).   DOI   PDF
  • Tegan Brennan, Nicolás Rosner, Tevfik Bultan. JIT Leaks: Inducing Timing Side Channels through Just-In-Time Compilation. UCSB Technical Report (2018).   PDF
  • Tegan Brennan, Nestan Tsiskaridze, Nicolás Rosner, Abdulbaki Aydın, Tevfik Bultan. Constraint normalization and parameterized caching for quantitative program analysis. ACM Symposium on Foundations of Software Engineering (FSE 2017).   DOI   PDF
  • Nicolás Rosner, Jaco Geldenhuys, Nazareno Aguirre, Willem Visser, Marcelo Frias. BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support. IEEE Transactions on Software Engineering (TSE Journal 2015).   DOI   PDF
  • Nicolás Rosner, Valeria Bengolea, Pablo Ponzio, Shadi Khalek, Nazareno Aguirre, Marcelo Frias, Sarfraz Khurshid. Bounded Exhaustive Test Input Generation from Hybrid Invariants. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2014).   DOI   PDF
  • Pablo Ponzio, Nicolás Rosner, Nazareno Aguirre, Marcelo Frias. Efficient Tight Field Bounds Computation Based on Shape Predicates. International Symposium on Formal Methods (FM 2014).   DOI   PDF
  • Nicolás Rosner, Junaid Siddiqui, Nazareno Aguirre, Sarfraz Khurshid, Marcelo Frias. Ranger: Parallel Analysis of Alloy Models by Range Partitioning. IEEE/ACM Conference on Automated Software Engineering (ASE 2013).   DOI   PDF
  • J.P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo Frias. TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds. IEEE Transactions on Software Engineering (TSE Journal 2013).   DOI   PDF
  • Nicolás Rosner, J.P. Galeotti, S. Bermudez, G. Marucci, S. PĂ©rez, L. Pizzagalli, L. Zemin, Marcelo Frias. Parallel Bounded Analysis of Code with Rich Invariants by Refinement of Field Bounds. International Symposium on Software Testing and Analysis (ISSTA 2013).   DOI   PDF
  • Nicolás Rosner, Carlos López Pombo, Nazareno Aguirre, Ali Jaoua, Ali Mili, Marcelo Frias. Parallel Verification of Alloy Models by Transcoping. Verified Software: Theories, Tools, and Experiments (VSTTE 2013).   DOI   PDF
  • J.P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo Frias. Analysis of Invariants for Efficient Bounded Verification. International Symposium on Software Testing and Analysis (ISSTA 2010).   DOI   PDF
  • Nicolás Rosner, J.P. Galeotti, Carlos López Pombo, Marcelo Frias. ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models. Abstract State Machines, Alloy, B and Z (ABZ 2010).   DOI   PDF
  • J.P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo Frias. Distributed SAT-based Analysis of Object-Oriented Code. International Symposium on Automatic Program Verification (APV 2009).   PDF

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.

Contact info

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