- talks - lists.cs.princeton.edu

Zoe Paraskevopoulou will present her pre-FPO "An Verified Optimizing Backend for a Purely Functional Language" on January 14, 2020 in CS 402 at 10am
by Nicki Mahler 06 Jan '20

06 Jan '20

Zoe Paraskevopoulou will present her pre-FPO "An Verified Optimizing Backend for a Purely Functional Language" on January 14, 2020 in CS 402 at 10am. The members of her committee are: Andrew Appel (adviser), David Walker (reader), Amal Ahmed (Northeastern University), Aarti Gupta (non-reader), Zachary Kincaid (non-reader) Everyone is invited to attend her talk. The talk title and abstract follow below. An Verified Optimizing Backend for a Purely Functional Language --------------------------------------------------------------------------------------------------------- CertiCoq is a verified compiler for the source language of the interactive theorem prover Coq. The goal of CertiCoq is to bridge the gap between a certified source program and the compiled executable program. Coq's source language, Gallina, is a pure functional language without side effects. To allow programs to interact with their environment despite the lack of side effects, CertiCoq compiles Gallina to C, where the program can be linked with C code that handles the input and the output. In my thesis, I focus on the design, the implementation, and the verification of the optimizing backend of CertiCoq, that is responsible to efficiently compile untyped higher-order functional code to a first-order representation ready to be complied to C. The design of the CertiCoq backend follows a micropass compiler architecture that consists of small compiler passes each of them performing a simple task, and optimizations in the final code rely on the interaction of these transformations. To prove the set of backend transformations correct, I developed a proof framework based on step-indexed logical relations, a powerful proof technique that is used to show program equivalence. The modular and compositional nature of logical relations greatly fits the architecture of our compiler, allowing for proof reuse and compositional reasoning. Despite their mathematical elegance, logical relations cannot generally be used to show correctness of separate compilation in multi-pass compilers. I show how our existing proof framework can be extended to provide guarantees not only about whole-program compilation, but also about the correctness of the interaction of programs that are compiled separately through CertiCoq, perhaps using different backend optimizations. This is the first time that logical relations are used to obtain a proof of correctness for separate compilation. In the second part of my thesis, I show how to strengthen the guarantees that the proof framework provides, but from a different angle. Bugs in compilers manifest themselves not only in the final result of the computation, what we usually call functional correctness of the transformation, but also in other observable behaviours of the program, such as resource consumption. In order to ensure that a transformation will not introduce timing and memory leaks, I extended the logical relation framework so that it supports reasoning about preservation of running time and space. I used this extended proof framework to prove that the closure conversion algorithm of CertiCoq is not only correct with respect to the final result, but also safe for space. Furthermore, I also show that the garbage collection strategy followed by CertiCoq is safe with respect to the idealistic space consumption model. This is the first formal proof of space-safety for a closure conversion algorithm and a particular garbage collection strategy and also the first time that logical relations were used to reason about space safety.

1 0

Yixin Sun will present her FPO "Enhancing Anonymity Systems under Network and User Dynamics" on Tuesday, December 17, 2019 at 9:30am in CS 402.
by Nicki Mahler 09 Dec '19

09 Dec '19

Yixin Sun will present her FPO "Enhancing Anonymity Systems under Network and User Dynamics" on Tuesday, December 17, 2019 at 9:30am in CS 402. The members of her committee are as follows: Advisers: Mung Chiang and Prateek Mittal; Readers: Jennifer Rexford, Prateek Mittal, and Nick Feamster; Nonreaders: Jennifer Rexford, Ed Felten, and Mung Chiang. A copy of her thesis is available upon request. Please email ngotsis(a)cs.princeton if you would like a copy of the thesis. Everyone is invited to attend her talk. The talk title and abstract follow below. Privacy on the Internet is eroding rapidly. Anonymity systems have been designed to protect the identity and privacy of users from untrusted destinations and third parties on the Internet. However, many prior works on anonymity systems assume that important system components, such as network routing and user location, are static. In practice, these components are highly dynamic, leading to new vulnerabilities that can compromise user anonymity. In this dissertation, we exploit dynamics in anonymity systems across two different layers: network dynamics (i.e., changes in routing) at the network layer and user dynamics (i.e., changes in user location) at the application layer. First, we present RAPTOR attacks that exploit the dynamics in Internet routing to compromise user anonymity in the Tor network. The attacks enable adversaries to observe more user traffic and deanonymize them more effectively than previously thought. We successfully demonstrate the attacks by performing them on the live Tor network, ethically. Second, we build proactive and reactive defenses to protect Tor users from RAPTOR attacks: (1) a novel Tor relay selection algorithm that proactively reduces the probability of Tor users being affected by an attack, and (2) a monitoring system with novel detection analytics that detect routing anomaly for Tor relays in real time. Finally, we present attacks that exploit user mobility to compromise user anonymity across a wide range of anonymity systems. While prior works assume that user locations are fixed when accessing anonymity systems, we demonstrate that users can be highly mobile and subsequently expose themselves to adversaries as they visit more locations. In summary, we demonstrate the dangers of abstracting dynamics in Internet routing and user location from the analysis of anonymity systems, and take the step to design anonymity systems with these important system components in mind.

