October 2016 - talks - lists.cs.princeton.edu

Jordan Fix will present his Pre-FPO on Monday, November 7th, 2016 at 4pm in CS 401
by Nicki Gotsis 07 Nov '16

07 Nov '16

Jordan Fix will present his Pre-FPO on Monday, November 7th, 2016 at 4pm in CS 401. The members of his committee are: Advisor: David August Non-readers: David Wentzlaff, Margaret Martonosi Readers: Andrew Appel, David Callahan (Facebook) Everyone is invited to attend his talk. Abstract: Speculation with transactional memory (TM) systems helps programmers and compilers produce profitable thread-level parallel programs. Prior work shows that supporting transactions that span multiple threads, rather than requiring transactions be contained within a single thread, enables new types of speculative parallelization techniques for both programmers and parallelizing compilers. The only prior TM systems with this multithreaded transactional (MTX) support are software-based TM (STM) systems. Unfortunately, these systems are notorious for their high overheads when validating speculative memory operations, which often make otherwise good parallelization unprofitable. Thus, parallelized programs using these prior STM systems with MTX support were forced to overcome this problem through significant manual effort by the programmer to optimize away most of this speculation validation. Unfortunately, compiler technology and static analyses have not proven strong enough to relieve the programmer of this burden. This thesis presents the first complete design and implementation of a hardware TM (HTM) system with MTX support. This system provides low overhead speculation validation, enabling the aforementioned new types of speculative parallelization techniques to achieve good performance even with high amounts of speculation validation. Profitable parallelization of complex programs can be achieved even with maximal speculation validation of every load and store inside transactions of tens to hundreds of millions of instructions, thus making parallelization less laborious and more feasible for both programmers and compilers. In addition to supporting MTXs, transactions in this system are more resilient than in many other prior works. Transactions avoid false misspeculation due to branch misprediction; provide for large read and write sets that commit in a lazy fashion; and allow for context switches (and thread migration) due to common operations such as preemption or virtual memory management. This allows the system to accommodate the large and long running transactions that are needed to parallelize complex programs. Across 6 SPEC benchmarks a geomean speedup of 2.11X over sequential execution is achieved on a multicore machine with 4 cores, while increasing energy usage by 10%.

1 1

Rajesh Ranganath will present his Pre-FPO on Monday, October 31, 2016 at 11:15am in CS 401.
by Nicki Gotsis 28 Oct '16

28 Oct '16

Rajesh Ranganath will present his Pre-FPO on Monday, October 31, 2016 at 11:15am in CS 401. The members of his committee are as follows: David Blei (adviser), Sanjeev Arora, Barbara Englehardt, and Peter Orbanz (Columbia Univ.) Title and Abstract follow below. Title: Black Box Variational Inference and Deep Generative Models Abstract: To model data we desire to express assumptions, infer hidden structure, make predictions, and simulate new data. Probabilistic generative models provide a common toolkit to meet these challenges. In this talk, I will discuss deep exponential families (DEFs). DEFs are a class of latent variable models built from exponential families inspired by the hidden structure used in deep neural networks. We show results on text, and we show how to compose DEFs to build a model for pairwise recommendations. Key to working with probabilistic generative models is computing the posterior: a typically tedious task. In the second half of the talk, I will present black box variational inference, a method to approximate the posterior with minimal model-specific analysis. This family of generic inference algorithms makes approximating the posterior of deep exponential families and other models possible.

1 0

Colloquium Speaker Jonathan Mayer, today, 12:30pm CONVOCATION ROOM
by Nicole E. Wagenblast 25 Oct '16

25 Oct '16

