- talks - lists.cs.princeton.edu

Qinxiang Cao will present his FPO "Separation-Logic-Based Program Verification in Coq" on Wednesday, 8/8/2018 at 9am in CS 302.
by Nicki Gotsis 01 Aug '18

01 Aug '18

Qinxiang Cao will present his FPO "Separation-Logic-Based Program Verification in Coq" on Wednesday, 8/8/2018 at 9am in CS 302. The members of his committee are as follows: Adviser: Andrew Appel; Examiners: Lennart Beringer and Arti Gupta; Readers: Lars Birkedal (Aarhus University) and Zachary Kincaid Everyone is invited to attend his talk. The talk abstract follow below. In our interconnected world, software bugs can seriously compromise our safety and security. To provide adequate safety or protection, security-critical kernels (of large systems) must be functionally correct. To ensure functional correctness of C programs, we can use Hoare logic and its extensions such as separation logic. But such correctness proofs are large and complex enough that we cannot trust them unless they are machine-checked. This dissertation shows how we can construct mechanized proofs of program correctness using separation logic. I answer three questions: How shall we specify our programs? How shall we prove our programs correct w.r.t. their speci cations? How shall we mechanize such correctness proofs? I present practical techniques for separation-logic-based program veri cation and demonstrate them on several examples. I introduce VST-Floyd, a tool for users to build formal C program correctness proofs in Coq using separation logic. VSTFloyd is built based on Veri able C, a proved sound separation logic; I show how to reformulate its rules to make them practical for use in veri cation. Finally, I introduce a unifying semantics in separation logic so that research results of one separation logic can be generalized to all separation logics. Thus the techniques used in VST-Floyd can be used in other separation logics in the future.

1 0

Joshua Wetzel will present his Pre FPO "Structure-aware approaches for deciphering sequence-specific protein-DNA interactions" on August 2, 2018 at 2:30pm in CS 302.
by Nicki Gotsis 30 Jul '18

30 Jul '18

Joshua Wetzel will present his Pre FPO " Structure-aware approaches for deciphering sequence-specific protein-DNA interactions" on August 2, 2018 at 2:30pm in CS 302. The members of his committee are Mona Singh (adviser), Barbara Engelhardt, Olga Troyanskaya, Ben Raphael, and Stanislav Shvartsman (CBE). All are welcome to attend. Title: Structure-aware approaches for deciphering sequence-specific protein-DNA interactions Abstract: Interactions between proteins and specific genomic loci are critical to the proper functioning of all cells. The ability of DNA-binding proteins to distinguish between their target binding sites and other regions of the genome has been demonstrated to be responsible for directing processes as fundamental as development, meiotic recombination, chromatin regulation, and even organization of the genome into a condensed three-dimensional nuclear structure. Highly precise X-ray or NMR co-complex structural studies have provided great insight into biochemical and stereo-chemical principles guiding such interactions; however, such studies are inherently low-throughput and provide us with the binding behavior of a protein with respect to only a single DNA target. Meanwhile, high-throughput experimental methodologies continue to scale, allowing us to examine a protein’s relative binding preferences across enormous libraries of DNA sequences, albeit at lower-resolution and with decreased interpretability of the interactions. Indeed, while we continue to characterize the individual DNA-binding preferences of large quantities of naturally-occurring or synthetic proteins, the fundamental relationship between the amino acid sequence of the protein and its DNA-binding preferences remains largely elusive. In this talk, I will describe three projects that further our understanding of the relationship between amino acid sequence and DNA-binding preferences (specificities): First, I will discuss a combined experimental-computational effort to systematically determine the DNA-binding landscape across an extremely large library of randomized protein variants of the Cys2His2zinc finger (C2H2-ZF) family, the most abundant group of DNA-binding proteins in eukaryotes. From an integrative analysis of the resulting data, I inferred the largest set of specificities to date for C2H2-ZFs, developed a state-of-the-art structurally-inspired method for predicting specificities for C2H2-ZFs based on amino acid sequence alone, and confirmed or discovered various fundamental and complex characteristics of DNA recognition for this protein family. Second, while specificities of proteins within a single family are related to one another via a common underlying structural DNA-binding interface; this fact is routinely ignored when inferring specificities. Accounting for such relationships should allow considerably more robust estimation in the presence of noise or under-sampling: common properties of high throughput data. To address this, I have developed a platform-independent method for joint inference of specificities for related proteins via enforcement of global within-dataset consistency, according to a structural interface model. Among other results, I will demonstrate that enforcing global consistency within a dataset increases agreement of specificities with an external gold standard beyond the level of agreement achieved via either individual inference of specificities or simple enforcement of local consistency. Finally, individual protein-DNA interaction screens do not provide any direct information that maps amino acid residue positions within the protein to particular DNA base positions in the derived specificities. Such mappings are valuable for learning protein-DNA recognition rules from high-throughput data and would provide insight into which binding site positions may be affected by point mutations in the protein. To help close this gap, I have created an unsupervised statistical framework for mapping groups of proteins from a given family, along with their corresponding specificities, onto structural interface models derived from aggregated family-level co-complex data. The framework outputs a multiple-motif alignment across proteins with potentially diverse DNA-binding specificities, along with a specificity prediction model consistent with the alignment. I will demonstrate proof of principle for this approach by showing that the multiple motif alignment produced for a group of mouse homeodomain proteins with diverse binding preferences is consistent with a known (experimentally-determined) alignment for related homeodomain proteins in fruit fly.