1 0

Colloquium Speaker Subhash Khot TODAY at 12:30pm
by Emily C. Lawrence 09 Dec '19

09 Dec '19

Distinguished CS Colloquium Speaker Subhash Khot, New York University Monday, December 9 - 12:30pm Computer Science - Room 105 Host: Ran Raz [ https://www.cs.princeton.edu/events/25898 | https://www.cs.princeton.edu/events/25898 ] Hardness of Approximation: From the PCP Theorem to the 2-to-2 Games Theorem Computer scientists firmly believe that no algorithm can efficiently compute optimal solutions to a class of problems called NP-hard problems. For many NP-hard problems, even computing an approximately optimal solution remains NP-hard. This phenomenon, known as the hardness of approximation, has numerous connections to proof checking, optimization, combinatorics , discrete Fourier analysis, and geometry. The talk will provide an overview of these connections. It will address why graph coloring is a computationally hard problem, how it is possible to check a proof without even looking at it, why computer scientists love the majority vote, and whether a shape exists that looks spherical as well as cubical. It will explain how all this fits into a 30-year research program starting with the foundational Probabilistically Checkable Proofs (PCP) Theorem and leading to the recent 2-to-2 Games Theorem. Bio: Subhash Khot is a professor of computer science at the Courant Institute of Mathematical Sciences at New York University. His prior affiliations include Princeton University (PhD), Institute for Advanced Study (member), Georgia Tech (assistant professor) and University of Chicago (visiting professor). His research centers on computational complexity and its connections to geometry and analysis. He is a recipient of the National Science Foundation’s Alan T. Waterman Award, the International Mathematical Union’s Nevanlinna Prize, the Simons Investigator Award, a MacArthur Fellowship, and is a Fellow of the Royal Society.

1 0

Reminder: Colloquium Speaker Subhash Khot, Monday Dec 9
by Emily C. Lawrence 06 Dec '19

06 Dec '19

Distinguished CS Colloquium Speaker Subhash Khot, New York University Monday, December 9 - 12:30pm Computer Science - Room 105 Host: Ran Raz [ https://www.cs.princeton.edu/events/25898 | https://www.cs.princeton.edu/events/25898 ] Hardness of Approximation: From the PCP Theorem to the 2-to-2 Games Theorem Computer scientists firmly believe that no algorithm can efficiently compute optimal solutions to a class of problems called NP-hard problems. For many NP-hard problems, even computing an approximately optimal solution remains NP-hard. This phenomenon, known as the hardness of approximation, has numerous connections to proof checking, optimization, combinatorics , discrete Fourier analysis, and geometry. The talk will provide an overview of these connections. It will address why graph coloring is a computationally hard problem, how it is possible to check a proof without even looking at it, why computer scientists love the majority vote, and whether a shape exists that looks spherical as well as cubical. It will explain how all this fits into a 30-year research program starting with the foundational Probabilistically Checkable Proofs (PCP) Theorem and leading to the recent 2-to-2 Games Theorem. Bio: Subhash Khot is a professor of computer science at the Courant Institute of Mathematical Sciences at New York University. His prior affiliations include Princeton University (PhD), Institute for Advanced Study (member), Georgia Tech (assistant professor) and University of Chicago (visiting professor). His research centers on computational complexity and its connections to geometry and analysis. He is a recipient of the National Science Foundation’s Alan T. Waterman Award, the International Mathematical Union’s Nevanlinna Prize, the Simons Investigator Award, a MacArthur Fellowship, and is a Fellow of the Royal Society.

1 0

Colloquium Speaker Tom Kwiatkowski TODAY at 1:30pm
by Emily C. Lawrence 03 Dec '19

03 Dec '19

CS Colloquium Speaker Tom Kwiatkowski, Google Tuesday, December 3 - 1:30PM Computer Science - Room 104 Host: Karthik Narasimhan [ https://www.cs.princeton.edu/events/25905 | https://www.cs.princeton.edu/events/25905 ] New Challenges in Question Answering: Natural Questions and Going Beyond Word Matching Abstract: Recently, learned deep models have surpassed human performance on a number of question answering benchmarks such as SQuAD . However, these models resort to simple word matching and answer typing heuristics, and they are easily fooled. In this talk, I will present two different lines of work that aim to take us beyond the current status quo in question answering, and push us towards more robust representations of semantics, pragmatics, and knowledge. First, I will present Natural Questions (NQ), a new question answering benchmark from Google. NQ contains real user questions, which require an understanding of the questioner's intent. NQ also requires systems to read entire Wikipedia pages to decide whether they fully answer a question. This is much harder than finding an answer given the knowledge that one is present. I will convince you that the question 'when was the last time a hurricane hit Massachusetts?' is under-specified with many reasonable answers, and I will tell you how we developed robust evaluation metrics to deal with this ambiguity. In the second part of the talk I will present a complementary method of challenging today's question answering systems by removing access to evidence documents at inference time. Instead of building joint representations of questions and documents, we perform ahead of inference time reading and retrieve answers via fast maximum inner product search. I will show that this leads to large gains in accuracy and speed when finding answers in very large corpora. I will also show some preliminary results that show how our methods can be used to aggregate information from multiple diverse documents.

1 0

Noah Apthorpe will present his Pre FPO "Network Privacy and User Protection in the Internet of Things" on Wednesday, December 4, 2019 at 10:30am in CS 402
by Nicki Mahler 02 Dec '19

02 Dec '19

Noah Apthorpe will present his Pre FPO, "Network Privacy and User Protection in the Internet of Things" on Wednesday, December 4, 2019 at 10:30am in CS 402. The members of his committee are as follows: Nick Feamster (adviser), Examiners: Ed Felten and Arvind Narayanan; Readers: Jennifer Rexford and Marshini Chetty Everyone is invited to attend his talk. The talk abstract follows below. In this talk, I will present my research combining networks, human-computer interaction, and machine learning to study privacy repercussions of Internet of things (IoT) devices and associated online services. This interdisciplinary approach has provided a unique perspective for measuring privacy issues at scale, protecting users from privacy vulnerabilities, and understanding how privacy norms interact with data collection and regulation. First, I will demonstrate that passive network observers can easily infer private in-home user activities from IoT network traffic metadata. This is possible because most user interactions with home IoT devices cause noticeable changes in network traffic rates that are detectable with thresholds or machine learning methods. The limited functionality of these devices makes it easy to associate these traffic rate changes with specific user activities. Fixed distribution traffic shaping can efficiently protect IoT devices that tolerate long network latencies or that have relatively constant traffic rates, but devices with more complicated network activity require more sophisticated protections. I will discuss a zero-latency traffic shaping algorithm, “Stochastic Traffic Padding,” that mimics user activity patterns, provides probabilistic limits on adversary inference accuracy, and allows for tuning of privacy protection versus bandwidth overhead. Next, I will present a survey instrument based on the theory of contextual integrity that allows researchers to measure individual and societal privacy norms at scale. My collaborators and I first applied this survey method to discover home IoT privacy norms of 1,731 U.S. adults, providing recommendations for IoT device manufacturers, regulators, and consumer advocates. We then surveyed 195 U.S. parents, showing that data handling requirements from the Children’s Online Privacy Protection Act (COPPA) generally align with parents’ privacy expectations for IoT toys. However, observed variations in the perceived acceptability of data collection across specific toys, information types, and other conditions emphasize the importance of detailed contextual factors to privacy norms and suggest potential improvements to COPPA. I will conclude with a summary of my ongoing research and a timeline for the completion of my degree.

1 0

Reminder: Colloquium Speaker Tom Kwiatkowski, tomorrow at 1:30pm
by Emily C. Lawrence 02 Dec '19

02 Dec '19

CS Colloquium Speaker Tom Kwiatkowski, Google Tuesday, December 3 - 1:30PM Computer Science - Room 104 Host: Karthik Narasimhan [ https://www.cs.princeton.edu/events/25905 | https://www.cs.princeton.edu/events/25905 ] New Challenges in Question Answering: Natural Questions and Going Beyond Word Matching Abstract: Recently, learned deep models have surpassed human performance on a number of question answering benchmarks such as SQuAD . However, these models resort to simple word matching and answer typing heuristics, and they are easily fooled. In this talk, I will present two different lines of work that aim to take us beyond the current status quo in question answering, and push us towards more robust representations of semantics, pragmatics, and knowledge. First, I will present Natural Questions (NQ), a new question answering benchmark from Google. NQ contains real user questions, which require an understanding of the questioner's intent. NQ also requires systems to read entire Wikipedia pages to decide whether they fully answer a question. This is much harder than finding an answer given the knowledge that one is present. I will convince you that the question 'when was the last time a hurricane hit Massachusetts?' is under-specified with many reasonable answers, and I will tell you how we developed robust evaluation metrics to deal with this ambiguity. In the second part of the talk I will present a complementary method of challenging today's question answering systems by removing access to evidence documents at inference time. Instead of building joint representations of questions and documents, we perform ahead of inference time reading and retrieve answers via fast maximum inner product search. I will show that this leads to large gains in accuracy and speed when finding answers in very large corpora. I will also show some preliminary results that show how our methods can be used to aggregate information from multiple diverse documents.

1 0

Laura Roberts will present her Pre FPO "Prevention and Detection of Internet Surveillance" on Tuesday, December 3, 2019 at 2:30pm in CS 402
by Nicki Mahler 27 Nov '19

27 Nov '19

Laura Roberts will present her Pre FPO on Tuesday, December 3, 2019 at 2:30pm in CS 402. The members of her committee are as follows: Ed Felten (adviser); Readers: Prateek Mittal and Jonathan Mayer; Examiners: Jennifer Rexford and Arvind Narayanan Everyone is invited to attend her talk. The talk title and abstract follow below. Title: Prevention and Detection of Internet Surveillance If you believe that privacy is important in a free and democratic society, then you are surely worried about the enormous surveillance system that is the Internet. In this talk, I present practical ways to prevent being watched while using the Internet by plugging holes in Tor and a practical way to watch who’s watching you. First, we investigate the effect of DNS on Tor’s anonymity. Previous work had not analyzed DNS’s role in deanonymizing Tor users. We discovered that DNS exposes Tor users’ behavior to more adversaries than previously thought, we discovered that Google gets to learn a lot about what websites Tor users are visiting via DNS, we performed simulations at Internet-scale in order to understand how our proof-of-concept attacks could affect real people, and finally, we provided recommendations to Tor operators on how they should be handling DNS in Tor. Next, we analyzed millions of RSA keys in Tor relays in search of anomalies. Previous work has shown how weak cryptographic keys can compromise users’ safety by allowing adversaries to compute the all-important private key. We indeed found anomalous keys and demonstrated that they were indicative of suspicious behavior. Our results led to The Tor Project’s taking action to develop tools that catch these anomalous keys. Finally, Internet users and providers of services don't know who's watching their Internet traffic. We desire a way to detect who is monitoring Internet traffic and to determine where that traffic might be monitored. Thus, we present NOISE, the Nonce Observatory for Inverse Surveillance of Eavesdroppers, a method and system to detect eavesdroppers remotely that involves disseminating nonces--unique, pseudorandom values--in traffic and seeing if they are observed elsewhere, indicating they must have been "eavesdropped" and acted upon unexpectedly. We take advantage of IPv6's large address space and embed 64-bit nonces innocuously into IPv6 addresses. We disseminate these "nonced" addresses via Internet-wide, traceroute-like active measurement campaigns to approx. 15.2M targets as unique source addresses in each outbound probe. We monitor for subsequent interest in these nonces via packet capture on our system's infrastructure and inspection of system logs, email, and a third-party passive DNS database. Disseminating ~1.2 billion nonces, we detect eavesdropping more than 200k times, involving 268 networks, for probes destined for 437 networks. These observations reveal: (a) data collection for security incident handling, (b) traffic information being shared with third parties, and (c) man-in-the-middle monitoring in one of the world's largest commercial peering exchanges.

1 0

Colloquium Speaker Tom Kwiatkowski, Tues. Dec 3
by Emily C. Lawrence 27 Nov '19

27 Nov '19

CS Colloquium Speaker Tom Kwiatkowski, Google Tuesday, December 3 - 1:30PM Computer Science - Room 104 Host: Karthik Narasimhan [ https://www.cs.princeton.edu/events/25905 | https://www.cs.princeton.edu/events/25905 ] New Challenges in Question Answering: Natural Questions and Going Beyond Word Matching Abstract: Recently, learned deep models have surpassed human performance on a number of question answering benchmarks such as SQuAD . However, these models resort to simple word matching and answer typing heuristics, and they are easily fooled. In this talk, I will present two different lines of work that aim to take us beyond the current status quo in question answering, and push us towards more robust representations of semantics, pragmatics, and knowledge. First, I will present Natural Questions (NQ), a new question answering benchmark from Google. NQ contains real user questions, which require an understanding of the questioner's intent. NQ also requires systems to read entire Wikipedia pages to decide whether they fully answer a question. This is much harder than finding an answer given the knowledge that one is present. I will convince you that the question 'when was the last time a hurricane hit Massachusetts?' is under-specified with many reasonable answers, and I will tell you how we developed robust evaluation metrics to deal with this ambiguity. In the second part of the talk I will present a complementary method of challenging today's question answering systems by removing access to evidence documents at inference time. Instead of building joint representations of questions and documents, we perform ahead of inference time reading and retrieve answers via fast maximum inner product search. I will show that this leads to large gains in accuracy and speed when finding answers in very large corpora. I will also show some preliminary results that show how our methods can be used to aggregate information from multiple diverse documents.

1 0

Colloquium Speaker Jason Weston TODAY at 1:30pm
by Emily C. Lawrence 26 Nov '19

26 Nov '19

CS Colloquium Speaker Jason Weston, Facebook Tuesday, November 26 - 1:30PM Computer Science - Room 104 Host: Danqi Chen [ https://www.cs.princeton.edu/events/25903 | https://www.cs.princeton.edu/events/25903 ] Putting together the threads of conversational AI Maybe we don't have enough threads yet to knit together the whole, but let's try anyway! We present our view of what is necessary for conversational AI, and the pieces we have worked on so far to get there. In particular: software ( ParlAI , a unified platform for dialogue research), various neural architectures for memory, reasoning, retrieval and generation, and interactive learning, tasks for employing personality (Persona-Chat), knowledge (Wizard of Wikipedia) and perception (Image-Chat), evaluation studies & techniques (Acute- Eval ), and a recent competition (ConvAI2). We'll try not to be too pessimistic (!), but we'll also discuss how far we still have to go. Bio: Jason Weston is a research scientist at Facebook, NY and a Visiting Research Professor at NYU. He earned his PhD in machine learning at Royal Holloway, University of London and at AT&T Research in Red Bank, NJ (advisors: Alex Gammerman , Volodya Vovk and Vladimir Vapnik ) in 2000. From 2000 to 2001, he was a researcher at Biowulf technologies. From 2002 to 2003 he was a research scientist at the Max Planck Institute for Biological Cybernetics, Tuebingen , Germany. From 2003 to 2009 he was a research staff member at NEC Labs America, Princeton. From 2009 to 2014 he was a research scientist at Google, NY. His interests lie in statistical machine learning, with a focus on reasoning, memory, perception, interaction and communication. Jason has published over 100 papers, including best paper awards at ICML and ECML, and a Test of Time Award for his work "A Unified Architecture for Natural Language Processing: Deep Neural Networks with Multitask Learning", ICML 2008 (with Ronan Collobert ). He was part of the YouTube team that won a National Academy of Television Arts & Sciences Emmy Award for Technology and Engineering for Personalized Recommendation Engines for Video Discovery. He was listed as the 16th most influential machine learning scholar at AMiner and one of the top 50 authors in Computer Science in Science.

1 0