- talks - lists.cs.princeton.edu

11am talk today on secure provenance in distributed systems in room 402
by Jennifer Rexford 12 Dec '11

12 Dec '11

Speaker: Wenchao Zhou, U. Penn Title: Secure Provenance in Distributed Systems Date/time: 11am-noon Monday December 12 Room: 402 Abstract: Operators of distributed systems often find themselves needing to answer forensic questions, to perform a variety of managerial tasks including fault detection, system debugging, accountability enforcement, and attack analysis. In this talk, we present Secure Provenance, a novel approach that provides the fundamental functionality required for answering such forensic questions -- the capability to "explain'' the existence (or change) of a certain distributed system state at a given time in a potentially adversarial environment. We show that it is both possible and practical to efficiently and scalably maintain and query provenance in a distributed fashion, where provenance maintenance and querying are modeled as recursive continuous queries over distributed relations. We then propose enhancements to the provenance model that allow operators to reliably query provenance information in adversarial environments. Our extensions incorporate tamper-evident properties which provide the guarantee that operators can eventually detect the presence of compromised nodes that lie or falsely implicate correct nodes. Finally, we present ongoing efforts that consider privacy protection of sensitive information in provenance maintenance and querying, and discuss our work in the context of our longer term vision towards provably secure distributed systems.

1 0

11am-noon Mon Dec 12 talk on secure provenance in distributed systems
by Jennifer Rexford 08 Dec '11

08 Dec '11

Speaker: Wenchao Zhou, U. Penn Title: Secure Provenance in Distributed Systems Date/time: 11am-noon Monday December 12 Room: 402 Abstract: Operators of distributed systems often find themselves needing to answer forensic questions, to perform a variety of managerial tasks including fault detection, system debugging, accountability enforcement, and attack analysis. In this talk, we present Secure Provenance, a novel approach that provides the fundamental functionality required for answering such forensic questions -- the capability to "explain'' the existence (or change) of a certain distributed system state at a given time in a potentially adversarial environment. We show that it is both possible and practical to efficiently and scalably maintain and query provenance in a distributed fashion, where provenance maintenance and querying are modeled as recursive continuous queries over distributed relations. We then propose enhancements to the provenance model that allow operators to reliably query provenance information in adversarial environments. Our extensions incorporate tamper-evident properties which provide the guarantee that operators can eventually detect the presence of compromised nodes that lie or falsely implicate correct nodes. Finally, we present ongoing efforts that consider privacy protection of sensitive information in provenance maintenance and querying, and discuss our work in the context of our longer term vision towards provably secure distributed systems.

1 0

Colloquium Speaker Celine Latulipe Mon Dec 5- 4:30pm
by Nicole E. Wagenblast 05 Dec '11

05 Dec '11

Expressive Interaction and the Evaluation of Creativity Support Celine Latulipe, University of North Carolina at Charlotte Monday, December 5, 2011, 4:30pm Computer Science Small Auditorium (Room 105) Visionaries in Computer Science have long seen the computer as a tool to augment our intellect. However, while it is relatively straightforward to measure the impact of a tool or technique on task efficiency for well-defined tasks, it is much more difficult to measure computers' impact on higher-level cognitive processes, such as creativity. In my own research in Human-Computer Interaction, I create novel interaction techniques, but run up against the problem of trying to evaluate how these tools impact higher-level processes such as creativity, expressiveness and exploration. In this talk, I briefly present a variety of interaction techniques that I have developed, and I then describe a new survey metric, the Creativity Support Index (CSI), that we have developed to help researchers and designers evaluate the level of creativity support provided by these types of systems, tools or interfaces. I will then present some current results using EEG and machine learning to classify the creative experience with more specific, temporal granularity. I present this work within the context of my longer term goal to develop a suite of tools that provide both stronger analytical power and a general framework for evaluating computational support for creative activities, engagement and aesthetic experience. Dr. Celine Latulipe has a PhD in Computer Science from the University of Waterloo in Canada. She is an Assistant Professor of Human-Computer Interaction in the Department of Software and Information Systems in the College of Computing and Informatics at UNC Charlotte. Dr. Latulipe has long been fascinated by two-handed interaction in the real world, and the absence of it in the human-computer interface. She has developed numerous individual and collaborative two-handed interaction techniques and these have blossomed into a more general exploration of creative expression. Dr. Latulipe works on projects with choreographers, dancers, artists and theatre producers to better understand creative work in practice and how technology may play a role in supporting and evaluating creative work practices. Currently, Dr. Latulipe is working on many projects, including the NSF CreativeIT-funded Dance.Draw project, which has received national media attention.