1 0

Yuanzhi Li will present his FPO "On the ability of gradient descent to learn neural networks" on Friday, 8/3/2018 at 11am in CS 301
by Nicki Gotsis 30 Jul '18

30 Jul '18

Yuanzhi Li will present his FPO "On the ability of gradient descent to learn neural networks" on Friday, 8/3/2018 at 11am in CS 301. The members of his committee are as follows:Sanjeev Arora (Adviser); Readers: Elad Hazan and Yingyu Liang (University of Wisconsin- Madison); Examiners: Yoram Singer, Matthew Weinberg, Sanjeev Arora All are welcome to attend. A copy of his thesis will be available in CS 310. Abstract is below. Neural networks stand in the center of the recent breakthrough in Machine Leaming. In the past few years, neural networks have found enormous of applications in various areas. However, due to the intrinsic non-convexity in the networks, theoretical understandings of them remain rather limited. The following major questions are largely unsolved: 1. Why can we train a neural network by minimizing a non-convex objective using local search algorithms? 2. Why does the training result generalizes instead of memorizing? On the theory side, the answer to these questions were rather pessimistic: It is known that even training a 2 layer neural network is NP-hard, and modem neural networks have so large capacity that allow them to fit arbitrary labels, so overfitting seems to be unavoidable. However, on the practice side, the answers to these questions are completely different: In practice, gradient descent (and its variants SGD, Momentum, Adagrad, Adam, RMSProp and AdamDelta) are quite effective in minimizing the training loss, moreover, the solutions found by these algorithms also often generalize well, even on neural networks with trillions of parameters. This thesis aims to build new theorems to address these questions in a way that matches the practical observations. We first consider neural networks with "identity mapping' (Resnet). We show that by adding this mapping to the network, the loss function becomes "locally convex" in a neighborhood of the optimal. We then consider neural networks with "quadratic activations". We show that even if we over-parametrize the network arbitrarily, the set of solutions given by gradient descent will remain on a manifold with small intrinsic dimensions, thus they will generalize. Next we consider neural networks with multiple outputs. We show that as long as the inputs and the labels are actually "structured" and the network is trained using gradient descent, the result will still generalize. In the end we extend our result to non-negative matrix factorization. We show that if we initialize the weights using "pure samples", and train it using an analog of gradient descent, then we are able to recover the hidden structures in the data almost optimally.

1 0

Ryan Beckett will present his FPO, "Network Control Plane Verification and Synthesis" on Monday, 7/23/2018 at 2pm, 101 Marx Hall
by Nicki Gotsis 16 Jul '18

16 Jul '18