Colloquium Speaker Dr. Jonathan Mayer, Stanford University Tuesday, October 25, 2016 - 12:30pm Friend Center Convocation Room Constitutional Malware The United States government hacks computer systems, for law enforcement purposes. As encryption becomes more pervasive, and as anonymization tools become easier to use, the government will foreseeably increase its resort to malware. This article provides a comprehensive examination of how federal law regulates law enforcement hacking. The article's first contribution is descriptive. It explains why and how law enforcement agencies hack computer systems, and it offers a framework for examining critical steps in the operation of government malware. The article's next contributions are doctrinal, analyzing the appropriate legal procedures for law enforcement hacking. About half of courts have, surprisingly, concluded that government malware does not necessarily implicate constitutional privacy protections. The article argues that law enforcement hacking constitutes a Fourth Amendment "search," and presumptively requires a warrant and associated protections. The article also makes theoretical contributions. Government malware is the latest flashpoint for electronic surveillance, and it illuminates longstanding scholarly debates about the Fourth Amendment. Law enforcement hacking is a case study in how the three branches of government articulate surveillance regulation, the inherent challenges of rebalancing privacy law to account for new technology, and the relationship between statutory and constitutional privacy protections. Jonathan Mayer is Chief Technologist of the Federal Communications Commission Enforcement Bureau, where he works to protect the security and privacy of America's telecommunications infrastructure. Jonathan is also a Cybersecurity Fellow at Stanford University, where he is completing a Ph.D. in computer science and received a J.D. in 2013.

1 0

Colloquium Speaker- Ruslan Salakhutdinov, today, 12:30pm
by Nicole E. Wagenblast 21 Oct '16

21 Oct '16

Colloquium Speaker Ruslan Salakhutdinov, Carnegie Mellon University Friday, October 21, 2016 - 12:30pm Computer Science 105 Learning Multimodal Deep Models Building intelligent systems that are capable of extracting meaningful representations from high-dimensional data lies at the core of solving many Artificial Intelligence tasks, including visual object recognition, information retrieval, speech perception, and language understanding. In this talk I will first introduce a broad class of deep learning models and show that they can learn useful hierarchical representations from large volumes of high-dimensional data with applications in information retrieval, object recognition, and speech perception. I will next introduce deep models that are capable of extracting a unified representation that fuses together multiple data modalities as well as present the Reverse Annealed Importance Sampling Estimator (RAISE) for evaluating these deep generative models. Finally, I will discuss models that can generate natural language descriptions (captions) of images, as well as generate images from captions using attention mechanism. I will show that on several tasks, including modelling images and text, these models significantly improve upon many of the existing techniques. Ruslan Salakhutdinov received his PhD in computer science from the University of Toronto in 2009. After spending two post-doctoral years at the Massachusetts Institute of Technology Artificial Intelligence Lab, he joined the University of Toronto as an Assistant Professor in the Departments of Statistics and Computer Science. In 2016 he joined the Machine Learning Department at Carnegie Mellon University as an Associate Professor. Ruslan's primary interests lie in deep learning, machine learning, and large-scale optimization. He is an action editor of the Journal of Machine Learning Research and served on the senior programme committee of several learning conferences including NIPS and ICML. He is an Alfred P. Sloan Research Fellow, Microsoft Research Faculty Fellow, Canada Research Chair in Statistical Machine Learning, a recipient of the Early Researcher Award, Google Faculty Award, Nvidia's Pioneers of AI award, and is a Senior Fellow of the Canadian Institute for Advanced Research.

1 0

ACM/IEEE Computer Graphics Film Show - October 20, 2016
by Nicole E. Wagenblast 20 Oct '16

20 Oct '16

