- talks - lists.cs.princeton.edu

Stephen Yi-Hsien Lin MSE thesis talk
by Melissa M. Lawson 11 Apr '14

11 Apr '14

Stephen Yi-Hsien Lin will present his MSE thesis talk on Wednesday April 16 at 3PM in Room 401 (note room!). The members of his committee are: Andrew Appel, advisor and Ed Felten, reader. Everyone is invited to attend his talk. His abstract follows below. --------------------- ROS, a flexible framework for developing robot software, has been widely used to implement many robots. ROS is highly decoupled into different function nodes in order to encourage collaborative development. However, these nodes communicate through non-authenticated messages over an insecure communication channel, which makes the robots highly susceptible to cyber attacks. Adversary might be able to inject malicious commands into the communication channel in order to take control over the robot. Therefore, a secure message authentication mechanism must be introduced to ROS in order to prevent such attack. We developed a message authentication mechanism based on HMAC to address this problem. Our design goal is to not only protect the integrity and authentication of the messages in ROS but also a) bring as few intrusion to the system as possible, b) maintain backward compatibility so the code developed in the past could also benefit from our message authentication package with very little modification and c) make the usage as simple as possible. Besides the message authentication mechanism, we also proposed a key generation and exchange protocol on ROS. Our measurements comparing the throughput and latency before and after introducing message authentication indicated that the performance of the whole system is still reasonable after introducing the message authentication functionality.

1 0

Marcela Melara MSE thesis talk
by Melissa M. Lawson 10 Apr '14

10 Apr '14

Marcela Melara will present her MSE thesis talk on Thursday April 17 at 2PM in Room 402. Her committee is: Ed Felten, advisor and Michael Freedman, reader. Everyone is invited to attend her talk. Her abstract follows below. --------------------------- Abstract: As a foundation for securing Internet communication, today’s public-key infrastructures attempt to certify that the “correct” principal owns a name and possesses a corresponding public key. Yet these assertions are not machine-verifiable, and their correctness can be and has been broken by error, malice, or external (and sometimes legal) coercion. Rather than focus on the “correctness” of name ownership, we argue that ensuring the continuity of that ownership, as defined by the binding of a name to a public key, is necessary and often sufficient for secure communication. To this end, we have designed CONIKS, a key management system that ensures online identity providers maintain and respond with valid bindings from names to cryptographic keys, even without users managing (or seeing) those keys. If providers disseminate invalid bindings or equivocate by presenting different bindings to different users, parties quickly detect this misbehavior and can publish irrefutable proof of this equivocation. The cryptographic mechanisms employed by CONIKS are highly efficient, supporting an Internet environment of millions of providers, any of which may have users in the billions. Our prototype Off-the-Record chat service, ConiksChat, demonstrates that one can achieve high usability while preserving the security and privacy of online communications.

1 0

Colloquium Speaker Dorit Aharonov Thurs April 10, 4:30pm
by Nicole E. Wagenblast 10 Apr '14

10 Apr '14

Quantum computation as a lens on quantum physics Dorit Aharonov ( Hebrew University, Jerusalem, Israel ) Thursday, April 10, 4:30pm Computer Science 105 Quantum computation inspires the study of quantum many body systems from a computational perspective. This approach leads to a remarkably rich set of insights and questions, with deep implications to both physics and quantum computation. This direction, now coined "quantum Hamiltonian complexity", had turned over the past decade into an exciting fast growing field. I will try to give a taste of some of its main achievements, e.g., unexpected hardness of certain physical systems, and testing quantum mechanics using interactive proofs. Dorit Aharonov did a BSc in Physics and Mathematics at the Hebrew university, an MSc in Physics at the Weizmann institute, and a PhD in Computer Science and Physics at the Hebrew university (1999). After a postdoc at IAS Princeton and UC Berkeley she joined the faculty of the CS department at the Hebrew university in 2001. In 2005, Aharonov was profiled in Nature as one of four "young theorists who are making waves in their chosen fields", and in 2006 she received the Krill Prize for Excellence in Scientific Research. In 2011 she was awarded an ERC starting grant from the European Research Council. Her current topics of interest include quantum algorithms and complexity, and the computational view on quantum mechanics and multiparticle entanglement.

1 2