1 2

C Wang preFPO
by Melissa M. Lawson 30 Nov '11

30 Nov '11

Chong Wang will present his preFPO on Wednesday November 7 at 1PM in Room 302 (note room!). The members of his committee are: David Blei, advisor; Rob Schapire and Eric Xing (CMU), readers; Christiane Fellbaum and Andrea LaPaugh, readers. Everyone is invited to attend his talk. His abstract follows below. -------------------------- Title: Hierarchical Bayesian modeling: models and inference algorithms Hierarchical Bayesian models have become a popular tool for analyzing large-scale real-world data, such as text and images. Through these models, people can build useful tools for latent structure discovery, browsing and recommendations. In this talk, I will present several recent advances in the area of hierarchical Bayesian modeling, with an emphasis on topic modeling, Bayesian nonparametrics and approximate posterior inference. Specifically, I will talk about a novel model on recommending scientific articles that provides an interpretable latent structure for both users and items in a recommender system and then present an online variational inference algorithm that scales up to millions of articles on a single machine and also does model selection. Finally, I will summarize with some ongoing work.

1 1

Distinguished Colloquium Speaker Scott Shenker Friday Dec 2nd- 4:30pm
by Nicole E. Wagenblast 29 Nov '11

29 Nov '11

The Future of Networking, and the Past of Protocols Scott Shenker, University of California, Berkeley Distinguished Colloquium Series Speaker Friday, December 2, 2011 Computer Science Small Auditorium, Room 105 Inspired by Barbara Liskov's brilliiant Turing Lecture on "The Power of Abstraction", I will discuss the role of abstraction in networking. I will show how searching for the appropriate network control abstractions leads to a new approach for network management called Software-Defined Networking (SDN), which is sometimes mistakenly referred to as "OpenFlow". This talk will not cover any details of SDN or OpenFlow, but will instead try to place these ideas in the context of broader architectural issues. Scott Shenker spent his academic youth studying theoretical physics but soon gave up chaos theory for computer science . Continuing to display a remarkably short attention span, his research over the years has wandered from computer performance modeling and computer networks to game theory and economics. Unable to hold a steady job, he currently splits his time between the U. C. Berkeley Computer Science Department and the International Computer Science Institute.

1 0

Colloquium speaker, Bjarne Stroustrup Wed Nov 30- 4:30pm
by Nicole E. Wagenblast 29 Nov '11

29 Nov '11