The Princeton ACM / IEEE-CS chapters kick off our season of meetings with the annual computer graphics film show, featuring the latest and greatest computer animations direct from the ACM SIGGRAPH conference held this summer. These films were selected for the juried Computer Animation Festival at the conference, to demonstrate advancements in graphics research, highlight creative visual effects, educate with scientific visualizations, and show the many uses of real-time game rendering engines. These graphics were created by large organizations and individuals, professional animators and students, on high-end supercomputers and ordinary personal computers. Come and enjoy our most popular meeting of each year! As in the past few years, we will be co-celebrating Martin Gardner's 102nd birthday by hosting a Celebration of Mind party (see http://www.g4g-com.org) as part of our meeting. Gardner (1914-2010) was the editor of the Mathematical Games column of Scientific American from 1956-1981. Plan to arrive at 7:30pm for refreshments and a special guest speaker, with the graphics video show starting around 8:15pm. All Princeton ACM / IEEE-CS meetings are open to the public. Students and their parents are welcome. There is no admission charge, and refreshments are served. Date: Thursday, October 20, 2016, 8:15 pm (Refreshments, networking, and G4G at 7:30 pm) Place: Friend Center Auditorium, Room 101, Princeton University, Olden & William Streets On-line info: http://PrincetonACM.acm.org

1 0

Sergiy Popovych will present his general exam on Monday, October 24, 3:30pm in CS 301.
by Nicki Gotsis 20 Oct '16

20 Oct '16

Sergiy Popovych will present his general exam on Monday, October 24, 3:30pm in CS 301. The members of his committee are David August (adviser), Nick Feamster, and Arvind Narayanan. His abstract and reading list are below. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. __________________________________ As has been demonstrated time and again, almost all systems can be compromised. Connecting to an external network through a unidirectional gateway physically disallows any outgoing traffic, and thus prevents data theft. Existing unidirectional gateways act as stateless links, only supporting inherently unidirectional applications. In an attempt to support applications that require request/response behavior (e.g. web browsing), Starlight adds a second, bidirectionally connected machine not entrusted with sensitive information, which improves usability. However, with Starlight an attacker can observe user actions on the external machine, which enables him to learn information about the enterprise, as well as mount attacks targeting the user (e.g. phishing) . This work proposes Moonshine, a system that uses content prefetching in order to prevent user-caused leakage, and presents usability and security evaluation of this approach. Books: * Ross J. Anderson. 2008. Security Engineering: A Guide to Building Dependable Distributed Systems (2 ed.). Wiley Publishing. (Chapters 1, 3, 6, 8, 13, 21) * Asaf Shabtai, Yuval Elovici, Lior Rokach. 2012. A Survey of Data Leakage Detection and Prevention Solutions. Springer US. Papers: * R. T. Barker and C. J. Cheese. "The application of data diodes for securely connecting nuclear power plant safety systems to the corporate IT network". System Safety, incorporating the Cyber Security Conference, 7th IET International Conference on, Edinburgh, 2012. * B. S. Jeon and J. C. Na. "A study of cyber security policy in industrial control system using data diodes", 18th International Conference on Advanced Communication Technology (ICACT), Pyeongchang, 2016. * Eric Byres. The air gap: SCADA's enduring security myth. Communications, 2013. * Arthur Gervais, Reza Shokri, Adish Singla, Srdjan Capkun, and Vincent Lenders. "Quantifying Web-Search Privacy". In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security , 2014. * M. Anderson, C. North, J. Griffin, R. Milner, J. Yesberg and K. Yiu. "Starlight: Interactive Link". Computer Security Applications Conference, 12th Annual, San Diego, CA, 1996. * Shuo Chen, Rui Wang, XiaoFeng Wang, and Kehuan Zhang. "Side-Channel Leaks in Web Applications: A Reality Today, a Challenge Tomorrow". In Proceedings of the 2010 IEEE Symposium on Security and Privacy, 2010. * Bracha Shapira, Yuval Elovici, Adlay Meshiach, and Tsvi Kuflik. "PRAW - A PRivAcy model for the Web" Research Articles. J. Am. Soc. Inf. Sci. Technol, 2005. * Panagiotis Papadopoulos, Antonis Papadogiannakis, Michalis Polychronakis, Apostolis Zarras, Thorsten Holz, and Evangelos P. Markatos. "k-subscription: privacy-preserving microblogging browsing through obfuscation". In Proceedings of the 29th Annual Computer Security Applications Conference, 2013.

1 1