Nick Johnson Pre-FPO
by Melissa M. Lawson 10 Apr '14

10 Apr '14

Nick Johnson will present his preFPO on Thursday April 17 at 9AM in Room 402. The members of his committee are: David August, advisor; David Wentzlaff and Jae Lee (SKKU), readers; David Walker and Andrew Appel, nonreaders. Everyone is invited to attend his talk. His abstract follows below. --------- Title: Static Dependence Analysis in an Infrastructure for Automatic Parallelization. Now that parallel architectures are common, software must exploit parallel functional units to fully utilize hardware resources and achieve efficient execution. Although developers may restructure their applications for explicit parallelism, that process requires developers to reason about low-level details of the execution environment to avoid concurrency bugs and achieve parallel performance. A favorable alternative is automatic thread extraction, since it relieves the developer of the arduous task of (re-)developing applications with each new architecture. This dissertation presents compiler middle-ware to support automatic thread extraction---analyses and transformations that allow the compiler to deliver parallel performance from sequentially-specified input programs. Specifically, this thesis contributes, 1. Collaborative Dependence Analysis: Compilers use static analysis to determine facts about the input code. These facts restrict compiler transformations to ensure correctness. The collaborative dependence analysis framework combines simple analysis algorithms into an ensemble algorithm. Such ensembles are structured for collaboration: the ensemble algorithm disproves dependence queries which no member analysis algorithm disproves alone. Preliminary results demonstrate that this framework has a large impact on even speculative thread extraction systems: for some benchmarks, the strength of analysis is the difference between a 28x speedup and an 11x slowdown (geomean) measured on 50 cores. 2. Scaling Analysis to Parallelize Larger Scopes: As scopes grow large, the burden of analysis becomes prohibitive. Observing that parallelization depends on the strongly-connected components of the PDG (the DAG_SCC), this dissertation presents a faster algorithm to compute the DAG_SCC. This algorithm greedily identifies dependence edges which cannot affect parallelization. It reduces analysis time by skipping such unimportant dependence edges, instead spending analysis effort on the remaining, important queries. Overall, this faster algorithm reduces analysis time by half while maintaining precision. The dissertation presents an end-to-end integration of these contributions. This infrastructure has proved robust and flexible; many works from the Liberty Research Group have built upon this infrastructure.

1 0

Colloquium Speaker: Stefanie Jegelka Tues April 8th 4:30pm
by Nicole E. Wagenblast 07 Apr '14

07 Apr '14

Efficient learning with combinatorial structure Stefanie Jegelka , University of California, Berkeley Tuesday, April 8, 4:30pm Computer Science 105 Learning from complex data such as images, text or biological measurements invariably relies on capturing long-range, latent structure. But the combinatorial structure inherent in real-world data can pose significant computational challenges for modeling, learning and inference. In this talk, I will view these challenges through the lens of submodular set functions. Considered a "discrete analog of convexity", the combinatorial concept of submodularity captures intuitive yet nontrivial dependencies between variables and underlies many widely used concepts in machine learning. Practical use of submodularity, however, requires care. My first example illustrates how to efficiently handle the important class of submodular composite models. The second example combines submodularity and graphs for a new family of combinatorial models that express long-range interactions while still admitting very efficient inference procedures. As a concrete application, our results enable effective realization of combinatorial sparsity priors on real data, significantly improving image segmentation results in settings where state-of-the-art methods fail. Motivated by good empirical results, we provide a detailed theoretical analysis and identify practically relevant properties that affect complexity and approximation quality of submodular optimization and learning problems. Stefanie Jegelka is a postdoctoral researcher at UC Berkeley, working with Michael I. Jordan and Trevor Darrell. She received a Ph.D. in Computer Science from ETH Zurich in 2012, in collaboration with the Max Planck Institute for Intelligent Systems, and completed her studies for a Diploma in Bioinformatics with distinction at the University of Tuebingen (Germany) and the University of Texas at Austin. She was a fellow of the German National Academic Foundation (Studienstiftung) and its scientific college for life sciences, and has received a Google Anita Borg Europe Fellowship and an ICML Best Paper Award. She has also been a research visitor at Georgetown University Medical Center and Microsoft Research and has held workshops and tutorials on submodularity in machine learning.