Ryan Beckett will present his FPO, "Network Control Plane Verification and Synthesis" on Monday, 7/23/2018 at 2pm, 101 Marx Hall. The members of his committee are as follows: Nonreaders: David Walker (adviser), Aarti Gupta, Jennifer Rexford, Nick Feamster, and Ratul Mahajan (Intentionet); Readers: Aarti Gupta and Ratul Mahajan (Intentionet) All are welcome to attend. Please see abstract below. Computer networks have become an integral part of modern infrastructure, and as the world continues to become increasingly interconnected and more devices come online, the importance of networks will only continue to grow. A critical component of networks is a process called routing, whereby the network determines how to move data from point A to point B as changes occur dynamically (e.g., when new devices connect or equipment fails). Routing is traditionally achieved through the manual configuration of one or more distributed protocols that exchange messages about available routes to different destinations. Manual configuration lets a network operator tune various low-level protocol parameters to accommodate the different economic-, performance-, and robustness-related objectives that they may have for the network. Unfortunately, the low-level nature of existing configuration primitives and the scale of modern networks makes it difficult for humans to predict the impact of configuration on all possible runtime behaviors of the network, often resulting in configuration bugs. This dissertation develops two complementary techniques for proactively finding and preventing bugs in configurations. The first technique is verification. Given a collection of router configurations and a high-level specification of what the network should do (e.g., certain devices should be reachable), verification aims to ensure that the configurations implement this high-level specification correctly for all possible network behaviors. To address this problem, we develop a formal model of network routing protocols and show how many common protocols can be translated to logic constraints that existing constraint solvers can solve to find (or prove the absence of) bugs. The second technique is synthesis. Given a high-level specification of what the network should do, synthesis aims to produce a collection of configurations that faithfully implement the specification for all possible dynamic network conditions. We develop a new high-level language for describing end-to-end network behavior and demonstrate an efficient synthesis algorithm that can generate correct configurations. Throughout the development of both techniques, we show the importance of “abstraction” in speeding up each technique by several orders of magnitude.

1 2

Naman Agarwal will present his FPO "Second-Order Optimization Methods for Machine Learning" on Wednesday, 7/18/2018 at 2:00 PM in CS 402
by Nicki Gotsis 10 Jul '18

10 Jul '18

Naman Agarwal will present his FPO "Second-Order Optimization Methods for Machine Learning" on Wednesday, 7/18/2018 at 2:00 PM in CS 402 The members of his committee are as follows: Readers: Yoram Singer and Yuxin Chen; Nonreaders: Elad Hazan (Adviser), Sanjeev Arora and Mark Braverman All are welcome to attend. Please see below for abstract. In recent years first-order stochastic methods have emerged as the state-of-the-art in largescale machine learning optimization. This is primarily due to their efficient per-iteration complexity. Second-order methods, while able to provide faster convergence, are less popular due to the high cost of computing the second-order information. The main problem considered in this thesis is can efficient second-order methods for optimization problems arising in machine learning be developed that improve upon the best known first-order methods. We consider the ERM model of learning and propose linear time second-order algorithms for both convex as well as non-convex settings which improve upon the state-of-the-art first-order algorithms. In the non-convex setting second-order methods are also shown to converge to better quality solutions efficiently. For the convex case the proposed algorithms make use of a novel estimator for the inverse of a matrix and better sampling techniques for stochastic methods derived out of the notion of leverage scores. For the non-convex setting we propose an efficient implementation of the cubic regularization scheme proposed by Nesterov and Polyak. Furthermore we develop second-order methods for achieving approximate local minima on Riemannian manifolds which match the convergence rate of their Euclidean counterparts. Finally we show the limitations of second/higher-order methods by deriving oracle complexity lower bounds for such methods on sufficiently smooth convex functions.

1 0

Arpit Gupta will present his Pre FPO on Thursday, July 12, 2018 at 10am in CS402
by Nicki Gotsis 06 Jul '18

06 Jul '18