C++11 Style Bjarne Stroustrup, Professor, Texas A&M University; Visiting Fellow, Princeton University Wednesday, November 30, 2011, 4:30 PM Computer Science Small Auditorium (Room 105) We know how to write bad code: Litter our programs with casts, macros, pointers, naked new and deletes, and complicated control structures. Alternatively (or in addition), obscure every design decision in a mess of deeply nested abstractions using the latest object-oriented programming and generic programming tricks. For good measure, complicate our algorithms with interesting special cases. Such code is incomprehensible, unmaintainable, usually inefficient, and not uncommon. But how do we write good code? What principles, techniques, and idioms can we exploit to make it easier to produce quality code? I will make an argument for type-rich interfaces, compact data structures, integrated resource management and error handling, and highly-structured algorithmic code. I will illustrate my ideas and motivate my guidelines with a few idiomatic code examples. I will use C++11 freely. Examples include auto, general constant expressions, uniform initialization, type aliases, type safe threading, and user-defined literals. C++ features are only just starting to appear in production compilers, so some of my suggestions have the nature of conjecture. However, developing a “modern style” is essential if we don’t want to maintain newly-written 1970s and 1980s style code in 2020. This presentation reflects my thoughts on what “Modern C++” should mean in the 2010s: a language for programming based on light-weight abstraction with a direct and efficient mapping to hardware, suitable for infrastructure code. Bjarne Stroustrup is the designer and original implementer of C++ and the author of Programming -- Principles and Practice using C++, The C++ Programming Language, The Design and Evolution of C++, and many other publications. His research interests include distributed systems, design, programming techniques, software development tools, and programming languages. He is actively involved in the ANSI/ISO standardization of C++. Dr. Stroustrup is a Distinguished Professor and holder of the College of Engineering Chair in Computer Science at Texas A&M University. He retains a link with AT&T Labs - Research as an AT&T Fellow. He has received numerous honors, including an honorary professorship in the University of Aarhus, Dr. Dobb's Excellence in Programming award, the William Procter Prize for Scientific Achievement from Sigma Xi, the IEEE Computer Society's Computer Entrepreneur Award, and the ACM Grace Murray Hopper award. He is a member of the National Academy of Engineering and an ACM and IEEE Fellow. He received his Cand. Scient. (Mathematics and Computer Science) 1975, University of Aarhus Denmark, and Ph.D. (Computer Science) 1979, Cambridge University, England.

1 1

X Chen preFPO
by Melissa M. Lawson 28 Nov '11

28 Nov '11

Xiaobai Chen will present his preFPO on Tuesday November 29 at 11:40am in Room 302. The members of his committee are: Thomas Funkhouser, advisor; Szymon Rusinkiewicz and Dan Goldman (Adobe), readers; Adam Finkelstein and David Dobkin, nonreaders. Everyone is invited to attend his talk. His abstract follows below. Title: Learning from people about how to analyze 3D meshes Abstract: Increasing amounts of 3D data from computer graphics to geospatial information systems to computational biology keeps pushing the front of shape analysis, from analysis of local geometries, to analysis of global properties, and to shape understanding. This thesis aims to advance shape understanding by learning from people: two problems are studied, one to understand how people decompose meshes into meaningful parts, and the other to investigate mesh salience in the social context. These studies not only have influenced geometry processing tasks like mesh segmentation and salient feature detection, but also have driven the development of new analysis tools: this thesis will introduce symmetry factored embedding and distance as a new method to characterize symmetry correspondences, and MeshMatch as a tool to transfer properties from studied models to unseen models.

1 0

R Dockins preFPO
by Melissa M. Lawson 22 Nov '11

22 Nov '11

Rob Dockins will present his preFPO on Tuesday November 29 at 10AM in Room 402. The members of his committee are: Andrew Appel, advisor; David Walker and Xavier Leroy (INRIA), readers; David August and Mark Braverman, nonreaders. Everyone is invited to attend his talk. His abstract follows below. ---------------------- Title ========== Behavioral Refinement Abstract ======================== What does it mean for a compiler to be correct? This question is of central importance for anyone attempting to prove a compiler correct, or for users of a compiler to understand what they should expect the compiler to do. Surprisingly, no real consensus has emerged as to the best answer to this question. As a result, it can be rather difficult to understand what a particular compiler correctness proof actually proves, and it is especially difficult to understand the relationship between various different compiler verification efforts. In this thesis, I will propose a specific approach to the question of compiler correctness which is simple and easy to understand, but is also capable of expressing the correctness statement for the majority of compiler correctness projects that currently exist. In other words, I will develop a single parametrized theory of correctness which can be instantiated multiple ways to achieve a theory specific to a particular language and compiler. To accomplish this, I borrow the idea of bisimulations from the concurrency calculus community and adjust it somewhat to fulfill our needs. The main strength of bisimulations is that they easily handle nondeterministic computation. Although popular programming languages rarely feature explicitly nondeterministic features, nondeterminism is nonetheless frequently introduced through interaction with the environment and/or via concurrency primitives. Thus, it is important to smoothly handle nondeterminism in our theory of program semantics. However, the bisimulations developed for concurrency calculi lack a feature we will find very important in our compiler correctness setting: they cannot reason about programs which may go wrong, or exhibit undefined behavior. In situations where undefined behavior occurs, the compiler writer wishes to have freedom to replace the undefined behavior with arbitrary behavior. Bisimulations to not allow us to express this sort of transformation. Thus, we develop a notion of program refinement, which weakens the notion of bisimulation just enough to allow the proper handling of undefined behavior. This notion of refinement provides exactly what we need to answer our motivating question: "A correct compiler is one which outputs a program which is a refinement of the input program." I defend the notion of refinement by relating to an axiomatic semantics based on a variant of Hennessy-Milner logic. The formulae of Hennessy-Milner logic allow one to express specifications of the observable behavior of a program. We show that refinement is precisely the same as preserving all observable specifications in the logic. I will also develop a theory of safe programs. Safe programs are those which will never exhibit undefined behavior. We show that for the safe programs, our notion of refinement collapses back into the more traditional notion of bisimulation. In addition, we demonstrate an interesting and unexpected result: program safety is intimately related to the axiom of the excluded middle (EM) in the logic of observable specifications. Safe programs enjoy EM, whereas unsafe programs do not. In this thesis, I will examine three different variations of bisimulation of increasing complexity (strong, branching and environmental), and show how they can all be relaxed into refinements. For each, we will give a logical characterization which will precisely capture the properties preserved by refinement, and for each we will develop the theory of safe programs. I intend to show that environmental refinement provides an excellent theory for reasoning about realistic languages and execution contexts. In particular, I shall argue that it provides just the right abstraction for discussing the correctness of the verified C compiler CompCert.