1 0

Colloquium Speaker Elad Hazan, Thurs April 3, 4:30pm
by Nicole E. Wagenblast 03 Apr '14

03 Apr '14

Sublinear Optimization for Machine Learning Elad Hazan, Technion, Israel Institute of Technology Thursday, April 3, 4:30pm Computer Science 105 In many modern optimization problems, particularly those arising in machine learning, the amount data is too large to apply standard convex optimization methods. We'll discuss new optimization algorithms that make use of randomization to prune the data produce a correct solution albeit running in time which is smaller than the data representation, i.e. sublinear running time. We'll present such sublinear-time algorithms for linear classification, support vector machine training, semi-definite programming and other optimization problems. These new algorithms are based on a primal-dual approach, and use a combination of novel sampling techniques and the randomized implementation of online learning algorithms. We'll describe information-theoretic lower bounds that show our running times to be nearly best possible in the unit-cost RAM model. The talk will be self contained - no prior knowledge in convex optimization or machine learning is assumed. Elad Hazan is an associate professor of operations research at the Technion, Israel Institute of Technology. His main research area is machine learning and its relationship to optimization, game theory and computational complexity. Elad received his Ph.D. in computer science from Princeton University. He is the recipient of several best paper awards including the Goldberg Best Paper award (twice), and the European Research Council starting grant.

1 1

Colloquium Speaker Arti Gupta Weds April 2, 4:30pm
by Nicole E. Wagenblast 02 Apr '14

02 Apr '14

Software Verification: Locks and MLoCs* Arti Gupta ( NEC Labs America ) Wednesday, April 2, 4:30pm Computer Science 105 Software verification deals with proving or falsifying correctness properties of programs, and has broad applications from ensuring safety of mission-critical software to improving program robustness and programmer productivity. This area has long held theoretical interest, but the inherent undecidability of the general problem and intractability of specific formulations have been barriers to practical success. Approaches based on automatic techniques for state space exploration, such as model checking and symbolic execution, have seen a resurgence of interest in recent years, driven largely by advancements in solvers for Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT). These solvers perform the underlying search for proofs or bugs, typically by reasoning over abstract models of programs. While abstraction is critical in scaling to real-life programs, it is equally important to ensure enough precision in the models and the analysis to verify specific properties of interest. In this talk, I will describe my work in foundational techniques that address these twin challenges of precision and scalability in verifying sequential and multi-threaded programs. I will also share the lessons learnt in my efforts in driving them to industry practice where they are routinely used in a modular methodology to find complex bugs in software projects, some with millions of lines of code. Finally, I will discuss future extensions and applications of this verification framework. *MLoC: Million Lines of Code Aarti Gupta received her PhD in Computer Science from Carnegie Mellon University. Her broad research interests are in the areas of formal analysis of programs/systems and automatic decision procedures. At NEC Labs she leads research in systems analysis and verification. She has given several invited keynotes highlighting the foundational research contributions of her group in verification and their successful industrial deployment. She has served as an Associate Editor for Formal Methods in System Design (since 2005) and for the ACM Transactions on Design Automation of Electronic Systems (2008-2012). She has also served as Co-Chair for the International Workshop on Satisfiability Modulo Theories (SMT) 2010, the International Conference on Computed Aided Verification (CAV) 2008, and Formal Methods in Computer Aided Design (FMCAD) 2006. She is currently serving on the Steering Committee of CAV.

1 2

Colloquium Speaker Emina Torlak, Today 4:30pm
by Nicole E. Wagenblast 31 Mar '14