Reminder: Colloquium Speaker- Ruslan Salakhutdinov, Fri Oct 21, 12:30pm
by Nicole E. Wagenblast 20 Oct '16

20 Oct '16

Colloquium Speaker Ruslan Salakhutdinov, Carnegie Mellon University Friday, October 21, 2016 - 12:30pm Computer Science 105 Learning Multimodal Deep Models Building intelligent systems that are capable of extracting meaningful representations from high-dimensional data lies at the core of solving many Artificial Intelligence tasks, including visual object recognition, information retrieval, speech perception, and language understanding. In this talk I will first introduce a broad class of deep learning models and show that they can learn useful hierarchical representations from large volumes of high-dimensional data with applications in information retrieval, object recognition, and speech perception. I will next introduce deep models that are capable of extracting a unified representation that fuses together multiple data modalities as well as present the Reverse Annealed Importance Sampling Estimator (RAISE) for evaluating these deep generative models. Finally, I will discuss models that can generate natural language descriptions (captions) of images, as well as generate images from captions using attention mechanism. I will show that on several tasks, including modelling images and text, these models significantly improve upon many of the existing techniques. Ruslan Salakhutdinov received his PhD in computer science from the University of Toronto in 2009. After spending two post-doctoral years at the Massachusetts Institute of Technology Artificial Intelligence Lab, he joined the University of Toronto as an Assistant Professor in the Departments of Statistics and Computer Science. In 2016 he joined the Machine Learning Department at Carnegie Mellon University as an Associate Professor. Ruslan's primary interests lie in deep learning, machine learning, and large-scale optimization. He is an action editor of the Journal of Machine Learning Research and served on the senior programme committee of several learning conferences including NIPS and ICML. He is an Alfred P. Sloan Research Fellow, Microsoft Research Faculty Fellow, Canada Research Chair in Statistical Machine Learning, a recipient of the Early Researcher Award, Google Faculty Award, Nvidia's Pioneers of AI award, and is a Senior Fellow of the Canadian Institute for Advanced Research.

1 0

Christopher Beck will present his FPO, "Time and Space in Proof Complexity" on Wednesday, 10/26/2016 at 4:30pm in CS 401.
by Nicki Gotsis 19 Oct '16

19 Oct '16

Christopher Beck will present his FPO, "Time and Space in Proof Complexity" on Wednesday, 10/26/2016 at 4:30pm in CS 401. The members of his committee are: Sanjeev Arora (Adviser), Readers: Bernard Chazelle and Russell Impagliazzo (UCSD); Nonreaders: Mark Braverman and Zeev Dvir. A copy of his thesis is available in Room 310. Everyone is invited to attend his talk. The talk abstract follow below: In this thesis we explore the limitations of efficient computation by way of the complexity of proofs. One of the goals of theoretical computer science is to understand algorithms broadly – to identify meta-algorithms that may be useful in a variety of cases, understand how they work, when they work well, and when they don’t. For several important groups of algorithms, there is a relatively simple mathematical proof that the algorithm is correct for every input. Moreover, when the algorithm is run on any particular input, this proof specializes to produce a very simple combinatorial proof of the correct answer for that input. A simple example is a linear program, which may find an optimal point and give a dual solution proving the optimality, or a graph search algorithm which may fail to find a path between two points and yield a cut separating them instead. Often times, self-contained proofs that the answer to some query is yes or no are just as important as the answer itself. When the algorithm is meant to identify problems in some system, or opportunities, the proof may actually represent actionable information in some domain. A good example is when a SAT solver is used to validate a system that is being designed. When the validation fails, the proof indicates where the problem is with the current design. Proof complexity attempts to place limits on how efficient such algorithms can be by showing that these proofs must sometimes be very complex, growing rapidly as the problem scales up. More broadly, proof complexity attempts to understand the proving power of traditional formal systems for logic, and to corroborate hypotheses like P != NP. We develop novel combinatorial techniques for studying proof complexity in several wellstudied proof systems. We give substantial quantitative improvements on existing results, and also, develop a new method that allows us to study the time and space needed for a proof simultaneously and prove “tradeoff” lower bounds. We show that small reductions in space can sometimes lead to large increases in time, even in situations where the algorithm has large amounts of space to work with. Previously no such results were known in that situation.