1 0

Colloquium talk starting now
by Nicole E. Wagenblast 21 Nov '11

21 Nov '11

Automating End-user Programming and Education using Program Synthesis Sumit Gulwani, Microsoft Research Monday, November 21, 2011, 1:30 PM Computer Science Small Auditorium (Room 105) Recent research in program synthesis has made it possible to effectively synthesize small programs in a variety of domains. In this talk, I will describe two useful applications of this technology that have the potential to influence daily lives of billions of people. One application involves automating end-user programming using examples or keywords, which can allow non-programmers to effectively use computational devices such as computers, smartphones (and in the future robots) to perform a variety of repetitive tasks. Another application involves building intelligent tutoring systems that can help teachers and students with a variety of educational activities such as synthesizing problems, hints, solutions in various domains including math, science, and programming. Sumit Gulwani is a senior researcher in the RiSE group at Microsoft Research, Redmond. His primary research interest is in the area of program synthesis with applications to automating end user programming and building intelligent tutoring systems. Sumit obtained his PhD in computer science from UC-Berkeley in 2005, and was awarded the C.V. Ramamoorthy Award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in computer science and engineering from the Indian Institute of Technology (IIT) Kanpur in 2000 and was awarded the President's Gold Medal.

1 0

Colloquium speaker Sumit Gulwani Monday Nov 21- 1:30pm
by Nicole E. Wagenblast 18 Nov '11

18 Nov '11

Automating End-user Programming and Education using Program Synthesis Sumit Gulwani, Microsoft Research Monday, November 21, 2011, 1:30 PM Computer Science Small Auditorium (Room 105) Recent research in program synthesis has made it possible to effectively synthesize small programs in a variety of domains. In this talk, I will describe two useful applications of this technology that have the potential to influence daily lives of billions of people. One application involves automating end-user programming using examples or keywords, which can allow non-programmers to effectively use computational devices such as computers, smartphones (and in the future robots) to perform a variety of repetitive tasks. Another application involves building intelligent tutoring systems that can help teachers and students with a variety of educational activities such as synthesizing problems, hints, solutions in various domains including math, science, and programming. Sumit Gulwani is a senior researcher in the RiSE group at Microsoft Research, Redmond. His primary research interest is in the area of program synthesis with applications to automating end user programming and building intelligent tutoring systems. Sumit obtained his PhD in computer science from UC-Berkeley in 2005, and was awarded the C.V. Ramamoorthy Award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in computer science and engineering from the Indian Institute of Technology (IIT) Kanpur in 2000 and was awarded the President's Gold Medal.

1 1