31 Mar '14

Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond Emina Torlak ( University of California, Berkeley ) Monday, March 31, 4:30pm Computer Science 105 We live in a software-driven world. Software helps us communicate and collaborate; create art and music; and make discoveries in biological, physical, and social sciences. Yet the growing demand for new software, to solve new kinds of problems, remains largely unmet. Because programming is still hard, developer productivity is limited, and so is end-users' ability to program on their own. In this talk, I present a new approach to constructing programs, which exploits advances in constraint solving to make programming easier for experts and more accessible to everyone else. The approach is based on two observations. First, much of everyday programming involves the use of domain-specific languages (DSLs) that are embedded, in the form of APIs and interpreters, into modern host languages (for example, JavaScript, Scala or Racket). Second, productivity tools based on constraint solvers (such as verification or synthesis) work best when specialized to a given domain. Rosette is a new kind of host language, designed for easy creation of DSLs that are equipped with solver-based tools. These Solver-Aided DSLs (SDSLs) use Rosette's symbolic virtual machine (SVM) to automate hard programming tasks, including verification, debugging, synthesis, and programming with angelic oracles. The SVM works by compiling SDSL programs to logical constraints understood by SMT solvers, and then translating the solver's output to counterexamples (in the case of verification), traces (in the case of angelic execution), or code snippets (in the case of synthesis and debugging). Rosette has hosted several new SDSLs, including imperative SDSLs for data-parallel and spatial programming; a functional SDSL for specifying executable semantics of secure stack machines; and a declarative SDSL for web scraping by example. Emina Torlak is a researcher at U.C. Berkeley, working at the intersection of software engineering, formal methods, and programming languages. Her focus is on developing tools that help people build better software more easily. She received her B.Sc. (2003), M.Eng. (2004) and Ph.D. (2009) from MIT, where she developed Kodkod, an efficient SAT-based solver for relational logic. Kodkod has since been used in over 70 tools for verification, debugging, and synthesis of code and specifications. Emina has also worked on a wide range of domain-specific formal methods. She won an ACM SIGSOFT distinguished paper award for her work at LogicBlox, where she built a system for synthesizing massive data sets, used in testing of decision support applications. As a member of IBM Research, she led the development of a tool for bounded verification of memory models, enabling the first fully automatic analysis of the Java Memory Model. These experiences inspired her current research on solver-aided languages, which aims to reduce the effort of applying formal methods to new problem domains.

1 0

Colloquium Speaker Keith Winstein Thurs March 27, 4:30pm
by Nicole E. Wagenblast 27 Mar '14

27 Mar '14

Transport Architectures for an Evolving Internet Keith Winstein, Massachusetts Institute of Technology Thursday, March 27, 4:30pm Computer Science 105 The technologies that make up the Internet are changing every year, but some transport protocols continue to act as though the Internet behaved as it did 20 years ago. This can cause poor performance on newer networks -- cellular networks, datacenters -- and makes it more challenging to roll out networking technologies that break markedly with the past. How do we make applications and protocols keep up with an evolving network? I will describe the Sprout algorithm, a transport protocol designed for videoconferencing over cellular networks, that uses probabilistic inference to forecast network congestion in advance. On commercial cellular networks, Sprout gives 2-to-4 times the throughput and 7-to-9 times less delay than Skype, Apple Facetime, and Google+ Hangouts. This work led to Remy, a computer program that generates transport protocols automatically, as a function of a protocol designer's assumptions about the network and statement of an objective function. Remy's computer-generated algorithms can achieve higher performance and greater fairness than some sophisticated human-designed schemes. I will discuss our work on using Remy to probe open questions of Internet congestion control -- what's the cost of maintaining backwards compatibility with existing algorithms, including the Transmission Control Protocol as it exists today ? Is there a tradeoff between a protocol's performance today and its ability to adapt to networks of the future? This talk includes joint work with Anirudh Sivaraman, Pratiksha Thaker, and Hari Balakrishnan. URL: http://mit.edu/keithw Keith Winstein is a doctoral candidate at MIT's Computer Science and Artificial Intelligence Laboratory. His work applies statistical and predictive approaches to teach computers to design better network protocols and applications. He created the Mosh (mobile shell) tool for remote access to Unix-like systems and the Sprout algorithm for cellular networks, which was awarded a 2014 Applied Networking Research Prize. From 2007 to 2010, Keith worked as a staff reporter at The Wall Street Journal, covering science and medicine.

1 1

CJ Bell FPO
by Melissa M. Lawson 25 Mar '14

25 Mar '14

CJ Bell will present his Final Public Oral on Tuesday April 1 at 1:30PM in Room 402. The members of his committee are: David Walker, advisor; Andrew Appel and David August, readers; Ed Felten and Sharad Malik, nonreaders. A copy of his thesis, "A Proof Theory for Loop-Parallelizing Transformations", is on display in Room 310. Everyone is invited to attend his talk.

1 0