Arpit Gupta will present his Pre FPO on Thursday, July 12, 2018 at 10am in CS402. The members of his committee are as follows: Nick Feamster (advisor), Jennifer Rexford (reader), Walter Willinger (reader), Kyle Jamieson (non-reader), Marshini Chetty (non-reader). His abstract follows below. All are welcome to attend. Abstract: The proliferation of Internet-connected devices, services, and applications makes it more critical than ever to make sure that the network they depend on is reliable, performant, and secure. At the same time, their increasing complexity and diversity have made even simple network management tasks, such as debugging performance or detecting attacks, more complicated than ever. Modern network management needs to provide operators with better ways to (1) monitor what is going on in their networks; (2) take real-time preventive or corrective actions based on this information, to improve reliability, performance, and security of the networks and the services that run on them. Achieving these goals given the limited compute and storage resources available on modern network devices is challenging. This talk describes two projects that address the challenges of better information gathering, and more flexible control, respectively. First, I will present SDX, a Software-Defined Internet Exchange Point that allows an operator to apply fine-grained control over specific network paths in a way that interacts harmoniously with the Internet’s routing protocols. Second, I will present Sonata, a streaming network telemetry system that gathers information based directly on the queries that operators write; Sonata exploits the programmability of the network switches to offload expensive operations inline, whenever possible, ensuring that queries can run online, in real-time. In both cases, I will describe: (1) the abstractions that allow operators to express flexible programs for monitoring and control; (2) the algorithms and data structures that make the best use of limited compute and storage resources; and (3) the systems that glue the high-level abstractions to the low-level algorithms.

1 0

Steven Englehardt will present his FPO "Automated discovery of privacy violations on the web" on Friday, 6/29/2018 at 10:00am in CS 402.
by Nicki Gotsis 20 Jun '18

20 Jun '18

Steven Englehardt will present his FPO "Automated discovery of privacy violations on the web" on Friday, 6/29/2018 at 10:00am, 402 Computer Science. All are welcome to attend. The members of his committee are as follows: Examiners: Arvind Narayanan (Adviser), Prateek Mittal (ELE), and Jennifer Rexford; Readers: Ed Felten, Nick Feamster Abstract follows below. Tracking protection provided by browsers is often ine↵ective, while solutions based on voluntary cooperation, such as Do Not Track, haven’t had meaningful adoption. Knowledgeable users may turn to anti-tracking tools for protection, but we find that even these more advanced solutions fail to fully protect against the techniques we study. In this dissertation, we introduce OpenWPM, a platform we developed for flexible and modular web measurement. We’ve used OpenWPM to run large-scale studies leading to the discovery of numerous privacy and security violations across the web and in emails. These discoveries have curtailed the adoption of tracking techniques, and have informed policy debates and browser privacy decisions. In particular, we present novel detection methods and results for persistent tracking techniques, including: device fingerprinting, cookie syncing, and cookie respawning. Our findings include sophisticated fingerprinting techniques never before measured in the wild. We’ve found that nearly every new API is misused by trackers for fingerprinting. The misuse is often invisible to users and publishers alike, and in many cases was not anticipated by API designers. We take a critical look at how the API design process can be changed to prevent such misuse in the future. We also explore the industry of trackers which use PII-derived identifiers to track users across devices, and even into the o✏ine world. To measure these techniques, we develop a novel bait technique, which allows us to spoof the presence of PII on a large number of sites. We show how trackers exfiltrate the spoofed PII through the abuse of browser features. We find that PII collection is not limited to the web—the act of viewing an email also leaks PII to trackers. Overall, about 30% of emails leak the recipient’s email address to one or more third parties. Finally, we study the ability of a passive eavesdropper to leverage tracking cookies for mass surveillance. If two web pages embed the same tracker, then the adversary can link visits to those pages from the same user even if the user’s IP address varies. We find that the adversary can reconstruct 62—73% of a typical user’s browsing history

1 0

Jieming Mao FPO Thursday June 14, 2018 10:00 CS 402
by Barbara A. Mooring 14 Jun '18

14 Jun '18

Jieming Mao will present his FPO on Thursday June 14, 2018 at 10:00 in room CS 402. Committee: Mark Braverman, Adviser - Princeton University Elad Hazan - Princeton University Ran Raz - Princeton University All are welcomed to attend. Title: Algorithms in Strategic or Noisy Environments Abstract: Algorithms are often used to interact with agents. When the input is collected from agents instead of being directly given, designing algorithms becomes more challenging. Two main challenges arise here: (i) agents may lie to maximize their own utility functions and we need to take their incentives into account (ii) the uncertainty in agents' behavior makes the input appear to be noisy. In this thesis, we study these two challenges in several contexts: the multi-armed bandit problem, combinatorial auctions and rank aggregation. Our goal is to understand how these strategic and noisy factors make the problem harder and to design new techniques which make algorithms robust against these factors. In Part I (Chapter 2 and Chapter 3), we study multi-armed bandit algorithms in strategic environments where rewards are decided by actions taken by strategic agents. We show that traditional multi-armed bandit algorithms could fail and we also develop multi-armed bandit algorithms which achieve good performance in strategic envrionments. In Part II (Chapter 4 and Chapter 5), we focus on combinatorial auctions which are a natural testbed for truthful mechanisms. We characterize the power of truthful mechanisms in several settings and make progress in understanding whether truthful mechanisms are as powerful as algorithms. In Part III (Chapter 6, Chapter 7 and Chapter 8), we study the top-k ranking problem. In this problem, even if the agents are perfectly incentivized, their reported comparison results could still be noisy caused by reasons like limit of knowledge and subjective preferences. We design algorithms which aggregate noisy comparisons to output the set of top items. Barbara A. Mooring Interim Graduate Coordinator Computer Science Department Princeton University