1 0

Colloquium Speaker: Dan Boneh, Today, 4:30pm
by Nicole E. Wagenblast 19 Oct '16

19 Oct '16

Colloquium Speaker Prof. Dan Boneh, Stanford University Wednesday, October 19, 4:30pm Computer Science 105 Hiding the metadata in chat systems The talk will survey a number of open problems in computer security, and discuss recent progress on communication systems that hide the metadata. We will present a recent system, called Riposte, that uses cryptographic techniques to provide anonymous Tweets for very large anonymity sets. This is joint work with Henry Corrigan-Gibbs and David Mazieres. Dr. Boneh is a Professor of Computer Science at Stanford University where he heads the applied cryptography group and co-directs the computer security lab. Dr. Boneh's research focuses on applications of cryptography to computer security. His work includes cryptosystems with novel properties, security for mobile devices, web security, and cryptanalysis. He is the author of over a 150 publications in the field and is a recipient of the 2014 ACM Infosys award, the 2013 Godel prize, and the Ishii award for education.

1 0

Zoe Paraskevopoulou will present her general exam on Monday, October 24, 2016 at 9:30am in CS 402.
by Nicki Gotsis 18 Oct '16

18 Oct '16

Zoe Paraskevopoulou will present her general exam on Monday, October 24, 2016 at 9:30am in CS 402. The members of her committee are Andrew Appel (adviser), David Walker, and Zachary Kincaid. Everyone is invited to attend her talk, and those faculty wishing to remain for the oral exam following are welcome to do so. Abstract and reading list are below: Formal Verification of Closure Conversion CertiCoq is a formally verified compiler for dependently typed functional languages that aims to bridge the gap between certified high-level programs and their translation to a low-level machine language. In this talk I will describe the process of implementing and proving correct, using machine checked proofs, the closure conversion phase of CertiCoq. The main transformation is preceded by a lambda lifting phase, that can be seen as an unboxing optimization for closure environments, and followed by a hoisting transformation, which flattens the structure of function definitions. As opposed to previous closure conversion implementations, our implementation decouples the lambda lifting phase from the closure conversion phase, allowing us to achieve a more modular design which is more amenable to formal verification. I will explain the implementation of the three phases as well as the proof techniques that were used to prove their correctness. Finally, I will focus on the challenges involved in the composition of the correctness proofs of the three phases. Reading List —————— * Closure conversion ** Zhong Shao and Andrew Appel, "Efficient and safe-for-space closure conversion" ** Amal Ahmed and Matthias Blume, "Typed Closure Conversion Preserves Observational Equivalence" ** Yasuhiko Minamide et al., "Typed Closure Conversion” ** Morrisett et al., "From System F to Typed Assembly Language" * Compiler correctness ** Nick Benton and Chung-Kil Hur, "Biorthogonality, Step-Indexing and Compiler Correctness" ** Yong Kiam Tan et al., "A New Verified Compiler Backend for CakeML" (This is the new CakeML paper appearing in ICFP 2016) ** Georg Neis et al., "Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language" * Extending Coq with effects ** Aleksandar Nanevski e al., "Ynot : Reasoning with the Awkward Squad" * Parametricity and Relational Reasoning ** John Reynolds, "Types, Abstraction and Parametric Polymorphism" ** Philip Wadler, "Theorems for free!" ** Andrew Appel and David McAllester, "An Indexed Model of Recursive Types for Foundational Proof-Carrying Code" * Books ** The Formal Semantics of Programming Languages, Glynn Winskel ** Types and Programming Languages, Benjamin C. Pierce

1 2