FMCAD 2013

Tutorials

The Tutorial is jointly organized by FMCAD and MEMOCODE. It will take place on October 20, 2013.

Speaker	Talk Title
Rajeev Alur	Syntax-Guided Synthesis
Jim Grundy	Firmware Validation: Challenges and Opportunities
Somesh Jha, Tom Reps, and Bill Harris	Secure Programs via Game-based Synthesis
Nate Foster, Arjun Guha, Mark Reitblatt, Cole Schlesinger	Network Programming in Frenetic

See the program for the complete FMCAD'13 schedule.

Speaker: [Top]

Rajeev Alur (Professor, University of Pennsylvania)

Title:

Syntax-Guided Synthesis

Abstract:

The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. Our goal is to identify the core computational problem common to these proposals in a logical framework. The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. We describe three different instantiations of the counter-example-guided-inductive-synthesis (CEGIS) strategy for solving the synthesis problem, report on prototype implementations, and present experimental results on an initial set of benchmarks.

Joint work with Ras Bodik, Garvit Juniwal, Milo Martin, Mukund Raghothman, Sanjit Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhsihek Udupa.

Bio:

Rajeev Alur is Zisman Family Professor of Computer and Information Science at University of Pennsylvania. He obtained his bachelor’s degree in computer science from Indian Institute of Technology at Kanpur in 1987, and PhD in computer science from Stanford University in 1991. Before joining Penn in 1997, he was with Computing Science Research Center in Bell Laboratories. His areas of research include formal modeling and analysis of reactive systems, hybrid systems, model checking, software verification, logics and automata, and design automation for embedded software. His awards include IEEE Logic in Computer Science (LICS) Test-of-Time award (2010), the inaugural CAV (Computer-Aided Verification) award (2008), ACM Fellow (2007), IEEE Fellow (2007), designation as a highly cited scientist by the Institute for Scientific Information (2005), Alfred P. Sloan Faculty Fellowship (1999), National Science Foundation’s CAREER award (1997), and President of India’s Gold Medal for academic excellence (1987). Prof. Alur has (co)chaired scientific meetings such as CAV (Intl Conf on Computer-Aided Verification), EMSOFT (ACM Symp on Embedded Software), HSCC (Intl Conf on Hybrid Systems: Computation and Control), and LICS (IEEE Symp on Logic in Computer Science). He has served as the chair of ACM SIGBED (Special Interest Group on Embedded Systems), and as the general chair of IEEE LICS, and is currently the lead PI on NSF Expeditions in Computing center ExCAPE (Expeditions in Computer Augmented Program Engineering).

Speaker: [Top]

Jim Grundy (Research Scientist, Intel Corporation)

Title:

Firmware Validation: Challenges and Opportunities

Abstract:

Firmware validation is driven by imperatives and challenges distinct from those of application level software. In this tutorial we will survey the characteristics of firmware projects, focusing on those that make them particularly challenging and important to validate. We’ll look at the tasks accomplished using firmware, the environments in which it executes, and how firmware is shaped by the constraints imposed by the greater product development program in which it fits. Finally, we’ll look at some of our experiences in firmware validation and the lessons we’ve learned from them. Specifically, we’ll be looking for lessons that can help to guide the selection of problems to study and appropriate case studies on which to evaluate them.

Bio:

Jim Grundy is a research scientist with the Strategic CAD Labs at Intel Corporation, where he leads the Logic Verification group in developing formal tools and methods for modeling and analysis of designs to be realized in both hardware and software. He has published in the fields of automated and interactive reasoning, software verification, and functional programming. Prior to joining Intel in 2000, Jim was faculty a member of the Department of Computer Science at The Australian National University. Jim has also worked as a post-doctoral researcher at Åbo Akademi in Finland, and as a research scientist at the Australian Defence Science and Technology Organisation. Jim holds a PhD from the University of Cambirdge, UK and BSc from the University of Queensland in Australia.

Speakers: [Top]

Somesh Jha (Professor, University of Wisconsin (Madison))
Tom Reps (Professor, University of Wisconsin (Madison))
Bill Harris (Ph.D. Student, University of Wisconsin (Madison))

Title:

Secure Programs via Game-based Synthesis

Abstract:

Several recent operating systems provide system calls that allow an application to explicitly manage the privileges of modules with which the application interacts. Such privilege-aware operating systems allow a programmer to a write a program that satisfies a strong security policy, even when the program interacts with untrusted modules. However, it is often non-trivial to rewrite a program to correctly use the system calls to satisfy a high-level security policy.

This paper concerns the policy-weaving problem, which is to take as input a program, a desired high-level policy for the program, and a description of how system calls affect privilege, and automatically rewrite the program to invoke the system calls so that it satisfies the policy. We describe a reduction from the policy-weaving problem to finding a winning strategy to a two-player safety game. We then describe a policy-weaver generator that implements the reduction and a novel game-solving algorithm, and present an experimental evaluation of the generator applied to a model of the Capsicum capability system. We conclude by outlining ongoing work in applying the generator to a model of the HiStar decentralized-information-flow control (DIFC) system.

Bios:

Somesh Jha

Somesh Jha received his B.Tech from Indian Institute of Technology, New Delhi in Electrical Engineering. He received his Ph.D. in Computer Science from Carnegie Mellon University in 1996. Currently, Somesh Jha is a Professor in the Computer Sciences Department at the University of Wisconsin (Madison), which he joined in 2000. His work focuses on analysis of security protocols, survivability analysis, intrusion detection, formal methods for security, and analyzing malicious code. Recently he has also worked on privacy-preserving protocols. Somesh Jha has published over 100 articles in highly-refereed conferences and prominent journals. He has won numerous best-paper awards. Somesh also received the NSF career award in 2005.

Thomas W. Reps