1 2

Sivakanth Gopi FPO June 11, 2018 10:00 am CS 402
by Barbara A. Mooring 08 Jun '18

08 Jun '18

Sivakanth Gopi will present his FPO on June 11, 2018 at 10:00 am in room CS 402. All are welcomed to attend. Committee: Zeev Dvir, Adviser - Princeton University Ran Raz - Princeton University Avi Wigderson - Institute for Advanced Study Title: Locality in Coding Theory Abstract: Error correcting codes have been extremely successful in practice to build storage and communication systems which are resilient to noise and corruptions. They also found several theoretical applications in complexity theory, pseudorandomness, probabilistically checkable proofs and cryptography. Each application requires codes with specific properties. One such property desirable in many applications is ‘locality’. Locality refers to the ability to perform operations like decoding/correction/testing in sublinear or sometimes constant time. For example, a constant query locally decodable code (LDC) allows decoding of any message bit in constant time given a corrupted encoding of the message. Much of the work in this thesis is to understand the power and limitations of codes with locality. We show that one can get non-trivial locality and still match the best known rate-distance tradeoffs of traditional error correcting codes (Gilbert- Varshamov bound). We prove several conditional lower bounds on codes with locality and give new directions for constructing such codes by showing an analytic characterization of LDCs. We also explore applications of such codes to additive combinatorics, information privacy and data storage. We show how to use ideas from existing constructions of LDCs to design 2-server private information retrieval schemes where a user can efficiently and privately query a database replicated among two (non-communicating) servers without revealing any information about their query to either server. We also show limits and improved constructions of maximally recoverable local reconstruction codes which are locally correctable codes designed specifically for distributed data storage applications. Barbara A. Mooring Interim Graduate Coordinator Computer Science Department Princeton University

1 1

Amy Tai PreFPO Wednesday, June 6, 2018 1:00 pm CS402
by Barbara A. Mooring 06 Jun '18

06 Jun '18

Amy Tai will present her PreFPO on Wednesday, June 6, 2018 at 1:00 pm in CS 402. Committee: Mike Freedman (advisor) Jen Rexford Kai Li Kyle Jamieson Wyatt Lloyd All are welcomed to attend. Title: Leveraging Distributed Storage Redundancy in Datacenters Abstract: Replication is a widely used primitive in distributed storage systems to achieve properties such as durability and availability. In this talk, I will discuss two projects in which we design and implement two novel properties that replication can achieve. With each property, we also define the set of tradeoffs introduced as well as propose new techniques for exploring these tradeoffs. Our work shows that replication has several more useful properties than previously assumed. First, I will discuss Replex, which harnesses distributed storage redundancy to build distributed secondary indices. Traditionally, storage systems punt on building fully functional distributed secondary indices because they do not have the correct primitive for doing so. We introduce a new replication primitive, a replex, that treats distributed secondary indices as first-class data objects. The tradeoff that results is between steady-state and failure performance, and we explore this tradeoff with a primitive we denote a hybrid replex. Second, I will discuss DIRECT, which is a set of principles for systematically leveraging storage redundancy to fix corruption errors in live production storage systems. Corruption errors are generally treated as device failures in today's storage systems, but we show that by fixing them online, we can extend the lifetime of flash devices by orders of magnitude. The tradeoff that results is between size of failure domain (and hence time to recovery) and ease of implementation. Barbara A. Mooring Interim Graduate Coordinator Computer Science Department Princeton University

1 2