Thomas W. Reps is Professor of Computer Science in the Computer Sciences Department of the University of Wisconsin, which he joined in 1985. Reps is the author or co-author of four books and more than one hundred seventy-five papers describing his research (see http://www.cs.wisc.edu/~reps/). His work has concerned a wide variety of topics, including program slicing, dataflow analysis, pointer analysis, model checking, computer security, code instrumentation, language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars.

His collaboration with Professor Tim Teitelbaum at Cornell University from 1978 to 1985 led to the creation of two systems — the Cornell Program Synthesizer and the Synthesizer Generator — that explored how to build interactive programming tools that incorporate knowledge about the programming language being supported. The systems that they created were similar to modern program-development environments, such as Microsoft Visual Studio and Eclipse, but pre-dated them by more than two decades. Reps is President of GrammaTech, Inc., which he and Teitelbaum founded in 1988 to commercialize this work.

Since 1985, Professor Reps has been co-leader, with Professor Susan Horwitz, of a research group at the University of Wisconsin that has carried out many investigations of program slicing and its applications in software engineering. His most recent work concerns program analysis, computer security, and software model checking.

In 1996, Reps served as a consultant to DARPA to help them plan a project aimed at reducing the impact of the Year 2000 Problem on the U.S. Department of Defense. In 2003, he served on the F/A-22 Avionics Advisory Team, which provided advice to the U.S. Department of Defense about problems uncovered during integration testing of the plane’s avionics software.

Professor Reps received his Ph.D. in Computer Science from Cornell University in 1982. His Ph.D. dissertation won the 1983 ACM Doctoral Dissertation Award.

Reps’s 1988 paper on interprocedural slicing, with Susan Horwitz and his then-student David Binkley, was selected as one of the 50 most influential papers from the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 1979-99. According to Google Scholar, the 1988 paper and the subsequent journal version have received over 1,600 citations.

His 2004 paper about analysis of assembly code, with his student Gogul Balakrishnan, received the ETAPS Best-Paper Award for 2004 from the European Association for Programming Languages and Systems (EAPLS). His 2008 paper about a system for generating static analyzers for machine instructions, with his student Junghee Lim, received the ETAPS Best-Paper Award for 2008 from EAPLS. In 2010, his 1984 paper "The Synthesizer Generator", with Tim Teitelbaum, received an ACM SIGSOFT Retrospective Impact Paper Award. In 2011, his 1994 paper "Speeding up slicing", with Susan Horwitz, Mooly Sagiv, and Genevieve Rosay, also received an ACM SIGSOFT Retrospective Impact Paper Award.

Three of his students, Gogul Balakrishnan, Akash Lal, and Junghee Lim have been the recipients of the Outstanding Graduate Student Research Award given by the University of Wisconsin Computer Sciences Department. Akash Lal was also a co-recipient of the 2009 SIGPLAN Outstanding Doctoral Dissertation Award, and he was named as one of the 18 awardees selected for the 2011 India TR-35 list (top innovators under 35).

In 2003, Reps was recognized as a "Highly Cited Researcher" in the field of Computer Science—one of 230 worldwide who received such recognition by the Institute for Scientific Information. As of February 2013, Reps was ranked 8th (citations) and 4th (field rating) on Microsoft Academic Search’s list of most-highly-cited authors in the field of Programming Languages, and 23rd (citations) and 13th (field rating) on its list of most-highly-cited authors in the field of Software Engineering.

Reps has also been the recipient of an NSF Presidential Young Investigator Award (1986), a Packard Fellowship (1988), a Humboldt Research Award (2000), and a Guggenheim Fellowship (2000). He is also an ACM Fellow (2005).

Reps has held visiting positions at the Institut National de Recherche en Informatique et en Automatique (INRIA) in Rocquencourt, France (1982-83), the University of Copenhagen, Denmark (1993-94), the Consiglio Nazionale delle Ricerche in Pisa, Italy (2000-2001), and the University Paris Diderot Paris 7 (2007-2008).

William Harris

William Harris is a PhD student and research assistant at the University of Wisconsin-Madison, where he is advised by Somesh Jha and Thomas Reps. His current research focuses on applying formal methods to problems in computer security. He received his B.S. from Purdue University in 2007, and received his M.S. from the University of Wisconsin-Madison in 2011. He has worked as a visiting researcher for NEC Labs America and Microsoft Research. He was a Microsoft Research Fellow from 2010 - 2011.

Speakers: [Top]

Nate Foster (Assistant Professor, Cornell University)
Arjun Guha (Assistant Professor, University of Massachusetts Amherst)
Mark Reitblatt (Ph.D. Student, Cornell University)
Cole Schlesinger (Ph.D. Student, Princeton University)

Title:

Network Programming in Frenetic

Abstract:

Modern networks provide a wide variety of services including routing, load-balancing, traffic monitoring, authentication, and access control. These services are logically distinct, but they must be implemented on top of low-level networking hardware, which offers no support for modular programming. Network programs are thus written in a monolithic style, which complicates programs, makes reasoning difficult, and frequently leads to failures.

In recent years, several research groups have applied ideas from programming languages and formal methods to help make network programs safer and easier to write. The catalyst has been the emergence of software defined networking (SDN) and OpenFlow as a simple and open platform for developing network applications.

This tutorial will provide an introduction to languages, abstractions, and reasoning tools for networks, focusing both on the low-level OpenFlow protocol and the high-level Frenetic language. Participants will spend most of the tutorial engaged in programming exercises. We will assume proficiency with basic functional programming in OCaml and some familiarity with undergraduate-level networking concepts. The tutorial will cover all other background material.

Bios:

Nate Foster

Nate Foster is an Assistant Professor of Computer Science at Cornell University. His research focuses on developing language abstractions and tools for building reliable systems. He received a PhD in Computer Science from the University of Pennsylvania in 2009, an MPhil in History and Philosophy of Science from Cambridge University in 2008, and a BA in Computer Science from Williams College in 2001. He was a postdoc at Princeton University from 2009-2010. His awards include a Sloan Research Fellowship, an NSF CAREER Award, a Yahoo! Academic Career Enhancement Award, and the Morris and Dorothy Rubinoff Award.

Arjun Guha

Arjun Guha is an Assistant Professor of Computer Science at the University of Massachusetts Amherst. He received his PhD from Brown University in 2012. His dissertation research covered semantics, type systems, and program analysis for JavaScript, with applications to Web security. Arjun spent 2012-2013 as a postdoc at Cornell University, working on the Frenetic project.

Mark Reitblatt

Mark Reitblatt is a fourth-year PhD Student in the Department of Computer Science at Cornell University advised by Nate Foster. His research focuses on problems in programming languages, networks and distributed systems. He previously received bachelors degrees in Computer Science and Mathematics from the University of Texas at Austin, where he worked with J Moore and Matt Kaufmann.

Cole Schlesinger

Cole Schlesinger is a fifth-year Ph.D. student at Princeton University advised by David Walker. His research focuses on developing safe and robust abstractions for programming software-defined networks, which are accompanied by formal models and proved-correct guarantees. His current work on the Frenetic project is driven by his background in formal methods and program verification in the programming languages community.